Unembedding domain-specific languages

Publication Information

Robert Atkey, Sam Lindley, and Jeremy Yallop. Unembedding domain-specific languages. In Proceedings of the 2nd ACM SIGPLAN symposium on Haskell, Haskell '09, 37-48. ACM, 2009.
DOI: 10.1145/1596638.1596644

Abstract

Higher-order abstract syntax provides a convenient way of embedding domain-specific languages, but is awkward to analyse and manipulate directly.

We explore the boundaries of higher-order abstract syntax. Our key tool is the unembedding of embedded terms as de Bruijn terms, enabling intensional analysis. As part of our solution we present techniques for separating the definition of an embedded program from its interpretation, giving modular extensions of the embedded language, and different ways to encode the types of the embedded language.

Additional Information

This work builds on the result of a TLCA 2009 paper where I used a model of System F with Kripke relational parametricity to show that the higher-order abstract syntax (HOAS) encoding is adequate.

The code is available in the file unembedding.hs. It has been tested with GHC 7.6.3, but nothing newer than that. Newer features of GHC, such as DataKinds and closed type families are almost certainly better ways of accomplishing some of the same type level computation that we did in the paper.