Type Systems - The Good, Bad and Ugly
summary
The claim "not all type systems are good" gets unpacked into a concrete comparison framework: an informal hierarchy and the Lambda Cube framework, tradeoffs like type inference vs. explicit types, and language-level features that make types usable. Expect worked examples — dependent types with a vector-size example that fails to compile if sizes mismatch, a monstrous Java tic-tac-toe signature as a cautionary artifact, notes on pattern matching, product types, parametric polymorphism, and the pragmatic verdict that Idris-style dependent typing is promising but not yet production-ready.
AI-written summary · about
chapters (36)
- 0:00Intro
- 1:53The Goal
- 2:22Original Thought
- 2:55People Lack Knowledge
- 4:01Pauls Quote
- 4:22Amandas Quote
- 5:41Disclaimer
- 5:54Theres still facts
- 6:06We will be fair
- 6:22So lets dive right in
- 6:58Type is a theorem
- 7:49The function type
- 9:55Pattern matching
- 10:53Product types
- 11:53Dependent types
- 13:45Parametric polymorphism
- 15:13Extensibility
- 15:56Intuition
- 16:16Bad Type System
- 18:39Structural Type
- 20:29Ugly Type
- 21:44Type
- 23:48Tim Sweeney
- 27:59Type Inference
- 29:27Cost of Proof
- 29:48Popularity
- 30:27Not helpful
- 30:57Culture
- 31:35Type Functional Languages
- 32:10Type Theory
- 32:50Informal Hierarchy
- 33:33Basic correctness
- 33:57Xpassivity
- 34:24Dependent Type World
- 35:05Lambda Cube
- 36:04Director Notes
