Is Haskell a dependently typed programming language? Should it be? The Glasgow Haskell Compailer's many type-system features, such as Generalized Algebraic Datatypes (GADTs), datatype promotion, multiparameter type classes, and type families, give programmers the ability to encode domain-specific invariants in their types. Clever Haskell programmers have used these features to enhance the reasoning capabilities of static type checking. But really, how far have we come? Could we do more?
In this talk, I will discuss dependently typed programming in Haskell, through examples, analysis and comparisons with modern full-spectrum dependently typed languages, such as Coq, Agda and Idris. What sorts of dependently typed programming can be done in Haskell now? What could GHC learn from these languages? Conversely, what lessons can GHC offer in return?
- Demonstrate the expressiveness of GHC's type system
- Functional programmers
Stephanie Weirich has been a functional programmer since 1993 and a Penn faculty member since 2002. She's crazy about types.