My favorite type theory book

I often see questions about what to read to learn type theory and I recommend Harper’s Practical Foundations for Programming Languages (PFPL). To be clear, this book is not a good recommendation if you want to learn more practically how to think in types. It’s instead a deep dive into what are types, why do they work, and how do we design practical type systems which cover the features we see in many programming languages.

First, a critical piece of reading advice

Before I go any further I need to mention a critical trick for reading this book. Unless you are very comfortable with formal proofs, skip to “Part II: Statics and Dynamics” to begin. You may struggle with some exercises which have prerequisites in Part I—skip those too for at least a little while. Once you get the hang of what types mean, return to Part I, recover those dependencies, and return.

Part I covers the foundational formal objects that type theory is built upon—the syntax. It introduces the formal notion of a judgement and methods of proof that work atop judgements. Effectively, this is a design document for actually implementing a type system. It’s also critical for demonstrating the soundness of the techniques you learn throughout the book.

But unless you’re very comfortable with this kind of formal thinking already it’ll be stupendously dry and almost without value. Even if you are very comfortable with formal proof, you probably still want to skip them. The rest of the book is full of interesting content that’s actually about types as opposed to proof systems for talking about types. Reading it will motivate the usefulness of Part I.

Anyway, that’s my disclaimer. If you don’t believe me, this is also, to my understanding, how Dr. Harper teaches this book himself.

Practical foundations of programming languages

By its title, PFPL isn’t even about type systems. Practical foundations for programming languages actually feels about as far away of a study of type theory as you might imagine. Type systems feel neither practical nor foundational.

This worldview is pervasive in PFPL, though. Instead of treating types as a veneer atop programming languages, PFPL uses them to explore foundational notions of data and computation. Types become both the language for discussing programming language features and the scaffolding which lets us glue these features together safely.

The core narrative of PFPL is the slow construction of an “industry strength” programming language from austere beginnings. Part II thoroughly explores a language of arithmetic expressions involving numbers, addition, and multiplication. Part III explores Godel’s T language which includes natural numbers, recursion, and function abstraction (lambdas). Part IV adds simple data and their types. Part VI extends these data with recursion enabling infinite data types. Part VII extends the type system to enable more complex type abstraction like polymorphism, existential types, and higher kinds.

And it goes on, slowly increasing the complexity of the language and the type system that describes it. You “grow” a language throughout the book arriving eventually at concurrent, distributed, modularized Algol.

Read the TOC in the partial preprint Dr. Harper has on his website to get a sense for the progression.

Why I like PFPL

In going from 0 to understanding basic type theory there are essentially two textbook choices: PFPL and Pierce’s Types and Programming Languages (TaPL). I recommend both, but if pressed I always recommend PFPL.

The biggest difference between the two is that PFPL is opinionated and narrative. The arc of “growing a language” throughout the book provides motivation for each new language feature and each exploration of the theory of types needed to describe those new features. You feel invested in the developmental arc and even get to get a sense for the historical work required for each of these features to be designed and refined.

TaPL is, to my eye, more encyclopedic. To be clear, it also has a narrative arc of growing a language as new type theoretic and linguistic features are added step by step. At the same time, TaPL often feels like more of an exploration. It holds you hand more and explains things more luxuriously. It also has OCaml code companioning the material so you can really sink your teeth in and play with an implementation of these techniques.

In a lot of ways, it might be more your cup of tea than PFPL. You can take a look at the TaPL TOC as well and get a sense for whether it might be more of your style.

But I still recommend PFPL. Skip Part I, don’t get too hung up on the exercises (at first!), and focus on the narrative. There will be less hand-holding, less explanation, less preparation, but you’ll be able to pick up a perspective on the whole affair that’s a little harder to see in TaPL.

And then, of course, go read TaPL afterward. And possibly even Pierce’s follow-up, Advanced Topics in Types and Programming Languages, after that.

A final nudge

One last, very minor reason you might want to try reading PFPL first is that there’s a preprint PDF available for free from Dr. Harper’s personal website. This is an early preprint, may contain errors, and is missing whole sections. That said, you can use it to read quite a ways into the book and see how it feels.

But then go buy the hardback. I personally find it a lot easier to read math books when you’ve got a physical copy. It also makes for a great coffee table book to intimidate your friends.