---

Who is this book for?

The Little Typer is an introduction to dependent types, but not a textbook. So you won’t get deep theories, or practical details. Instead, you’ll get what’s like to “do” dependent types.

The main gain of dependent types, in my opinion, is the ability to encode a useful property into a type. Then the type checker will help you to construct a program of that type, and at the same time, you get a proof of that property.

In the book, the dialogue will walk you through several examples of this process. And it’s even better if you try to work out the proof by yourself before reading the text. In the end, you’ll have a pretty good idea of the workflow and will perhaps be eager to try out on “real world” problems.

So I think this book is best for those who are looking from the outside, or trying to get their very first steps into the field of dependent types. It’s a system small enough to understand and experiment with freely. Then you can take what you’ve learned and meet the industrial level systems. They will feel less magical and more grounded. Although you might not know the exact mechanism, you’ll find the intention and the general direction very familiar.

It’s not exactly a bad deal, to get the big picture out of the little typer.

Set up the Pie

Playing with the Pie language is perhaps the most essential part of the learning process, but the set up is not exactly simple, at least not for me.

What the above linked repository contains is the implementation of the Pie language, not code examples used in the book. As is stated in README, the language is provided as a package to Racket, and it’s already in the Racket package server. So to use the language, you don’t need to clone or build the repository (it doesn’t build for me). What you want is to install Racket, then install the pie package. After that you’re good to go.

Install DrRacket from Racket

The path of least resistance is to use DrRacket. It’s an editor/IDE that comes with Racket. To install Racket, head to the download page and choose your platform.

Install Pie

After Racket is installed, open DrRacket. Then follow the Installation Instructions from README:

From DrRacket

Click the “File” menu, and then select “Install Package…”. Type pie in the box, and click the “Install” button.

which will download and install pie.

To create and run Pie programs, start the file with #lang pie. You might need to restart DrRacket for the changes to take effect.

To check the installation, put the following into the editor:

#lang pie

(claim +
  (→ Nat Nat
    Nat))

when you hover over keywords like claim or Nat, there should be an arrow pointing to it from pie and a floating window saying something like “imported from pie”.

You can also use the REPL (or the “interaction”) to test. In the menu, find “Racket”, then hit “Run” (or press F5), which should bring up the interaction window. Type (add1 zero), then hit enter, it should report (the Nat 1).

Configure DrRacket for Pie (optional)

All of the following configurations are optional but useful.

Preference

Inside the DrRacket - Preferences setting group:

1. Font and colors. One feature that I find especially useful is Colors - Racket, which allows you to define styles for different component types. Another one is Colors - Background - Parenthesis color scheme. You can use e.g. “Shades of grey”, so that different levels of parentheses have different shades of colors.
2. Background Expansion. Tick “Enable background expansion”, so that errors are reported as you type. I also find the “with gold highlighting” option very useful.

Keybindings

These are platform specific. Three especially useful ones are Run (F5 by default), Check Syntax (F6), and Reindent All (d:i, which means Cmd+i).

You can show and search existing key bindings from Edit - Keybindings - Show Active Keybindings.

macOS users might want to tick Treat alt key as meta under DrRacket - Preferences - Editing - General Editing for some keybindings to work.

Input fancy symbols

The book uses unicode symbols extensively and Pie uses them as well.

It is also possible to use the ASCII version directly, like -> for →, fun for λ, etc. You can find a complete list of these mappings in The Pie Reference, available online or locally from search-help-desk (default F1) and then search for pie.

Alternatively, there’s the LaTeX approach, which gets tedious after a while.

What I used is to input these symbols via custom keyboard shortcuts.

Create a file with the following content:

#lang s-exp framework/keybinding-lang
(keybinding "d:r" (λ (editor evt) (send editor insert "→")))
(keybinding "d:p" (λ (editor evt) (send editor insert "Π")))
(keybinding "d:l" (λ (editor evt) (send editor insert "λ")))
(keybinding "d:s:s" (λ (editor evt) (send editor insert "Σ")))

From the menu, Edit - Keybindings - Add User-defined Keybindings... and select this file. Note that DrRacket only loads the keybindings at start. So after a change to the file or new bindings being added, you need to restart DrRacket for it to take effect.

Then you can use Cmd+r to input right arrow and so on. Notice I used d:s:s or Cmd+Shift+s for Σ because d:s was used for saving the definition.

Read the documentation and create your own keybindings. And again, macOS users might want to tick Treat alt key as meta under DrRacket - Preferences - Editing - General Editing for some keybindings to work.

Tips for middle to late chapters

If you find any part of the book difficult, one option is to revisit previous materials and do the exercise again. Apart from this “git gud” advice, I also have an approach that works well for me. I should highlight that I had some experience with other proof assistant, so it might not be universally applicable.

When a new concept is introduced, I find it useful to think about the motivation. For example, why is mot needed for induction? Is it possible to do induction without this argument? Do we have mot in other proof assistants? Why or why not? What’s the minimum information needed to automatically fill out a hypothetical mot?

Answering these questions helped me a lot for later chapters. For example, figuring out the purpose of mot in the definition of replace.

For the last question specifically, before reading Chapter 9, I recommend this blog post by Andrew Helwer, which adds a small dialogue before the text to clarify some concepts. I find it very helpful.

TODO helps, sometimes

In the source file, you can write TODO in place of a term. DrRacket will give you a list TODOs and for each one, the needed type and the typing environment. This corresponds to the boxes in the book. It is called a typed hole in Haskell and Agda.

This feature would have been much more useful if it weren’t for two limitations of Pie:

1. The type checker often cannot determine the type in presence of TODO.
2. Types are often “elaborated”, that is, with definitions unfolded, making it hard to read.

These limitations are understandable since Pie needs to be small and simple. However, this also makes me appreciate the “delaborator” in Lean and notation printing in Coq more.

Learn by playing and reading, or thank you Jonathan Blow

At the end, I want to reflect a bit on the methodology exemplified by this book.

You know that a conventional wisdom of story telling is “show, do no tell”. Well, this book certainly does not “tell” you what are dependent types, but “shows” you how to do dependent types. With the provided Pie language, it actually follows a better principle. I call it “play, and thus show”.

In a talk titled Video games and the future of education, Jonathan Blow identifies two ways of learning: by playing with a thing and by reading a book. Of course, these two methods are not mutually exclusive, rather, they often complement each other.

Playing can give you a lot of knowledge, fast and intuitively, but often implicit and imprecise. Think about writing a manual to teach people how to ride a bike. After thousands of pages, it would still be difficult to get the idea through. Books, on the other side, is very good at conveying precise knowledge, but it can be quite hard to make progress (or even to evaluate the progress already made!). Jonathan postulates that the ideal form of education should be a combination of both methods.

Well, with the advent of a myriad of interactive textbooks, we can get pretty close to that ideal form:

1. Software Foundations comes with exercises to be finished with the help of and checked by the interactive theorem prover Coq
2. Natural Number Game by Kevin Buzzard (and the Lean 4 port) teaches the Lean theorem prover with carefully designed levels
3. An interactive version of Learn You a Haskell for Greater Good! teaches you, well, Haskell. The interactive version was ported by my friend James Brock, a big believer in interactive learning and the computational essay

I think The Little Typer along with the Pie language could well be consed onto this list of shiny examples. Anyway, it is a much bigger topic and beyond the scope of this little blog post.

Enjoy your read and play of The Little Typer!