Episode 14 - Richard Eisenberg on Dependent Types in Haskell
Jun 14, 2017•1 hr 6 min
Listen to this episode in Metacast mobile app
Don't just listen to podcasts. Learn from them with transcripts, summaries, and chapters for every episode. Skim, search, and bookmark insights. Learn more
Episode description
- 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
For the best experience, listen in Metacast app for iOS or Android
Open in Metacast