Reading Notes — Types and Programming Languages

A surprisingly fun read on type systems and programming languages

Types and Programming Languages (TAPL) by Benjamin C. Pierce is known as the introductory material on type systems and their application/implementation in programming languages. So much so that it’s very difficult to not run into this book when researching literature on types.

So inevitably, I came across it a couple months ago and it looked very daunting at first glance. Its content is very formal as it is designed as graduate-level course literature. This is what initially put me off from reading it.

Despite my premonitions, the book’s material is actually more intuitive than I previously thought. I realized that if I restrain my initial gut reaction to be apalled at the book’s formalisms, the content is not difficult to grasp.

Additionally, the book has several chapters where it walks you through applying its concepts by writing several type-checkers in standard ML (which feels very close to Haskell / Rust). So you aren’t just bombarded with theory, you actually get a taste of its practical application.

So a few months ago I set forth in reading TAPL. I wanted to learn about Hindley-Milner style type inference so I plotted a path based on the book’s chapter dependency graph tech tree:

I finished my tech tree in about a week of casual reading in my free time, and I was surprised by how much fun I had advancing through the chapters. I’ll definitely write about some of my findings later.

A chapter that was unexpectedly the most fun was chapter 5: The Untyped Lambda-Calculus. The lambda calculus is the underpinning “computational substrate” for the type systems presented in the book, so an entire chapter is dedicated to teaching the reader the ins and outs of it.

This was a lot of fun because the lambda calculus is a simple language with only variables, functions (lambda abstractions), and function invocations (applications). The book walks you through building basic programming abstractions like conditional logic, boolean, numbers, arithmetic, pairs, and lists with just the basic constructs of the lambda calculus.

Side note: A critique on compiler/type systems educational materialλ

If you try to look online for learning resources, 90% of them will be academic literature chock-full of formalisms that are inaccessible to those outside of academia.

Bidirectional typing, in particular, is extremely simple to implement and very intuitive. However, a simple Google search will lead you to resources that shroud its simplicity with academic formalisms.

This makes me wonder what other simple computer science concepts suffer a similar dilemma, and how much learning I’m missing out because of my tendency to immediately dismiss certain things.