Keynote: Dependently-Typed Haskell
summary
Argues that Haskell already supports a useful form of dependent typing using GHC features and demonstrates it by encoding red‑black trees with checked invariants: implementations range from an unverified 12‑line version to an Agda‑style 49‑line encoding and a simpler 32‑line Haskell variant. Uses GADTs, datatype promotion plus type families and Singletons to track colors and black height; notes GHC differences (erasure, no totality check) and upcoming features like TypeInType and explicit type application that make these encodings practical and working.
AI-written summary · about
chapters (19)
- 0:00Intro
- 3:47Example: Red-black Trees
- 10:36Red-black Trees in Agda (Licata)
- 13:48Red-black Trees in GHC
- 16:03Static enforcement
- 18:35How are Agda and Haskell different?
- 20:21Types are erased
- 21:58Split balance into two cases
- 23:28Decompose argument
- 24:06Specialize Color
- 26:32Programming with types (Agda)
- 29:50GHC version of Almost Tree
- 33:26Implementation of insert
- 34:38Difference: Totality
- 35:12Not proving things is simpler
- 37:41Dependently-Typed Haskell
- 40:14Ivory: Safe bit-level programming
- 41:44Length-preserving Convolution
- 44:44Safe Database Access
related talks
49mMaking sense of the Haskell type system
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
01h 04mHaskell - A Peek Inside the Ivory Tower
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
24mReasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs
23mPartial Type Constructors in Practice
04h 08mHaskell Beginners' Track
01h 22mHaskell for Everyday Programmers