u/mightybytein r/haskell • Recommends
Dependent Types in Haskell: Present and Future (NY Haskell Meetup Video)
0:00 / 0:00
Dependent Types in Haskell: Present and Future
NYC Haskell User's Group
1.7K subscribers • 19 videos on Hallway
- Recommended by 2 people: 1 on Lobsters and 1 in engineering communities.
- Presented by Richard Eisenberg
Advanced. Deep dive for people who know the field.
2.2K views11 years ago2 recommendations
Programming languagesComputer scienceHaskellLanguage design and type systemsComputation and complexity
Richard Eisenberg explains how to emulate dependent types in Haskell today and outlines the future plans for proper dependent types in GHC.
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.