1 Department of Computer Science, Faculty of Science, Aarhus University, Aarhus University2 unknown
Recent work on embedding object languages into Haskell use "phantom types" (i.e., parameterized types whose parameter does not occur on the right-hand side of the type definition) to ensure that the embedded object-language terms are simply typed. But is it a safe assumption that only simply-typed terms can be represented in Haskell using phantom types? And conversely, can all simply-typed terms be represented in Haskell under the restrictions imposed by phantom types? In this article we investigate the conditions under which these assumptions are true: We show that these questions can be answered affirmatively for an idealized Haskell-like language and discuss to which extent Haskell can be used as a meta-language.
B R I C S Report Series, 2002, Issue RS-02-34
Embedded languages; Haskell; Standard ML; completness; high-order abstract syntax; phantom types; type safety; type soundness