Depending on Types

on YouTube ↗45m

" summary

Argues that Haskell already supports a lot of dependently typed programming by using GADTs, datatype promotion and type families to encode invariants; demonstrates with a red‑black tree implementation that adds precise types for red-black trees, `hidden`/`almost` tree forms, `balance`/`insert`, and singleton types to keep runtime values. Notes some patterns cannot be promoted yet, presents a GHC branch (Eisenberg) that lifts promotion limits, uses a singleton library as a workaround, and contrasts weaker totality guarantees versus Agda/Idris/Coq.

AI-written summary · about

" chapters (17)

1. 0:00Introduction
2. 1:16Overview
3. 1:47Running Example
4. 3:48Red Black Trees
5. 6:34Rebalancing
6. 8:43Type checker
7. 11:58Dependent types
8. 13:49RBT type
9. 15:56GHC type
10. 17:37Differences between types
11. 18:59Type promotion
12. 19:30Erased types
13. 26:15Hidden trees
14. 30:30Type family
15. 36:07Not proving is simpler
16. 38:31Whats next
17. 41:06Why not Haskell

" related talks

• 39mDependent Types in HaskellStephanie Weirich · Strange Loop 2017
• 01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in HaskellThomas Dietert · LambdaConf 2019
• 49mThe Trouble With TypesMartin Odersky · Strange Loop 2013
• 48mEnhancing your Haskell with Dependently Typed ProgrammingJustin Le · LambdaConf 2017
• 33mStatically Typed InterpretersChristopher Hockenbrocht · LambdaConf 2017
• 35mGADTs and You; Writing Safer Code Using GADTsNathan Holland · LambdaConf 2019
• 38mType Systems - The Good, Bad and UglyPaul Snively, Amanda Laucher · Strange Loop 2014
• 56mWrite You Some Proofs for Great GoodRobert Peszek · LambdaConf 2019