Liberating Merges via Apartness and Guarded Subtyping
summary
Introduces type apartness plus a strengthened guarded subtyping that lets merges overlap yet remain deterministic, enabling function and return-type overloading, extensible records, and nested composition in one calculus. Provides an algorithm, source-and-target encodings, and machine-checked proofs in Coq; the paper claims full determinism and automatic conflict resolution where disjointness previously rejected programs. Evaluation includes formal soundness proofs and reusable artifacts reproducing the results.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:03Intersection types and merge
- 3:09Disjoint intersections limits
- 5:16Conflict resolution in types
- 7:24Introducing apartness
- 9:09Guarded subtyping for safety
- 10:57Apartness theoretical effects
- 12:24Q&A
related talks
19mMaking a Type Difference: Subtraction on Intersection Types as Generalized Recor...
15mResolution as Intersection Subtyping via Modus Ponens
20mImperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
14mA dependently typed calculus with pattern matching and erasure inference
19mMutually Iso-Recursive Subtyping
21mPolymorphic Type Inference for Dynamic Languages
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml