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 top types, two types are disjoint if
they do not share any common supertypes at all. The other two variants
introduce top 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 top
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.