Resolution as Intersection Subtyping via Modus Ponens
summary
Integrates resolution into coercive subtyping with intersection types by adding a modus ponens rule that, when a context type is both a function and its domain, yields the codomain via a coercion; implements merges as tuples and intersections as products so projections realize coercions; enforces coherence with a disjointness restriction on merges; proves a sound, complete, terminating subtyping algorithm (with loop detection), gives a conditional coherence proof, and ships a Haskell prototype.
AI-written summary · about
chapters (6)
- 0:00Start
- 3:20urch of Intersection Types
- 3:45Intersection Types and
- 7:31First-class Implicit Contexts
- 10:14Coherence
- 11:02Disjoint Merges
related talks
20mImperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)
15mLiberating Merges via Apartness and Guarded Subtyping
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...
21mPolymorphic Type Inference for Dynamic Languages
24mDecoupling Resolution from Type Inference
30mOn Distributive Subtyping with Finitary and Infinitary Unions and Intersections
15mThe Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Ma...
48mA History of Subtyping