
TL;DR
This paper introduces a foundational approach for compiling unrestricted intersection and union types in programming languages, using an elaboration system with a Forsythe-like merge to preserve type safety during evaluation.
Contribution
It presents a novel elaboration type system that supports unrestricted intersection and union types, enabling encoding of diverse language features with a type-preserving evaluation strategy.
Findings
Prototype implementation demonstrates practical applications
Elaboration system supports encoding of records and operator overloading
Type-preserving evaluation aligns with source program semantics
Abstract
Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume many different features. In modern type systems, parametric polymorphism is fundamental, but intersection polymorphism has gained little traction in programming languages. Most practical intersection type systems have supported only refinement intersections, which increase the expressiveness of types (more precise properties can be checked) without altering the expressiveness of terms; refinement intersections can simply be erased during compilation. In contrast, unrestricted intersections increase the expressiveness of terms, and can be used to encode diverse language features, promising an economy of both theory and…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
