Dependent Types with David Christiansen - Functional Futures

In this month’s episode of Functional Futures, our guest is David Christiansen, the executive director of the Haskell Foundation, a contributor to a number of dependently typed languages, and a dependent type advocate that has managed to introduce many people to the topic today through his work, talks, and texts.
In the episode, we cover topics such as dependent types, theorem proving, metaprogramming, and many more. We also discuss the book David co-authored with Daniel P. Friedman, The Little Typer, and his current work in progress: Functional Programming in Lean.
Get FP merch that doesn't suck. 👇
shop.serokell.io/
David's books:
The Little Types - mitpress.mit.edu/978026253643...
Functional Programming in Lean - leanprover.github.io/function...
Follow on social media:
/ d_christiansen
/ serokell
Learn more about us:
serokell.io/
Transcript of the episode:
serokell.io/blog/dependent-ty...
0:00 Intro
1:08 What are dependent types?
4:47 Intermediate example of dependent types
9:43 How to sell dependent types to customers
14:15 Servant
18:00 Ergonomics of dependent types in Haskell
27:14 Will Haskell have dependent types?
33:40 The Little Typer
44:02 Proof objects
45:20 History of dependently typed languages
48:50 Where proof objects come into play
55:11 Idris
1:01:25 Metaprogramming
1:04:45 Difference between type inference in Haskell and Lean
1:08:26 Lean
1:10:32 David's Lean book
1:17:34 Costs of dependent types
1:24:24 Recursive functions in Lean
1:26:22 How do you write a web server in dependently typed language?
1:31:14 Type universes in Lean
1:39:44 Typeclasses in Lean
1:49:28 Are there optics in Lean?
1:51:20 Tactics in theorem proving
1:56:06 Sort in Lean
1:59:30 Haskell Foundation

[@neilbedwell7763]

Thanks so much for this interview/conversation. Another piece of the puzzle for all

[@tanchienhao]

Looking forward to the lean4 book!

[@shutterrecoil]

type addicts about dependent types ;)

[@neilbedwell7763]

Are tactics to proof objects the same as thereoms to axioms?