Disjoint Polymorphism with Intersection and Union Types

Intersection and union types are advance programming features and are able to encode various classical programming constructs. The significance of intersection and union types is visible by the fact that these types are available in many modern programming languages including Scala, TypeScript and Ceylon. (Un-tagged) Union types are normally eliminated using a type-based switch construct. The branches of the switch construct may overlap thus resulting in an ambiguous semantics. Recently, a disjointness based approach so called 𝜆𝑢 has been proposed to deal with ambiguity in (un-tagged) union elimination. When studied with intersection types and parametric polymorphism, 𝜆𝑢 poses an un-intuitive ground type restriction on type variable bounds. This restriction reduces the expressiveness of the calculus. In this paper, we propose a novel disjointness algorithm based on union splittable types. The novel disjointness algorithm does not require ground type restriction on type variable bounds. Therefore, the resulting calculus is more expressive. We prove soundness and completeness of our disjointness algorithm (without parametric polymorphism) w.r.t disjointness specifications for monomorphic 𝜆𝑢. All the metatheory of this paper has been formalized in Coq theorem prover.