Dependent Types in Haskell: Present and Future
New York Haskell Users Group, October 24, 2014
Dependent Types in Haskell by Richard Eisenberg
Why you want them,
How to use them today, and
What they will look like tomorrow
This talk will introduce the concept of dependent types through simple, practical examples, all written in Haskell and compilable in GHC 7.8. Then, it will dive into the details of how we can "fake" the encoding of dependent types today. Finally, it will show some plans for a new language extension, which Richard is hard at work on, that will integrate proper dependent types right into GHC. This extension, whose implementation is under active development, will bake Pi-types right into the compiler, allowing full dependently-typed programming in the style of Idris, Agda, or Coq.