"Dependent Types in Haskell" by Stephanie Weirich

What has dependent type theory done for Haskell? Over the past ten years, the Glasgow Haskell compiler (GHC) has adopted many type system features inspired by dependent type theory. In this talk, I will discuss the influence of dependent types on the design of GHC and on the practice of Haskell programmers. In particular, I will walk through an extended example and use it to analyze what it means to program with with dependent types in Haskell. Throughout, I will will discuss what we have learned from this experiment in language design: what works now, what doesn't work yet, and what surprised us along the way.
Stephanie Weirich
UNIVERSITY OF PENNSYLVANIA
Stephanie Weirich is a Professor of Computer and Information Science at the University of Pennsylvania, having received tenure in 2008 and the rank of full professor in 2015. She received her B.A. in Computer Science from Rice University and her Ph.D. from Cornell University. She has published broadly in the areas of functional programming, type systems, machine-assisted theorem proving and dependent types. During the past ten years, she and her students have made significant contributions to the design of the Glasgow Haskell Compiler and its type system. Dr. Weirich has served as the program chair of the The 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010 and the 2009 Haskell Symposium and is also an editor of the Journal of Functional Programming. She has given invited talks at many venues, including ICFP, FLOPS, RDP, LFMTP, OPLSS, and PLMW. Her recent awards include a 2016 Microsoft Outstanding Collaborator award, and the 2016 Most Influential ICFP Paper award (for 2006) for the paper "Simple unification-based type inference for GADTs" with her co-authors Simon Peyton Jones, Dimitrios Vytiniotis and Geoffrey Washburn, and the 2016 ACM SIGPLAN Robin Milner Young Researcher Award.

[@alexcoventry7580]

Thanks, this was a terrific introduction, and the concrete example clarified things a great deal.

[@marksaving756]

Excellent talk. I learned Haskell after learning Martin-Lof type theory and look forward to writing Π in my programs.

[@FourTetTrack]

I loved the talk, thanks a lot Dr Weirich!!!

[@johnmiller8884]

Thank you for the excellent talk. I appreciate the explanation of the use case for dependent types which are so often described win formal computer science terms without ever giving a motivation for their value.
Seeing now why dependent types might be useful, is there a good resource that describes the skills and techniques needed to write something like the library in your example?

[@xtty7644]

Benjamin Pierce's book Advanced Topics in Types and Programming Languages gives a pretty good explanation on the theoretical background of dependent typing. The book is an extension of the ideas developed in Pierce's previous book, Types and Programming Languages, so you might want to pick that one up first. This should be enough to understand how dependent types work. The rest is just advanced GHC features.

[@lordquaggan]

Wow, having the equivalence proofs just be superclass constraints (32:30) is a really neat idea, which I, for some reason, never thought of. I always end up writing functions that match on singletons and return `:~:` when I need to prove properties like that, which is obviously way more painful.

[@centril]

A truly awesome and detailed talk!

[@nilp0inter2]

Awesome talk!

[@shutterrecoil]

the most representative DT example is at 26:00

[@tricky778]

At 32:00, is this the same as saying that Repeat is a monad at the typeclass level? Is there any utility in casting the solution in that light? Does anyone know the paths that line of reasoning has taken people?

[@mskiptr]

This talk is awesome!
That `~` relation between types is not commutative, right? Like in 34:00, repeating ≥1 times is also ≥0, but we couldn't write it the other way around: `Repeat s` does not ~ `Merge s (Repeat s)`?

[@user-dn7qr7vs1h]

It is commutative.