Book review: The Little Typer

On 2021-03-07 by ThatGeoGuy

I finally managed to finish working through “The Little Typer”. The “Little” series is a series of (semi-)introductory books published by MIT press, which typically use Scheme or Lisp as a vehicle to teach some interesting aspect of programming. In this case, “The Little Typer” aims to teach the most interesting aspects of dependently typed programming. The “Little” series has been one of my favourite series of programming books, and the books have always been a delight to work through. Having spent quite a considerable time working through the book (several weekends since around sometime last November / December or so), I figured I would write up a review, since I have a lot to say about the book!

The Little Typer by Daniel P. Friedman and David Thrane Christiansen.

The book clocks in at around 400 pages, but it’s not the length that made me spend so much time on it. I’ve read a considerable number of programming books, and I’ve worked in several languages, ranging from C, to Rust, to Scheme, and even dabbled in Haskell back in grad school once-upon-a-time. A large percentage of what I know about programming is self-study, but I like to believe that I’m relatively well informed. Needless to say, this book was dense, and it was considerably harder to read for me than any other books in the series have been in the past.

For this review, I wanted to go through the parts of the book I liked, some of what I didn’t, and advice to people who might try to work through the book themselves. If you just want to skip to the end, see my overall thoughts.

Why dependent types?

To be entirely honest, I did not pick up this book for the topic itself. Mostly , I read this because of how much I enjoyed the rest of the “Little” series, and I had some high expectations. In fact, when I had picked this book up, I hadn’t really known what dependent types were, or why one might be interested in them. I had known the book was about types, but I had actually thought it was going to be more inline with something like Shen, and discussing some of the more interesting points behind Hindley-Milner type systems.

To put it bluntly, this is not at all what the book is about. It certainly touches the boundary between strongly-typed languages and Scheme, but dependent types are different than just stapling Haskell and Scheme together¹. Instead, the book opened my eyes to a very different concept, in which types can be formed around something that is not a type (usually, a value). I’m not wholly disappointed, but I think not having formal education in programming langugage theory certainly didn’t help my confusion around the topic of the book.

Anyways, now that I’ve read the book, I think I can say with confidence that I now understand that dependent types are cool. However, they also appear to be a lot of work. I can categorize the main things I learned from this book in the following sections.

Types are proofs are computation

Using types to prove something is equivalent to producing a function that determines that proof. This is a bit abstract, but I think is part of the main thesis of the text. There’s a particular moment in the book where you define a function called even-or-odd, which not only proves that every Nat (natural number) is either even or it is odd, but can also given any number can tell you if that specific number is even or odd. Same code, but there’s two different ways to think about it.

Dependent types enable correctness preserving transformations

Using dependent types, you can implement a different program by first proving that two smaller programs are the same, and then replace-ing an easy-to-write program with a harder-to-write program in a correctness-preserving way. This was the main thesis of chapter 9, which I will probably speak more on later.

In any case, the interesting bit here is that by writing a proof that two programs are the same, we’re able to not only guarantee that a transformation preserves the semantics of the program but also use that proof to do the transformation itself. This is… admittedly still very abstract. The book spends time in Chapter 9 to show off how one might do this with two procedures, twice and double, and a third procedure twice=double that relates the two.

Given that “[o]ptimization is always just a few correctness-preserving transformations away”, this is very interesting! The idea that you can write programs this way is something I haven’t done before, and I don’t think is possible if you’re not deeply embedded into the Idris or Coq ecosystems.

Bridging compile and runtime together

The main bridge between types and values today is a lack of induction on types. Especially when working in C or Rust, we tend to distinguish between “runtime” and “compile time” concerns. One of the chief advantages of Rust over C in this respect, is that the more powerful type system can sometimes help us push many of our errors from runtime to compile time. This helps us specify what an “incorrect” program is, since an incorrect program will fail. Rust does this in a lot of ways², but there’s no way for the compiler to know about user-defined runtime values.

Values have types, and we can make judgements about those values (and their types). Together, this is how the book uses induction to effectively say: well, I don’t know what that value is yet, but I can break this type down and try to reason about the possibilities. This is akin to what is done in first-order logic, and I noticed a lot of similarities to relational (i.e. mini-Kanren) and logic programming styles, although the types do add a bit more theatre.

In any case, dependent types are all about bridging run and compile-time together. Why make assertions about just your types when you can make assertions about values as well? Or rather, assertions about every value of a possible type, or every type of a possible value? Or assert that a value must exist that has a property, etc.

The joy of being able to describe the universe

One thing I really enjoyed about the book is that it provides clear and concise names for many of the underlying concepts in type-theory. The first few that it throws out are constructor and eliminator, which actually helped me formulate a lot of thoughts around structuring types in other languages. In particular, languages often try to separate different kinds of functions as one of the following:

