Bidirectional Higher-Rank Polymorphism with Intersection and Union Types
summary
Presents FIU, a bidirectional type system combining higher‑rank polymorphism with intersection and union types, and proves a sound, complete, decidable algorithm for a practical fragment. Formal development and proofs are formalized in Coq, with a prototype implementation available and artifacts released. Shows how explicit type application, syntactic well‑formedness checks, and a worklist/constraint solver interact, and explores extensions for records and relaxed monotype instantiation that increase expressiveness while trading some completeness.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:27Higher-rank polymorphism
- 1:54Intersection and union types
- 3:20Type inference
- 6:09FIU system overview
- 7:54Quantifier order challenges
- 9:19Subtyping rules changes
- 10:47Intersection/union subtyping
- 12:14Bidirectional typing rules
- 13:18Formalization in Rocq
- 14:42Proof structure
- 15:46Design choices
- 16:08Contributions summary
- 16:33Q&A
related talks
18mBidirectional Typing for Erlang
20mImperative Compositional Programming: Type Sound Distributive Intersection Subtyping(…)
32mMLstruct: Principal Type Inference in a Boolean Algebra of Structural Types
41mPolymorphism Unbound
49mThe Trouble With Types
22mTransformation Function Called Higher-Order
30mConstraint Typing with Boolean Algebra
11mThe Secrets of Polymorphic Variants