Book review: The Little Typer
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 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 together1. 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
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
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,
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,
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 ways2, 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:
…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.3
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
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
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-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
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.
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
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
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.4
Touching on this point and the next one a little bit together: parts of Pie like
which-Nat are effectively just a
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
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
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.5
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.
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.
In reality, the Pie language used throughout the book is more like stapling together Idris and Scheme. Idris 2, as I understand, is actually implemented in terms of Chez Scheme. They may not be so different after all! ↩
Rust does this in a lot of ways. The borrow-checker is one, in that null pointer checks and lifetime semantics are represented as polymorphic types (i.e.
'staticor whatever) on references / pointers. Strongly typed enums are another way, if you want to guarantee that you always check every possibility of a condition.
However, Rust still cannot perform induction on types and thus cannot fully check every part of your program. As an example: Rust cannot at compile time check if a number is zero or not-zero, and then branch on different types as a result of the value of that number. Dependently typed languages with induction are needed for this in a general form. ↩
I do understand why languages feel the need to be more specific about the difference between a function and a procedure, or a method vs. a constructor, but I also feel like this is one of those distinctions that nobody gets correct. When I talk to people who write primarily in C++, everything is a function. In Java, everything is a method. In Scheme, a procedure. Semantically there are differences but I have found pushing the discussion more towards the constructor / eliminator dichotomy has helped in some cases.
It is much clearer to say “we need to write a new constructor from this type” or “we need an eliminator to access the internal resource X” than to say “write a function doing X.” One problem that I see a lot with junior programmers is writing methods instead of constructors, resulting in types that can contain a lot of invalid states. This isn’t advice per sé, but I thought the distinction was a cool and useful insight in the book that was never directly pointed out to me before. ↩
There’s a lot of interesting “either-or” logic that could have been done by compounding the
Atoms. Had I written the book, I probably would have had at least a chapter early on to demonstrate what induction is by limiting the scope to a set of binary choices, and then expanding this to numbers.
After all, if you wanted to test “either-or” relationships on numerical values, you’d need a nested
Eithertype for every value, sequentially. Of course, this would get burdensome quickly, which leads you to introducing
ind-Natas a more natural (hah, get it) way to do induction on numbers. As I mentioned later,
which-Natcould be more or less implemented in terms of
Perhaps the error in my thinking here is that I’ve been pre-disposed to a lot of programming and logic over the years, and I have some kind of assimilation bias. ↩
This is particularly important for the
even-or-oddfunction. I put a number over a few billion into it and very quickly realized I had made an error in judgement. ↩