Parametricity The Essence of Information Hiding
summary
Claims that parametricity lets types enforce invariants by excluding implementation possibilities and shows how to prove behavior from signatures. Covers universal and existential quantification, uses Haskell code (but maps ideas to unityped languages), refactors a broken list-based implementation into one with a functor constraint for firsts, demonstrates doctest laws to pin down reverse, and points out unsafe primitives like head/bottom that break reasoning. Practical and example-driven: concrete rewrites and failure modes are shown.
AI-written summary · about
chapters (7)
- 0:00Intro
- 1:37About This Talk
- 11:26Simple Examples
- 14:03Code Reuse
- 17:13Typeclasses
- 22:04Pitfalls
- 26:46Existential Solution
related talks
01h 12mTruth about Types
01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in Haskell
40mGuarded Impredicativity
11mThe Secrets of Polymorphic Variants
50mPinafore: Strongly Typed Information Representation
49mThe Trouble With Types
55mKeynote: Propositions as Types
01h 03mHow to use Phantom Types and Existential Types in Production