A type-preserving closure conversion in haskell

The use of typed intermediate languages can significantly increase the reliability of a compiler. By type-checking the code produced at each transformation stage, one can identify bugs in the compiler that would otherwise be much harder to find. Also it guarantees that any property that was enforced by the source-level type-system is holds also for the generated code. Recently, several people have tried to push this effort a bit further by verifying formally that the compiler indeed preserves typing. This is usually done with proof assistants or experimental languages. Instead, we decided to use Haskell, to see how far we can go with a more mainstream system, supported by robust compilers and plentiful libraries. This article presents one part of our type preserving compiler, namely the closure conversion and its associated hoisting phase, where we use GADTs to let Haskell's type checker verify the we obey the object language's typing rules and that we correctly preserve typ...

• Type: Conference
• Year: 2007
• Where: HASKELL
• Authors: Louis-Julien Guillemette, Stefan Monnier
• Keywords: Bruijn Representation, Compiler, HASKELL 2007, Programming Languages, Typed Intermediate Languages