Episode 14 - Richard Eisenberg on Dependent Types in Haskell

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