Online reference book for *implementing* concepts in type theory.

Solution 1:

There is no such book. If someone wants to implement a proof assistant based on type theory now, they can look at a) tutorial implementations b) papers c) source code of existing systems.

The issue with a) is that it only covers a small fraction of real-world functionality and commonly presents naive solutions which don't scale and differ greatly from real-world implementation. The issue with b) is that it's scattered, contains lots of outdated and irrelevant information, requires expertise to navigate, and it's also incomplete with respect to real-world systems. The issue with c) is that it's even harder to navigate and contains many legacy hacks and suboptimal solutions.

It is also the case that the core implementations of the real-world systems are very different. E.g. Coq elaborates induction to fixpoints and case splits, Agda to recursive definitions and case trees and Lean to eliminators. There is also no clear consensus on design philosophy and in particular on how big a "kernel" should be and what it should include.

Nonetheless, I can do a quick survey on references. Be warned that it is highly opinionated and reflects my personal take on the subject.

1. Basic type checking and conversion checking

A modern view on this matter is that Coquand's semantic type checking algorithm is the preferred basic algorithm because of its performance and simplicity. Bidirectional type checking is another ubiquitous foundational principle. All of the sources below use both.

• http://davidchristiansen.dk/tutorials/nbe/ detailed and beginner-friendly. Code available in Racket in the previous link, there's also a Haskell version.
• Coquand's original paper has more technical parts, but the basic idea is readable. Includes Haskell appendix.
• My minimal self-contained Haskell implementation.
• Another small implementation, in OCaml, with additional explanation.

2. Basic unification and inference

Here, the core ideas used in the larger systems are pattern unification and contextual metavariables. See my introduction.

3. Advanced unification, elaboration, implicit arguments

• Chapter 3 of Ulf Norell's thesis is good introduction to implicit arguments and constraint postponing. I have again a small implementation for implicit arguments (not for postponing though).
• Abel & Pientka on advanced unification features, most of which are implemented in Agda. This is a bit dense and short on implementation details.
• Gundry & McBride significantly overlaps with the previous reference, and is helpful as an alternative take.
• Ziliani & Sozeau on unification. Describes a version which is not the one actually implemented in Coq, but which is fairly close. Contains many implementation-relevant details.

4. Inductive types, induction, termination checking

At this point, approaches diverge and literature becomes sparse. Coq, Agda and Lean have greatly different implementations.

• Mini-TT has simple inductive types and dependent case splits. Less expressive than Coq/Agda but good as starting point.
• Reference on the calculus of inductive constructions used in Coq. This is fairly detailed, and it should be possible to do an implementation based on this.
• The most recent piece on Agda pattern matching. Also partly describes inductive types in Agda. Fairly technical.
• The third main approach is compiling to eliminators, which is used in Lean AFAIK. The Lean elaboration paper lists references on elaborating to eliminators.

On termination checking, the main reference is this, which is very similar to the one used in Agda. I'm not familiar with the Coq termination checker, I believe the basic principles are the same, although the Agda one is more powerful/complicated. In Lean, termination checking is implicit in the compilation to eliminators.

5. Modules, type classes, automation

Unfortunately, I run out of expertise at this point, and I'm not sure what are the good references and approaches. The CiC manual and Norell's thesis can be used to copy the Coq or Agda module implementation. For tactics, reflection and type classes, I imagine the best would be to dig into Coq/Agda/Idris/Lean docs and sources and learn how they work.

I haven't mentioned Idris so far, because it's similar to Agda, and its unique features are fairly experimental and more relevant to programming than to proof writing. I'm mentioning error reflection here specifically which I think is highly useful in any system.

Solution 2:

These are not complete books, but they are the most useful written resources I can think of (in addition to what András Kovács already mentioned).

Daniel Friedman and David Christiansen give a somewhat comprehensive treatment of the implementation of Pie, a small dependently typed language, in the appendix to The Little Typer.

Andres Löh, Conor McBride and Wouter Swierstra describe a tutorial implementation of a dependently typed lambda calculus here.