00:29 What are dependent type systems?03:38 applying dependent types to industry07:30 writing dependently typed programs in Haskell today09:07 GADTs (Generalized Algebraic Data Types)11:01 the future of dependent types in GHC13:40 teaching dependent types18:03 learning dependent types20:20 a future style of Haskell programming with dependent types21:21 Servant and opaleye as an example of type-level features23:22 tool support for dependently typed programming24:06 simple applications of dependent types for linear algebra26:25 Are dependent types worth it?28:47 complex type system errors33:07 LiquidHaskell36:26 safe zero-cost coercions41:20 total vs type safe48:36 working on GHC’s type system51:09 using GHC extensions in the GHC source code53:00 road to Haskell55:37 teaching Haskell to students1:03:00 a hopeful future for reliable software through dependent types