Depending on Types - Stephanie Weirich

Stephanie Weirich discusses dependently typed programming in Haskell and compares its type system features with languages like Coq, Agda, and Idris.

Slides and more info: codemesh.io/codemesh2015/stephanie-weirich 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? Talk objectives: - Demonstrate the expressiveness of GHC's type system Target audience: - Functional programmers About Stephanie Stephanie Weirich has been a functional programmer since 1993 and a Penn faculty member since 2002. She's crazy about types.