KnowledgeBase » SEMINAR » ID = 665

Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

by Chung-chieh Shan
2011-2012

Chung-chieh Shan (joint work with Jacques Carette and Oleg Kiselyov)
Slides available: PDF

This "functional necklace" aims to change how you try to write your next interpreter: by deforesting the object language, to exhibit more static safety in a simpler type system.  We show how easy it is to build a family of interpreters for a typed object language (such as the simply typed lambda calculus) in a typed metalanguage (such as Haskell or ML) that preserve types without using dependent types, generalized algebraic data types, or postprocessing to eliminate tags.  The interpreters include an evaluator, a compiler, a partial evaluator, and call-by-name and call-by-value CPS transformers.
Our main idea is to encode abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but in an arbitrary algebra. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformation. Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck.