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