SImply Easy! An Implementation of a Dependantly Typed Lambda Calculus

I like to mention papers that I've enjoyed on this blog, and I thought "Simply Easy! An Implementation of a Dependantly Typed Lambda Calculus" by Andres Loh, Conor McBride and Wouter Swierstra was a nice read. It makes use of De Bruijn Indices and Higher Order Abstract Syntax in an implementation of a Dependant lambda calculus in Haskell to show that its isn't so daunting or complex as one might expect. Its nice to see discussion of these techniques and to see how they simplify the implementation, and I appreciated that they took the time to discuss every line code. It was easy to read, assuming basic knowledge of each of the relevant subjects, and was successful in convincing me that a Dependant Type System is not black magic.

I definitely recommend this one.