DiscoverThe Haskell CastEpisode 14 - Richard Eisenberg on Dependent Types in Haskell
Episode 14 - Richard Eisenberg on Dependent Types in Haskell

Episode 14 - Richard Eisenberg on Dependent Types in Haskell

Update: 2017-06-14
Share

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

Comments 
loading
00:00
00:00
1.0x

0.5x

0.8x

1.0x

1.25x

1.5x

2.0x

3.0x

Sleep Timer

Off

End of Episode

5 Minutes

10 Minutes

15 Minutes

30 Minutes

45 Minutes

60 Minutes

120 Minutes

Episode 14 - Richard Eisenberg on Dependent Types in Haskell

Episode 14 - Richard Eisenberg on Dependent Types in Haskell

haskellcast@haskellcast.com