- Abstracting over the final interpreter in IntroHOIF.hs
- Like GADT-based, but in lower-case
- Like ExpSYM, but repr is of kind * -> * -> *
- The types read like the rules of minimal logic
- Type system of simply-typed lambda-calculus in Haskell98!
- ``a way to write a typed fold function over a typed term.''
- Sample terms and their inferred types
- td2a = app (int 1) (int 2)
- Embedding all and only typed terms of the object language
- in the typed metalanguage
- Typed and tagless evaluator
- object term ==> metalanguage value
- R is not a tag!
- R is a meta-circular interpreter
- R never gets stuck: no variant types, no pattern-match failure
- Well-typed programs indeed don't go wrong!
- R is total
- The instance R is a constructive proof of type soundness
- R _looks_ like a reader monad (but h varies)
- Essentially, Haskell98! * Typed tagless-final interpreters for simply-typed lambda-calculus * de Bruijn indices based on the code accompanying the paper by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan