| Abstract
|
<p>Multi-stage programming languages … <p>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.</p>ng the soundness of that system.</p>
|
