Why Dependent Types Matter
Conor McBride, James McKinna, Thorsten Altenkirch
We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system using refinements of a well known program, merge sort, as a running example. We discuss the relationship to other proposals to introduce aspects of dependent types into functional programming languages and sketch some topics for further work in this area.
via The Types Forum.