Episode 14 - Richard Eisenberg on Dependent Types in Haskell
The Haskell Cast · [email protected]
June 14, 20171h 5m
Audio is streamed directly from the publisher (s3.amazonaws.com) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.
Show Notes
- 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