Finally Tagless, Partially Evaluated Tagless Staged Interpreters for Simpler Typed Languages

The authors have built the first family of tagless interpretations for a higher-order typed object language in a typed Meta-Language (Haskell or ML) that require no dependent types, generalized algebraic data types, or post-processing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value CPS transformers. Their main idea is to encode HOAS using cogen functions rather than data constructors. Their representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Their encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck.