Types are like the Weather, Type Systems are like Weathermen
summary
Argues that types are predictions and that adding them to an untyped ecosystem requires incremental typing, a boundary mechanism and runtime checks; demonstrates Type Racket tooling, occurrence typing, and module contracts that act as contracts as proxy wrappers to blame mismatches; reports surprising codebase numbers like ~500,000 lines of legacy code and personal libraries of ~20,000–25,000 lines; warns that higher‑order contracts allocate and can hurt performance, and that gradual typing must balance soundness, ergonomics and runtime cost.
AI-written summary · about
chapters (7)
- 0:00Start
- 4:20Notions of Types
- 18:11How Useful Is It To Have One Type
- 26:56Type Inference
- 29:16How Should Adding Types to an Untyped Language Work
- 37:29Incrementality
- 38:39What Does It Mean To Have a Module
related talks
45mTDD, as in Type-Directed Development
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
31mTotal Type Classes
41mThe Dialectics of Type-Level Programming
46mThe Calculated Typer (Functional Pearl)
54mImplementing Modern Types in C#
52mType Theory and its Meaning Explanations
42mProgramming with Math