Publications:Tagless Staged Interpreters for Typed Languages

Revision as of 05:44, 26 June 2014 by Slawek (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Tagless Staged Interpreters for Typed Languages
Author Emir Pasalic and Walid Taha and Tim Sheard
Year 2002
PublicationType Conference Paper
Conference ICFP'02. International Conference on Functional Programming
Diva url
Abstract 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 animplementation that is both readable and efficient. In an untypedsetting, staging an interpreter “removes a complete layer of interpretive overhead”, just like partial evaluation. In a typed settinghowever, Hindley-Milner type systems do not allow us to exploittyping 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 experiencewith the issues that arise in writing such an interpreter and in designing such a language.To demonstrate the soundness of combining staging and dependent types in a general sense, we formalize our language (calledMeta-D) and prove its type safety. To formalize Meta-D, we extendShao, Saha, Trifonov and Papaspyrou’s λH language to a multilevel setting. Building on λH allows us to demonstrate type safetyin a setting where the type language contains all the calculus of inductive constructions, but without having to repeat the work neededfor establishing the soundness of that system.