Episode 14 - Richard Eisenberg on Dependent Types in Haskell
Recorded: 2017-06-01, Published: 2017-06-14
- 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
Links from the show:
- http://cs.brynmawr.edu/~rae/
- http://cs.brynmawr.edu/~rae/courses/17spring380/syllabus.html
- https://github.com/goldfirere/thesis
- https://haskell-servant.github.io/
- https://hackage.haskell.org/package/opaleye
- https://hackage.haskell.org/package/hmatrix
- https://ucsd-progsys.github.io/liquidhaskell-blog/
- http://www.seas.upenn.edu/~sweirich/papers/coercible-JFP.pdf
- https://www.youtube.com/watch?v=6snteFntvjM
The music used in the show is Ecstatic Wave by Jens Killstofte.