Why Advanced Topics in Types and Programming Languages Still Matters

I finished Benjamin C. Pierce’s Advanced Topics in Types and Programming Languages and kept thinking the same thing. A lot of “new” language features are old papers wearing a hoodie.

Rust’s borrow checker. Proof-carrying stuff in browsers and kernels. Module systems that still make people cry. Dependent types showing up in Lean, Agda, Idris, and even corners of Haskell. This 2005 MIT Press book is where a lot of that theory sits in one place.

Book: Advanced Topics in Types and Programming Languages Editor: Benjamin C. Pierce ISBN: 0-262-16228-8 Publisher: The MIT Press, 2005

This series is my review and retelling, chapter by chapter. Not a textbook rewrite. I want the ideas in normal language, plus what I actually think after sitting with them.

What this book is

ATTAPL is the sequel to Pierce’s Types and Programming Languages, usually called TAPL. TAPL is the friendly-ish intro: lambda calculus, simple types, references, subtyping, System F.

This one is not a second textbook with one voice. It is a stack of expert chapters. Each chapter has its own author. Pierce edited it so the notation does not completely fall apart, but you can feel the style change when you flip from Walker to Necula to Pottier.

The audience is graduate students and researchers who already know the first half of TAPL. If you have never seen a typing judgment, this book will flatten you. If you have written a type checker, or you keep wondering why Rust, ML, and Coq feel related, you are in the right room.

The five parts

The book is split into five chunks.

Precise type analyses. Types that track more than “this is an int.” Linear and ordered types count how you use a value. Dependent types let types mention actual values, like “a vector of length 5.” Effect types and regions track what a computation does to memory, not just what it returns.

Types for low-level languages. Can assembly be typed? Can untrusted machine code carry a proof that it will not trash your process? Greg Morrisett’s typed assembly language and George Necula’s proof-carrying code are the two answers here. This is the 90s and early 2000s mobile-code panic, written as math.

Types and reasoning about programs. Compilers are not the only clients of types. Humans use them to prove two programs behave the same. Logical relations and typed operational reasoning are the tools. Dry on the page. Extremely useful if you care about “can I swap this data structure without anyone noticing.”

Types for programming in the large. ML modules. Functors. Abstract types that sometimes reveal their definition and sometimes do not. Then Christopher Stone on type definitions and singleton kinds, which sounds boring until you try to compile type t = int without lying to the type checker.

Type inference. The last chapter is a monster. François Pottier and Didier Rémy try to explain what production ML inference actually is, not the cartoon Hindley-Milner you see in a blog post. Constraints, HM(X), rows. If you only read one technical chapter because you write compilers, this is the one.

Why I bothered

I did not pick this book because it is cozy. It is not.

I picked it because a lot of current language design is still arguing with these chapters. Linear types did not stay in a paper. They leaked into Rust, into ATS, into parts of Haskell, into session types. Regions keep coming back every time someone is mad at the garbage collector. Proof-carrying code is the ancestor of a lot of “don’t trust the compiler, check the artifact” work.

And ML modules are still the most ambitious module system most working programmers never fully learn. If you have ever fought OCaml functors, or wondered why Rust traits and Haskell type classes are not the same thing as ML modules, Harper and Pierce’s chapter is the map.

How I am writing this

Each post covers one chapter, or half a chapter when the source is huge. Chapter 10 is long enough that it gets four posts. I am not dumping inference rules on you. I will use small examples: file handles, vectors, stack slots, functors, record fields.

I will also say when a chapter felt like homework. Some of these authors write like they are talking to three other people in a seminar room. That is fine for a research book. It is a bad way to remember the idea six months later.

You do not need to read the posts in order. Pierce tried to keep chapter dependencies light. Still, part I before part II helps, and Stone’s type-definition chapter makes more sense after the ML modules tour.

Who should skip it

If you want a first type-systems book, get TAPL, or Practical Foundations for Programming Languages, or a modern tutorial. ATTAPL assumes you already know why substitution has to avoid capture.

If you want “how do I ship a language feature next week,” some chapters will feel far from production. The TAL and PCC chapters are closer to systems work. The logical relations chapters are closer to a theory course.

If you like seeing the same idea show up in compilers, proof assistants, and language design, stay. That is the whole point of this series.

Next I start where the book starts: you cannot close a file twice if the type system spends the file when you close it.

Next: Linear Types and Resource Control in Substructural Type Systems