For the last year, I have been reading Benjamin Pierce’s Types And Programming Languages (TAPL) with the London Computation Club.

Here are some of the things I learned from the book and the meetings with the group.

An Appreciation of Lambda Calculus

My computing degree introduced me to lambda calculus, presenting it as a system that could model computation and prove things about it such as the halting problem. Since we’d already covered similar concepts earlier with Turing machines and never did anything practical with it, lambda calculus never felt useful to me and it was a topic that I promptly forgot about.

TAPL first introduces lambda calculus without types and then walks through how you could add typing to it. Later we see how this typed lambda calculus can be augmented with other languages features such as lists, recursion and subtyping in a type-safe way.

[lambda calculus's] importance arises from the fact that it can be viewed simultaneously as a simple programming language in which computations can be described and as a mathematical object about which rigorous statements can be proved.

Benjamin C Pierce, Types and Programming Languages, page 51

The group went through evaluating and typing many lambda calculus expressions together on the whiteboard. This hands-on approach and gave me a greater understanding of lambda calculus, and the book showed me how you could then reason about it to prove properties of the language.

Being Able to Implement a Type Checker

The book comes with a reference implementation in OCaml. The book group decided to build up a Ruby implementation to mirror this as we went along.

If we hadn’t done this, I still might think I knew how to implement a type checker without actually being able to.

While there were some parts of the book that I thought I understood on the first read, when we came to implement the features as a group I realised I had sometimes missed the point. I found that seeing and writing the code as we went corrected my misconceptions and demonstrated the group’s knowledge.

One such part was the introduction of subtyping rules for functions which I found hard to think about until we wrote and saw it working with some test cases.

As well as following the group implementation in Ruby, I wrote some of a type checker in Elixir. I enjoyed doing more Elixir and found its pattern matching was a useful tool in deciding when running typing or evaluation rules.

Knowing the Trade-offs that Type Systems Make

A theme throughout the book was the trade-offs that you, as a designer of a typed programming language, would have to make.

These trade-offs were often the following:

• Expressiveness - does the type checker let you write all the programs that you might want to.
• Performance - how fast can the language be type checked, and what might the impact be at runtime.
• Implementation Complexity - how difficult is it to implement the type checker and prove it to be correct.
• Verbosity of the Language - how often does the programmer need to define types and handle error conditions.
• Type Safety - will the type checker let you write programs that get stuck or produce type errors while running.

An example of a language feature with trade-offs is casting. Casting gives us the ability to override the type of a value at runtime.

Object anObject = "hello";
String aString = (String)anObject;

Casting improves the expressiveness of the language. It allows programmers to do things that would have been hard to do before such as deserialise untyped data into typed values or retrieve typed values from an abstract data type. However, this comes at the cost of type safety since casting could produce a type error at runtime.

One way that Type safety can be returned to the language is by requiring the programmer to write an error handler that can run in the case that the cast fails. This handler increases the verbosity of the language since it requires more code to be written by the programmer every time they use a cast.

Casting is just one example of a feature that a typed programming could choose to support. We went through many other features in that the book presented as ‘extensions’ to a core language such as lists, references, subtyping and recursion.

I also enjoyed learning about the differences and trade-offs between structural and nominal type systems. I’ve had limited exposure to typed languages and this explained to me why the typed lambda calculus presented in the book and languages did not have the explicitly named subtypes that a language such as Java does.

Getting used to Complex Mathematical Syntax

Reading TAPL has not just given me a better understanding type systems. It has also made me more comfortable with the mathematical syntax and conventions used throughout the book. This could make other math-heavy books and research papers accessible to me when they may have been hard to follow before.

Even if I did get used to the mathematical syntax of the book, some of the examples were still hard to follow. In the last chapter that we looked at together, we spent a while deciphering the single-letter variables that the inference rules used. As a software developer, I am used to using descriptive variable names to improve the readability code. I think it’s a shame for the book to follow the mathematical convention of single-letter variable names and optimise for terseness rather than understanding.

Ending the Book

We made it to the end of the section on subtyping¹ and came to a group decision to finish there. We had enjoyed the time we’d spent on it and what we had learned but didn’t think it was worth investing more time in the rest of the book. I found I had understood some of the main points of the book and had been getting less out of it as the topics became more niche. The group also particularly enjoyed building up our implementation as we went along and found that the opportunities to do this diminished during the subtyping section.

I’m grateful for the time all the for other members of the Computation Club put into hosting, organising, writing code and for the discussions we had along the way.

If you would like to read more about TAPL, the London Computation Club has write ups of each of our meetings. You can also find out more about the club and what we’re doing next.