Why dependent types matter (in Haskell)

A year ago I published Agda code for “Why dependent types matter” paper by Thorsten Altenkirch, Conor McBride and James McKinna. Now I rewrote that code in Haskell. This work is similar to my recent conversion of weight-biased leftist heaps from Agda to Haskell so I won’t go into technical details. As usual you can view the code on Github.

Staypressed theme by Themocracy