I found this awesome paper “A tutorial implementation of a dependently typed lambda calculus“, by LĂ¶h, A., C. McBride, W. Swierstra and I decided to give it a go.

I read the paper a few times. The first time when I did it, it was just skimming through, copying and pasting the code as I go. Then, after doing the examples and playing with them for a bit, I read it again thoroughly to try to understand the mathematical definitions and the corresponding Haskell definitions and how they map to each other.

As I was implementing the code, I made sure to make a Git tag of every chapter implementation. This made it easier to match code to its mathematical definitions in the paper for the corresponding chapter.

Besides my interest in dependent types, I also noted this learning process was interesting, thus this blog post đź™‚

Even though papers take some time to read and digest, I highly recommend this paper to anyone interested in diving deeper into dependent types.

You can check the source code at https://github.com/bor0/lambdapi.

Bonus: Had some fun implementing TAPL exercise 3.2.4 in literate Haskell here.