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

Om Podcasten

Listen to regular interviews with the Haskell community. The podcast covers news, libraries, and whatever other topics we wander onto with our guests.