A Type-Preserving Compiler in Haskell
Louis-Julien Guillemette and Stefan Monnier
The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)
Victoria, British Columbia, Canada, September 22-24, 2008
There has been a lot of interest of late for programming languages that incorporate features from dependent type systems and proof assistants, in order to capture in the types important invariants of the program. This allows type-based program verification and is a promising compromise between plain old types and full blown Hoare logic proofs. The introduction of GADTs in GHC (and more recently type families) made such dependent typing available in an industry-quality implementation, making it possible to consider its use in large scale programs.
We have undertaken the construction of a complete compiler for System F, whose main property is that the GHC type checker verifies mechanically that each phase of the compiler properly preserves types. Our particular focus is on ``types rather than proofs'': reasonably few annotations that do not overwhelm the actual code.
We believe it should be possible to write such a type-preserving compiler with an amount of extra code comparable to what is necessary for typical typed intermediate languages, and with the advantage of static checking. This goal is already a reality for a simply typed language, and we show what extra work is still needed to handle polymorphism.
Conference Manager (V2.54.6)