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?