Tagless staged interpreters for typed languages

Multi-stage programming languages provide a convenient notation for explicitly staging programs. Staging a definitional interpreter for a domain specific language is one way of deriving an implementation that is both readable and efficient. In an untyped setting, staging an interpreter "removes a complete layer of interpretive overhead", just like partial evaluation. In a typed setting however, Hindley-Milner type systems do not allow us to exploit typing information in the language being interpreted. In practice, this can mean a slowdown cost by a factor of three or more. Previously, both type specialization and tag elimination were applied to this problem. In this paper we propose an alternative approach, namely, expressing the definitional interpreter in a dependently typed programming language. We report on our experience with the issues that arise in writing such an interpreter and in designing such a language. To demonstrate the soundness of combining staging and depen...

• Type: Conference
• Year: 2002
• Where: ICFP
• Authors: Emir Pasalic, Walid Taha, Tim Sheard
• Keywords: Definitional Interpreter, ICFP 2002, Multi-stage Programming Languages, Programming Languages, Type Language