• Procedure
• Function
• Method
• Constructor
• Destructor

…and so on. Being able to say a function is either a constructor (creates a value of a given type), or an eliminator (picks a new expression based on a value of a given type) seems semantically useful. I no longer need to think in terms of getters, setters, accessors, properties, etc.: only eliminators. Of course, for the sake of my peers who have not yet had this revelation, I will probably still maintain this vernacular.³

Normal and Neutral forms of an expression are also very useful! This is effectively a distinction between known values (normal) and runtime-specific values (neutral). However, being able to identify when a value is neutral has at the very least given me a clear and concise way to express that I can’t use types as a solution in a non-dependently typed language.

There’s a wealth of small bits of natural language scattered throughout the book that invoke similar feelings. While not strictly about dependent typing (the above terms could all be used to describe Rust or C code, for example), I thought it was a valuable aspect of the experience.

What I didn’t like

There was a lot of good insight into the book. It challenged me a lot. However, there are still things with which I remain unsatisfied by.

Chapters 8 and 9

Chapters 8 and 9 were the most frustrating chapters for me. They were probably also some of the more important chapters of the book, in that they went very deep into introducing same-ness, equality, etc. In fact, one of my most important insights from the book was about how dependent types can be used to make correctness-preserving transformations! That said, I feel like these chapters were the weakest out of the whole book.

Notably, the textual descriptions of what was going on seemed to be lacking. It was very unclear early on why replace was needed, and the textual description is pretty bad. It would have been helpful had there been more small-scale examples of using replace, or just not having cong as a distraction at all, perhaps.

I think this distracted me pretty hard when I was going through these chapters, and I felt that the final implications of what replace can do given a proof that two values / types are the same was not made clear enough. These are easily the weakest chapters of the book, and the worst part is that they’re right smack in the middle. If you can grasp ind-Nat and ind-List you can probably work through every other inductive eliminator. However, I think the book definitely shows some weakness in trying to introduce same-ness, equality, and replacing types in expressions.

I would have loved to see this done more completely, but it really isn’t until later chapters that types like Absurd and Trivial are introduced, and you don’t even really get to the point regarding same-ness vs. equality until page 323, which is in Chapter 15.

Ordering

This is going to be very subjective, but by the end of the book I felt that the whole thing could have been ordered differently. In particular it felt weird that the entire introduction chapters discussed Pie the language, then moved to induction over numbers / lists / vectors, then went into types like Either or Trivial or Absurd.

I think making small assertions using induction on Either types would have been a bit more friendly early on, especially with regards to induction. Starting with natural numbers seems small enough to be presentable while also interesting, but by the time I got to the section of the book that dealt with Either / Trivial / Absurd, I felt like there wasn’t nearly as much to say.

I would grant that perhaps Absurd belongs later in the book, since making negative assertions (i.e. not-X) gets into some pretty weird territory. That said, if your goal is to teach induction, doing so with Either is certainly easier than doing so with Nat. I found the later chapters easier than chapters 8 and 9, so perhaps I was expecting the difficulty curve to be a bit more linear.⁴

Touching on this point and the next one a little bit together: parts of Pie like which-Nat are effectively just a reduction into ind-Either. Perhaps the author doesn’t have to focus on every relationship between concepts in the book, but I certainly feel that it would have made the concepts a lot less abstract.

Useless(?) parts of Pie the language

This is mostly a complaint about symm, more than anything. symm is introduced as a way to invoke a “symmetry” relationship over an equality type. Basically: (= T from to) is the same as (= T to from). This is usually a pretty useful feature in logic systems that is often taken for granted.

symm is introduced near the end of chapter 9 to be able to describe to Pie that twice=double is the same thing as double=twice. They’re equal, they’re symmetric, right? Well, guess what, that’s the last time you see symm get used. No, seriously, it’s only a brief mention at the end of chapter 9 and then it disappears! It is literally only on page 217, and it’s gone. I get that it exists because otherwise going through every motion to re-define double=twice when you already have defined twice=double would be a lot of work; yet, it seems a bit of a distraction that it is included in Pie the language by default.

I had expected the idea of symmetry to show up again later in the text. In a later chapter, there was a need to define zero-not-add1, which is an assertion that zero is distinct from any number that has had 1 added to it. Even later, the book needs us to define add1-not-zero. The minute this came up, before even reading the next dialog, I was convinced this was a problem with symmetry, and the book was going to demonstrate how to define symmetries over absurdities. Unfortunately, the book just redefined the same function (albeit it’s a 4 line definition) with the add1 and zero in reverse order.

Needless to say, I was a bit disappointed because when I took first-order logic it was fairly natural to abuse notions of symmetry, commutativeness, etc. Here, we just took the easy route. I’m sure there’s an explanation for why this isn’t brought up at all, but even a footnote would have been satisfactory to describe why we couldn’t apply some form of symmetry to this problem.

Refusal to explain

Early in the book, you’ll encounter the phrase “Recursion is not an option.” This is asserted over and over again, as if it is a cute joke about how the argument recurs onto itself. I found this very annoying, because the book doesn’t really ever give a proper explanation as to why recursion is hard when working with types in this way. There’s the introduction of “primitive recursion,” and induction as it is used in this book is a form of recursive reasoning (rather, recursion is a type of inductive problem solving), but alas, you only get “recursion is not an option.”

Eventually you might read beyond the book and discover why other languages like Idris or Coq or whatever have limited recursion, and need to make very specific guarantees about recursion when it occurs. This is distinctly due to decidability / completeness problems that have yet to be solved. The Little Typer, however, doesn’t even attempt to explain that this a challenge, it just meaninglessly asserts that we can’t use recursion. I hardly feel as if a Y-combinator is out of reach in this situation, and I’m also certain it would break some of the guarantees made by Pie.

Again, even a note at the end of the book that explains this directly would have been welcome, but there doesn’t appear to be such a thing. Maybe this expectation is too harsh to lay on the authors, but it did stand out to me at least as an annoying omission.

Warning(s) to the reader?

Pie is slow

Many of the types you implement are probably not going to be very efficient in the name of pedagogy. If a function asks for a natural number, you may be inclined to put a very large number in. It is probably best not to use any number over 1000 if you don’t want Pie to ravage your CPU.⁵

The Little Schemer is not enough

The preface for this book asserts that all you really need to write and understand the code in the book is the first four chapters of The Little Schemer. It is highly probable that this is insufficient if this is your only programming experience. It is certainly all you need from a “how does this evaluate” perspective, but you’ll be missing out on a lot of context if you’ve never used a statically typed language before, or never structured a proof before.

Many of the insights I gained from this book were a direct result of having worked with many languages in the past, specifically in the context of having thought about types and type systems. To be entirely fair, you don’t need my experience to enjoy this book, and I probably have some level of assimilation bias due to the languages and tools I work with every day. However, if you’re coming at this and you’ve literally only ever used Scheme, and only worked through The Little Typer, you’re going to have a rough run of it. I also think you’ll be missing out on some of the key parts of the book that I enjoyed.

If I wanted to prescribe a minimum set of “what you need to know to get the most out of this book,” I’d probably recommend:

• The Little Schemer (yes, it is necessary but not sufficient)
• A class or textbook on first-order logic outside of programming. A 1st-year philosophy course on the subject would be more than enough, but learning how to structure proofs is a huge boon to getting through constructing proofs with types.
• Learning at least one language with a strong type system. This does not mean C or C++. I would recommend Shen to keep things as close to Scheme as possible, but Rust / Haskell / ML are also excellent choices.

Without all the above, I don’t think I would have enjoyed this book or found enough merit in it to continue past the first couple chapters. Dependent types are cool, but the reasons I think they are cool depend 😉 on the context I had built up surrounding proofs, type systems, etc.

Overall thoughts

The book aims to be an introduction into dependent typing and into structuring your types as proofs. The book does a really good job at a lot of this, and is very good at providing names and natural language for describing the process as you learn. In genral, I would say I learned a lot from this book, and while I will probably take a break from dependent types for a while, I can see why dependently typed languages are pretty cool, and learned some of the unique aspects that make them interesting.

The book does have a fairly steep learning curve if you’re not familiar with proof systems, first-order logic, or typed programming languages in general (more specifically, typed programming languages that use types in a more rigorous fashion than say, C). If you’re looking for the book to connect every dot and line in the realm of dependent types, I think you’ll be sorely disappointed. There are some concessions the book makes for brevity (symm, not explaining why recursion is not allowed), and you’ll have to live with those. Overall, what annoyed me the most were chapters 8 and 9, which seemed to be far less direct than many of the previous chapters. There’s a lot to learn there, but I retain my belief that they are the weakest chapters of the book (despite being very critical to later sections).

If you’re looking for a programming book to challenge you, or you just have a natural curiousity, I highly recommend this book. The whole “Little” series is pretty incredible, and this book doesn’t disappoint with both small insights you can inject into your current programming practice, or big shifts in how you think about types vs. values. Be warned, it is not something you’ll consume in a weekend or two. If you do though, feel free to @ me on twitter and brag, I will not be upset.

Having gone into this book expecting something completely different, I’m still happy I stuck through the book. I learned a lot, and despite my grievances, I feel like I still understood the central theme. While I don’t see any immediate practical first-order effects from the book (I am not, for example, going to try and convince my team at work to use Idris), I feel that some of the intuitions have already helped me in thinking about some of the problems I encounter.

---