Dependently Typed Lambda Calculus in Haskell
source link: https://www.tuicool.com/articles/hit/7ZjAvi7
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
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 .
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK