14
$\begingroup$

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?

$\endgroup$
3

2 Answers 2

12
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ To complement these implementations (which I found useful when learning) I also highly recommend checking out github.com/AndrasKovacs/elaboration-zoo, which also has some implementations of NbE. $\endgroup$
    – brendanzab
    Mar 25 at 7:57
  • $\begingroup$ Oh yes, this and several other projects of Andras are an excellent resource! $\endgroup$ Mar 25 at 8:35
3
$\begingroup$

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

  1. 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.

  1. 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).

$\endgroup$
1
  • $\begingroup$ If I'd have to type the code out into my editor manually in order to edit it and run it, then no it doesn't count. $\endgroup$ Mar 23 at 15:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.