Publications:Tagless Staged Interpreters for Typed Languages
From CERES
| Title | Tagless Staged Interpreters for Typed Languages |
|---|---|
| Author | Emir Pasalic and Walid Taha and Tim Sheard |
| Year | 2002 |
| PublicationType | Conference Paper |
| Journal | |
| HostPublication | |
| DOI | |
| Conference | ICFP'02. International Conference on Functional Programming |
| Diva url | http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:588280 |
| 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. |
