Applicative Intersection Types

on YouTube ↗30m

" summary

Two calculi for intersection types with an explicit merge operator: the first admits an unrestricted merge, proves type soundness but yields non-deterministic semantics; the second adds a disjointness restriction to regain determinism at the cost of rejecting some overloadings. Key technical contributions are an applicative subtyping relation and a matching applicative dispatching dynamic semantics that infer result types for applications and projections. Both calculi and proofs are formalized in Coq and a Racket interpreter exists.

AI-written summary · about

" chapters (22)

1. 0:00Intro
2. 0:45Intersection Types
3. 2:09Merge Operator
4. 3:09Extensible Records
5. 3:53Record Projection
6. 5:28Overloaded Application
7. 6:05Return type Overloading
8. 7:20Nested Composition?
9. 9:59Challenges in Type Inference
10. 11:27Challenges in Dynamic Semantics
11. 11:52Distributivity Breaks the Assumptions
12. 13:00Re-interpret Subtyping
13. 15:23Examples of Applicative Subtyping
14. 16:18Composition Operators
15. 17:41Examples (applying nested composition semantics)
16. 18:42Metatheory
17. 20:18Operational Semantics
18. 20:36Applicative Dispatching
19. 21:47Type Soundness
20. 21:59More in the paper
21. 23:06Overloaded Functions
22. 28:34Goodness of Nested Composition