Disjoint intersection types

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programming languages, as the semantics of the programming language becomes implementation-dependent. This paper presents λ-i: A coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of λ-i, with three variants of disjointness. In the simplest variant, which does not allow ĝŠ Currency sign types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce ĝŠ Currency sign types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with ĝŠ Currency sign types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants. © 2016 ACM.