Typed tagless-final interpreters for PCF Higher-order abstract syntax based on the code accompanying the paper by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan
Documentation
class Symantics repr whereSource
The language is simply-typed lambda-calculus with fixpoint and constants. It is essentially PCF. The language is just expressive enough for the power function. We define the language by parts, to emphasize modularity. The core plus the fixpoint is the language described in the paper
Hongwei Xi, Chiyan Chen, Gang Chen Guarded Recursive Datatype Constructors, POPL2003
which is used to justify GADTs.
- Core language
Sample terms and their inferred types
Typed and tagless interpreter
type VarCounter = IntSource
- R is not a tag! It is a newtype The expression with unR _looks_ like tag introduction and elimination. But the function unR is *total*. There is no run-time error is possible at all -- and this fact is fully apparent to the compiler. Furthermore, at run-time, (R x) is indistinguishable from x * R is a meta-circular interpreter This is easier to see now. So, object-level addition is _truly_ the metalanguage addition. Needless to say, that is efficient. * R never gets stuck: no pattern-matching of any kind * R is total
- Another interpreter
- The crucial role of repr being a type constructor rather than just a type. It lets some information about object-term representation through (the type) while keeping the representation itself hidden.
- * Extensions of the language
- Multiplication