Episode 14 - Richard Eisenberg on Dependent Types in Haskell The Haskell Cast

00:29 What are dependent type systems?
03:38 applying dependent types to industry
07:30 writing dependently typed programs in Haskell today
09:07 GADTs (Generalized Algebraic Data Types)
11:01 the future of dependent types in GHC
13:40 teaching dependent types
18:03 learning dependent types
20:20 a future style of Haskell programming with dependent types
21:21 Servant and opaleye as an example of type-level features
23:22 tool support for dependently typed programming
24:06 simple applications of dependent types for linear algebra
26:25 Are dependent types worth it?
28:47 complex type system errors
33:07 LiquidHaskell
36:26 safe zero-cost coercions
41:20 total vs type safe
48:36 working on GHC’s type system
51:09 using GHC extensions in the GHC source code
53:00 road to Haskell
55:37 teaching Haskell to students
1:03:00 a hopeful future for reliable software through dependent types