Making sense of the Haskell type system
summary
Traceable examples show Haskell evolving from Haskell 98 to modern code by using GADTs to encode sized lists, type families for compile‑time arithmetic (one plus one reduces to two), and singletons plus Template Haskell to fake dependent types so functions like replicate and length carry and check sizes at compile time. The talk stresses limits: type families are rewrite axioms (can leave junk like Bool unsimplified), type‑level computation can be slow, and totality/termination requirements motivate Idris/Agda for true dependent typing.
AI-written summary · about
chapters (12)
- 0:00Start
- 0:15MODERN HASKELL Making sense of the Type System
- 3:33TYPES CLASSIFY TERMS
- 4:33TYPES NOT 1ST CLASS
- 20:50TYPE FUNCTIONS FAMILIES
- 27:42STILL NON-DEPENDENT
- 33:28FAKING IT GETS MESSY...
- 34:44Increased Precision
- 35:31Flexible Type Signatures
- 37:07FULLY DEPENDENTLY TYPED
- 38:28TOTALITY
- 39:55PROGRAM - PROOF
related talks
59mKeynote: Dependently-Typed Haskell
01h 07mBuilding a Dependently Typed Language in Haskell Part 1
01h 22mHaskell for Everyday Programmers
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
04h 08mHaskell Beginners' Track
23mPartial Type Constructors in Practice
01h 04mHaskell - A Peek Inside the Ivory Tower
01h 35mSecrets of the GHC Typechecker in 100 Type Declarations