Making a Type Difference: Subtraction on Intersection Types as Generalized Recor...
summary
Defines a general type difference operator that extends record restriction to intersection, function and other types, gives an algorithm (deterministic) driven by subtyping and disjointness, and proves soundness and completeness of the specification. Implements the design by elaboration into disjoint intersection types plus a merge operator, encodes record ops (remove, rename, override) in a prototype language CP / A5-, and ships mechanized proofs in Coq and a working implementation.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:46Brief Overview of Intersection Types
- 4:12Motivation
- 6:04Related Works
- 7:03Limitations
- 8:32Contributions
- 9:27Deriving Type Difference
- 13:34Properties
- 15:55Conclusions and Future Work
- 17:59Language definitions and examples
related talks
20mImperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)
15mLiberating Merges via Apartness and Guarded Subtyping
15mResolution as Intersection Subtyping via Modus Ponens
28mTyping Records, Maps, and Structs
30mOn Distributive Subtyping with Finitary and Infinitary Unions and Intersections
15mPolymorphic Records for Dynamic Languages
48mA History of Subtyping
21mPolymorphic Type Inference for Dynamic Languages