On Distributive Subtyping with Finitary and Infinitary Unions and Intersections
summary
Argues that whether intersections and unions distribute over function and constructed types hinges on Church vs Curry divide: languages with internal typing (Scala, full distributivity) can justify distributing intersections across arrows and constructors, while externally typed languages (TypeScript) cannot. Shows a core calculus where full distributivity enables principal type inference, but adding first‑class polymorphism breaks soundness of that rule. Surveys semantic subtyping (Cidius), MLsub and practical language tradeoffs, and reports MLScript opts for Curry style.
AI-written summary · about
chapters (8)
- 0:00Distributive subtyping intro
- 1:09Intersection and union types
- 3:58Distributivity over functions
- 11:44Formal background
- 18:50Infinitary unions/intersections
- 20:14Church vs Curry semantics
- 27:43Language design trade-offs
- 28:37Q&A
related talks
20mImperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)
21mPolymorphic Type Inference for Dynamic Languages
48mA History of Subtyping
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...
15mResolution as Intersection Subtyping via Modus Ponens
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
42mDOT: Scala Types from Theory to Practice
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)