Wadler's Blog

Lennart Augustsson posted a nifty description of a compiler from a simple expression language to LLVM that included a conversion from expressions represented as an ADT to expressions represented as a GADT. The ADT requires a separately implemented type checker, while the GADT piggybacks on Haskell's type system to ensure expressions are well typed. However, Lennart's expression language does not include lambda abstraction.

Based on Lennart's code, I implemented ADT and GADT versions of simply-typed lambda calculus with de Bruijn indices, integer constants, and addition, plus the conversion between them, without the distraction of compiling to LLVM. The code was cleaned and improved by Shayan Najd, and made publicly available via github. Thanks to Josef Svenningson for the pointer to Lennart's post.

Labels: Functional Programming, Haskell