Type-Safe Code Transformations in Haskell

8 years 12 months ago
Type-Safe Code Transformations in Haskell
The use of typed intermediate languages can significantly increase the reliability of a compiler. By typechecking the code produced at each transformation stage, one can identify bugs in the compiler that would otherwise be much harder to find. We propose to take the use of types in compilation a step further by verifying that the transformation itself is type correct, in the sense that it is impossible that it produces an ill typed term given a well typed term as input. our approach on higher-order abstract syntax (HOAS), a representation of programs where variables in the object language are represented by meta-variables. We use a representation that accounts for the object language’s type system using generalized algebraic data types (GADTs). In this way, the full binding and type structure of the object language is exposed to the host language’s type system. In this setting we encode a type preservation property of a CPS conversion in Haskell’s type system, using witnesses...
Louis-Julien Guillemette, Stefan Monnier
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Louis-Julien Guillemette, Stefan Monnier
Comments (0)