A History of Subtyping
summary
Traces the technical claim that subtyping is not just a typing convenience but changes computation: adding a subsumption rule breaks the usual beta-on-derivations pattern and forces new reduction rules that push and split subsumption so the beta rule can fire. Uses lambda calculus with records (student/person example), proves preservation still matters, and frames the difference as intrinsic vs extrinsic typing (Church vs Curry). Shows typed derivations themselves perform steps — calling this beta reduction on derivations — and points to real systems like Liquid Haskell and Haskell typeclass expansion.
AI-written summary · about
chapters (21)
- 0:00Introduction
- 1:04Meaning of subtyping
- 4:21Typing and Lambda calculus
- 9:56Operational semantics
- 13:16Alonzo Church interlude
- 15:22Records in Lambda calculus
- 18:16Simply typed Lambda calculus
- 24:15Type preservation theorem
- 26:25Church vs Curry typing
- 28:11Intrinsic vs extrinsic typing
- 31:04Reduction of typing derivations
- 33:16What is subtyping
- 36:32Simula and subclassing
- 37:33F-sub subtyping system
- 39:21Semantics of subtyping
- 40:26Subtyping rules
- 41:51Liskov substitution principle
- 42:57First CS PhD woman
- 44:03Subtyping impact on reduction
- 46:57Modern intrinsic vs extrinsic
- 47:59Key takeaways and conclusion
related talks
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
28mTyping Records, Maps, and Structs
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)
30mOn Distributive Subtyping with Finitary and Infinitary Unions and Intersections
19mMutually Iso-Recursive Subtyping
16mTowards Algebraic Subtyping for Extensible Records
15mPolymorphic Records for Dynamic Languages
13mRevisiting Iso-Recursive Subtyping