Tutorial implementations of NbE

Question

For a project I'm planning on doing with some students this summer, I'm looking for an implementation of normalization-by-evaluation whose code the students can read, understand, and extend. So I'd like the code to be written for clarity at the expense of efficiency, hopefully well-commented and documented. I'm not too picky about the object-language, but it should be typed, simply or dependently I don't care too much. I would also like the meta-language to be a "real world" one that's statically typed and functional (Haskell and flavors of ML would be great, Idris is probably fine, Agda is borderline).

The main example of something like this that I've found is these notes by David Christiansen, which satisfies all my desiderata except that they're in Racket, which is not statically typed. But there's also a Haskell version, which may be what I end up using. However, I'm curious whether there are other options to compare with. In particular, has anyone written something like this in a flavor of ML?

Answer 1

Daniel Gratzer has written two tutorial implementations of normalization by evaluation in OCaml:

1. https://github.com/jozefg/nbe-for-mltt: plain MLTT with universes
2. https://github.com/jozefg/blott: a more complex type theory with an idempotent comonadic modality, based on our paper with Lars Birkedal from ICFP 2019

Both of these are based on Andreas Abel's version of NbE.

I have also written a tutorial implementation of type theory, which includes something roughly like NbE, here: https://github.com/jonsterling/dreamtt. Caveat is that my code may have bugs, as I have not executed it even once.

Answer 2

Does code in paper format count? In which case I would throw in

1. Danvy, Keller, and Puech's Typeful Normalization by Evaluation

You get an intro to deep vs. shallow, an analogy with printf, and an advanced example for an effectful setup (stlc + call/cc), all in OCaml.

As for a more classic setup in a dependently typed host language, I'm always fond of

2. Catarina Coquand's A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions

You get the whole story, including how to build the logical relations that make it possible to prove the normalisation function sounds & complete wrt a small step operational semantics.

3. Thierry Coquand and Dybjer's Intuitionistic Model Constructions and Normalization Proofs

It's really eye-opening on the model-construction aspect underlying the process, and suggests glueing as a way to overcome some mismatches between the object & meta languages (here glueing allows you to extract normal forms for the SKI calculus).