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.