Disjoint Intersection Types
Bruno C. d. S. Oliveira

Zhiyuan Shi

João Alpuim

The University of Hong Kong{bruno,zyshi,alpuim}@cs.hku.hk

Abstract
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 toexpressions that evaluate to different values. The lack of coherenceis an important disadvantage for adoption of his core calculus in
implementations of programming languages, as the semantics ofthe programming language becomes implementation-dependent.
This paper presents λi : a coherent and type-safe calculus witha form of intersection types and a merge operator. Coherenceis achieved by ensuring that intersection types are disjoint andprograms 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 threevariants of disjointness. In the simplest variant, which does notallow > types, two types are disjoint if they do not share any
common supertypes at all. The other two variants introduce >types and refine the notion of disjointness to allow two types tobe disjoint when the only the set of common supertypes are toplike. The difference between the two variants with > types is on thedefinition of top-like types, which has an impact on which types areallowed 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.
Categories and Subject Descriptors D.3.2 [Language Classifications]: Applicative (functional) languages; F.3.3 [Studies of Program Constructs]: Functional constructs
General Terms Design, Languages, Theory
Keywords Intersection Types, Type System

1.

Introduction

Intersection types date back to Coppo et al. [9] and Pottinger [26]work. Early work was motivated by the applications of intersection types to characterize exactly all strongly normalizing lambda
terms. Since then various researchers [6, 12, 15, 17, 22, 24] havestarted looking at the application of intersection types for designing

new and more powerful type systems for programming languages.
Since Reynolds’ work on the Forsythe [28] programming language,
various other languages, including CDuce [4], Scala [20] and Stardust [13] have incorporated some notion of intersection types.
Recently Dunfield [14] showed the usefulness of type systems
with intersection types and a merge operator. The presence of amerge operator in a core calculus provides significant expressiveness, allowing encodings for many other language constructs assyntactic sugar. For example single-field records are encoded as
types with a label, and multi-field records are encoded as the concatenation of single-field records. Concatenation of records is expressed using intersection types at the type-level and the merge operator at the term level. Dunfield formalized a simply typed lambda
calculus with intersection types and a merge operator. He showed
how to give a semantics to the calculus by a type-directed translation to a simply typed lambda calculus extended with pairs. The
type-directed translation is elegant and type-safe.
While Dunfield’s calculus is type-safe, it lacks the property ofcoherence: different derivations for the same source expression canlead to target expressions that evaluate to different values. Dunfieldleft coherence as an open problem. 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. AlthoughDunfield mentioned the possibility of extending the type system toallow only disjoint intersection types, he did not formalize or further pursue this approach.
This paper presents λi : a type-safe and coherent core calculus with intersection types and a merge operator. Coherence isachieved 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 when only a certain set of types are common supertypes of
A and B. We investigate three different variants of λi , with threevariants of disjointness. The difference between the variants of disjointness is on what is the set of allowed common supertypes. To
avoid type ambiguity, which arises from the undecidability of typeassignment of intersection types [30], we use a variant of the calculus that allows type annotations. Without additional type annotations the same term can have multiple types, and consequently
different semantics depending on the type. The additional annotations enable a type system based on bidirectional type-checking
techniques [16, 25], that ensures that every term has a unique type,eliminating an additional source of ambiguity in the semantics.
In the simplest variant of λi , which does not allow > types, twotypes A and B are disjoint (A ∗ B)1 if there is no type C such thatboth A and B are subtypes of C. With this definition of disjointness
we present a formal specification of a type system that prevents intersection types that are not disjoint. However, the formal definition
1 The notation A ∗ B is inspired by the separating conjunction construct inReynolds’ separation logic [29].

of disjointness does not lend itself directly to an algorithmic implementation. Therefore, we also present an algorithmic specification
to determine whether two types are disjoint. Moreover, this specification is shown to be sound and complete with respect to the formal
definition of disjointness.
The other two variants of λi introduce > types and refine thenotion of disjointness. The main problem of adding > types into λiis that now every two types have at least one common supertype.
Therefore, defining disjointness between two types as the nonexistence of a common supertype does not work. To account for >types we propose a notion of >-disjointness, where only common
supertypes that are top-like are allowed for two types A and B.
The difference between the two variants with > types is on theparticular definition of top-like types, which has an impact onwhich types are allowed on intersections. In a simple version, toplike types are the set of types: >, >&>, >&>&>, . . . . All suchtypes are proper top types: that is, they are supertypes of every
other type. Unfortunately the simple notion of top-like types has
limited expressiveness because it forbids any two function types
to be disjoint. The second definition of top-like types is more
liberal, and it allows for functional top types (such as Int → >)to be in the set of top-like types. With this variant of top-liketypes, the limitations in expressiveness are removed. Both variants
with > types are type-safe and coherent, and both notions of >disjointness have sound and complete algorithmic versions.
We have mechanized all three variants of λi and their metatheoretical results in the Coq proof assistant. The definitions andproofs use the locally nameless representation with co-finite quantification [3] to represent variables and binders. Except for two auxiliary lemmas used in the lambda cases for the proofs of soundness
and completeness of bidirectional type-checking, all proofs are “admit” free. In particular, the main proofs of this paper (coherence
and type-preservation) are complete. The two auxiliary theorems
that we did not manage to prove are trivially true, but they proved
surprisingly tricky to prove using the locally nameless representation with co-finite quantification.
In summary, the contributions of this paper are:
• Disjoint Intersection Types: A new form of intersection typewhere only disjoint types are allowed. A sound and complete
algorithmic specification of disjointness (with respect to thecorresponding formal definition) is presented for three different
variants of disjointness.
• Formalization of λi and Proof of Coherence: An elaboration

semantics of all three variants of λi into a simply typed λcalculus is given. Type-safety and coherence are proved andformalized. All definitions and metatheory are mechanicallyformalized using the Coq theorem prover.
• Implementation: An implementation of λi , encodings of sev-

eral examples presented in the paper, and also the Coq proofs
are available at:https://github.com/jalpuim/disjoint-intersection-types

2.

Overview

This section introduces λi and its support for intersection types
and the merge operator. We also discuss how the notion of disjoint
intersection types achieves a coherent semantics.
Note that this section uses some syntactic sugar, as well as standard programming language features, to illustrate the various concepts in λi . Although the minimal core language that we formalize
in Section 3 does not present all such features, our implementation
supports them.

2.1

Intersection Types and the Merge Operator

Intersection Types. The intersection of type A and B (denoted
as A & B in λi ) contains exactly those values which can be used asvalues of type A and of type B. For instance, consider the following
program in λi :let x : Int & Bool = . . . in -- definition omitted
let succ (y : Int) : Int = y+1 in
let not (y : Bool) : Bool = if y then False else True in(succ x, not x)

If a value x has type Int & Bool then x can be used as an integer
and as a boolean. Therefore, x can be used as an argument to any
function that takes an integer as an argument, and any function thattake a boolean as an argument. In the program above the functions
succ and not are simple functions on integers and characters, respectively. Passing x as an argument to either one (or both) of thefunctions is valid.
Merge Operator. In the previous program we deliberately did notshow how to introduce values of an intersection type. There aremany variants of intersection types in the literature. Our work follows a particular formulation, where intersection types are introduced by a merge operator [6, 14, 27]. As Dunfield [14] has argued
a merge operator adds considerable expressiveness to a calculus.
The merge operator allows two values to be merged in a single intersection type. In λi (following Dunfield’s notation), the merge oftwo values v1 and v2 is denoted as v1 , , v2 . For example, an implementation of x is constructed in λi as follows:
let x : Int & Boolean = 1,,True in . . .

Merge Operator and Pairs. The merge operator is similar to theintroduction construct on pairs. An analogous implementation of x
with pairs would be:
let xPair : (Int, Bool) = (1, True) in . . .

The significant difference between intersection types with a merge
operator and pairs is in the elimination construct. With pairs there
are explicit eliminators (fst and snd). These eliminators must be
used to extract the components of the right type. For example, inorder to use succ and not with pairs, we would need to write a
program such as:(succ (fst xPair), not (snd xPair))

In contrast the elimination of intersection types is done implicitly,
by following a type-directed process. For example, when a valueof type Int is needed, but an intersection of type Int & Bool isfound, the compiler generates code that uses fst to extract thecorresponding value at runtime.
2.2(In)Coherence

Coherence is a desirable property for the semantics of a programming language. A semantics is said to be coherent if any valid program has exactly one meaning [27] (that is, the semantics is not
ambiguous). In contrast a semantics is said to be incoherent if there
are multiple possible meanings for the same valid program.
Incoherence in Dunfield’s Calculus A problem with Dunfield’s
calculus [14] is that it is incoherent. Unfortunately the implicit
nature of elimination for intersection types built with a merge
operator can lead to incoherence. The merge operator combines
two terms, of type A and B respectively, to form a term of type
A&B. For example, 1, , T rue is of type Int&Bool. In this case,no matter whether 1, , T rue is used as Int or Bool, the result of
evaluation is always clear. However, with overlapping types, it is
not clear anymore to see the intended result. For example, whatshould be the result of the following program, which asks for an
integer (using a type annotation) out of a merge of two integers:(1,,2) : Int

Should the result be 1 or 2?
Dunfield’s calculus [14] accepts the program above, and it allows that program to result in 1 or 2. In other words the results ofthe program are incoherent.
Getting Around Incoherence In a real implementation of Dunfield’s calculus a choice has to be made on which value to compute. For example, one potential option is to always take the leftmost value matching the type in the merge. Similarly, one could
always take the right-most value matching the type in the merge.
Either way, the meaning of a program will depend on a biased implementation choice, which is clearly unsatisfying from the theoretical point of view. Dunfield suggests some other possibilities, suchas the possibility of restricting typing of merges so that a merge
has type A only if exactly one branch has type A. He also suggested
another possibility, which is to allow only for disjoint types in anintersection. This is the starting point for us and the approach that
we investigate in this paper.
2.3

Disjoint Intersection Types and their Challenges

λi requires that the two types in an intersection to be disjoint. Informally saying that two types are disjoint means that the set of valuesof both types are disjoint. Disjoint intersection types are potentially
useful for coherence, since they can rule out ambiguity when looking up a value of a certain type in an intersection. However there
are several issues that need to be addressed first in order to design
a calculus with disjoint intersection types and that ensures coherence. The key issues and the solutions provided by our work are
discussed next. We emphasize that even though Dunfield has mentioned disjointness as an option to restore coherence, he has notstudied the approach further or addressed the issues discussed next.
Simple disjoint intersection types Looking back at the expression 1, , 2 in Section 2.2, we can see that the reason for incoherenceis that there are multiple, overlapping, integers in the merge. Generally speaking, if both terms can be assigned some type C, bothof them can be chosen as the meaning of the merge, which leads tomultiple meanings of a term. A natural option is to try to forbid suchoverlapping values of the same type in a merge. Thus, for simple
types such as Int and Bool, it is easy to see that disjointness holds
when the two types are different. Intersections such as Int & Booland String & Bool are clearly disjoint. While an informal, intuitive notion of disjointness is sufficient to see what happens withsimple types, it is less clear what disjointness means in general.
Formalizing disjointness Clearly a formal notion of disjointness
is needed to design a calculus with disjoint intersection types,
and to clarify what disjointness means in general. As we shallsee the particular notion of disjointness is quite sensitive to thefeatures that are allowed in a language. Nevertheless, the different
notions of disjointness follow the same principle: they are definedin terms of the subtyping relation; and they describe which common
supertypes are allowed in order for two types to be considereddisjoint.
A first attempt at a definition for disjointness is to require that,given two types A and B, both types are not subtypes of each other.
Thus, denoting disjointness as A ∗ B, we would have:A ∗ B ≡ A 6<: B and B 6<: AAt first sight this seems a reasonable definition and it does prevent merges such as 1,,2. However some moments of thought areenough to realize that such definition does not ensure disjointness.
For example, consider the following merge:(1,,’c’) ,, (2,,True)

This merge has two components which are also merges. The firstcomponent (1,,’c’) has type Int&Char, whereas the second
component (2 ,, True) has type Int&Bool. Clearly,
Int&Char 6<: Int&Bool and Int&Bool 6<: Int&Char
Nevertheless the following program still leads to incoherence:succ ((1,,’c’),,(2,,True))as both 2 or 3 are possible outcomes of the program. Although thisattempt to define disjointness failed, it did bring us some additional
insight: although the types of the two components of the merge are
not subtypes of each other, they share some types in common.
In order for two types to be truly disjoint, they must not have any
sub-components sharing the same type. In a simply typed calculus
with intersection types (and without a > type) this can be ensured
by requiring the two types not to share a common supertype:Definition 1 (Simple disjointness). Two types A and B are disjoint(written A ∗ B) if there is no type C such that both A and B are
subtypes of C:A ∗ B ≡6 ∃C. A <: C and B <: CThis definition of disjointness prevents the problematic merge(1,,’c’),,(2,,True). Since Int is a common supertype of both
Int&Char and Int&Bool, those two types are not disjoint, according to this simple notion of disjointness.
The simple definition of disjointness is the basis for the first
calculus presented in this paper: a simply typed lambda calculus
with intersection (but without a > type). This variant of λi is usefulto study many important issues arising from disjoint intersections,
without the additional complications of >. As shown in Section 4,
this definition of disjointness is sufficient to ensure coherence in λi .
Disjointness of other types Equipped with a formal notion of
disjointness, we are now ready to see how disjointness works forother types. For example, consider the following intersection types
of functions:
1. (Int → Int) & (String → String)
2. (String → Int) & (String → String)
3. (Int → String) & (String → String)
Which of those intersection types are disjoint? It seems reasonable
to expect that the first intersection type is disjoint: both the domain
and co-domain of the two functions in the intersection are different.
However, it is less clear whether the two other intersection types are
disjoint or not. Looking at the definition of simple disjointness forfurther guidance, and the subtyping rule for functions in λi (whichis standard [5]):B1 <: A1A2 <: B2S→
A1 → A2 <: B1 → B2
we can see that the types in the second intersection do not share
any common supertypes. Since the target types of the two function
types (Int and String) do not share a common supertype, it is
not possible to find a type C that is both a common supertype of(String → Int) and (String → String). In contrast, for thethird intersection type, it is possible to find a common supertype:
String & Int → String. The contravariance of argument types
in S→ is important here. All that we need in order to find a common
supertype between (Int → String) and (String → String)is to find a common subtype between Int and String. One suchcommon subtype is String & Int. Preventing the third intersection type ensures that type-based look-ups are not ambiguous (andcannot lead to incoherence). If the third intersection type was allowed then the following program:f,,g : (String & Int) → String

where f has type Int → String and g has type String → String,
would be problematic. In this case either f or g could be selected,
potentially leading to very different (and incoherent) results whenapplied to some argument.
Is disjointness sufficient to ensure coherence? Another questionis whether disjoint intersection types are sufficient to ensure coherence. Consider the following example:

also required that the two types A and B are not themselves top-like(condition #1). The unary relation e · d denotes such top-like types.
Top-like types obviously include the > type. However top-liketypes also include other types which are syntactically different from>, but behave like a > type. For example, > & > is syntacticallydifferent from >, but it is still a supertype of every other type(including > itself). A standard subtyping relation for intersection
types includes a rule:
A1 <: A2A1 <: A3S&R
A1 <: A2 &A3(succ,,not) (3,,True)

Here there are two merges, with the first merge being applied tothe second. The first merge contains two functions (succ and not).
The second merge contains two values that can serve as input tothe functions. The two merges are disjoint. However what shouldbe the result of this program? Should it be 4 or False?
There is semantic ambiguity in this program, even though it onlyuses disjoint merges. However a close look reveals a subtly different problem from the previous programs. There are two possible
types for this program: Int or Bool. Once the type of the programis fixed, there is only one possible result: if the type is Int the result of the program is 4; if the type is Bool then the result of the
program is False. Like other programming language features (forexample type classes [31]), types play a fundamental role in determining the result of a program, and the semantics of the language is not completely independent from types. In essence there
is some type ambiguity, which happens when some expressions canbe typed in multiple ways. Depending on which type is chosen forthe sub-expressions the program may lead to different results. Thisphenomenon is common in type-directed mechanisms, and it also
affects type-directed mechanisms such as type classes or, more generally, qualified types [18].
The typical solution to remove type ambiguity is to add type annotations that choose a particular type for a sub-expression when
multiple options exist. Our approach to address this problem is touse bidirectional type-checking techniques [16, 25]. We show thatwith a fairly simple and unremarkable bidirectional type system,
we can guarantee that every sub-expression (possibly with annotations) has a unique type. For example:((succ,,not) : Int → Int) (3,,True)is a valid λi program, which has a unique determined type, andresults in 4. In this case the bidirectional type-system forces users toprovide an annotation of the expression being applied. Without the
annotation the program would be rejected. With the bidirectional
type system, disjointness is indeed sufficient to ensure coherence.
2.4

Disjoint Intersection Types with >In the presence of a > type the simple definition of disjointness isuseless: > is always a common supertype of any two types. Therefore, with the previous definition of disjointness no disjoint intersections can ever be well-formed in the presence of >! Moreover,since > is not disjoint to any type, it does not make sense to allow its presence in a disjoint intersection type. Adding a > typerequires some adaptations to the notion of disjointness. This paper
studies two additional variants of λi with > types. In both variants
the definition of disjointness is revised as follows:
Definition 2 (>-disjointness). Two types A and B are disjoint(written A ∗ B) if the following two conditions are satisfied:
1. (not eAd) and (not eBd)
2. ∀C. if A <: C and B <: C then eCd
In the presence of >, instead of requiring that two types do
not share any common supertype, we require that the only allowedcommon supertypes are top-like (condition #2). Additionally, it is

The presence of S&R means that not only >&><:> but also ><:>&> are derivable. In other words, in a calculus like Dunfield’s
there are infinitely many syntactically different types that behave
like a > type: >, >&>, >&>&>, . . .
The notion of >-disjointness has two benefits. Firstly, and more
importantly, >-disjointness is sufficient to ensure coherence. For
example, the following program is valid, and coherent:
3,,True : >Even though the types of both components of the merge are a
subtype of the type of the program (>), the result of the program isalways the unique > value. Secondly, >-disjointness has the sideeffect of excluding other top-like types from the system: the type>&> is not a well-formed disjoint intersection type. In contrast to
Dunfield’s calculus, λi has a unique syntactic > type.
Functional intersections and top-like types The two variants of
λi with > differ slightly on the definition of top-like types. The
concrete definition of top-like types is important because it affects
what types are allowed in intersections. In the simpler version of
λi with >, multiple functions cannot coexist in intersections. Thisis obviously a drawback and reduces the expressiveness of the system. The essential problem is that a simple notion of top-like types
is too restrictive. For example consider again the intersection type:(String → Int) & (String → String)
According to the simple definition of disjointness, this disjoint
intersection type is valid. However according to >-disjointness
and a simple definition of top-like types, which accounts only forproper top types, this disjoint intersection type is not valid. The
two types have a common supertype which is not a supertype ofevery type: String → >. In this case (String → >) <: >,but > <
6 : (String → >). Therefore the two types do not meetthe second condition of >-disjointness as there exists a common
supertype, which is not top-like.
Generalizing top-like types In the second variant of λi top-liketypes are defined more liberally and they allow function types
whose co-domain is a top type to be considered as a top-like
type. For example, the type String → > is considered a top-like
type. The benefit of allowing this more liberal notion of top-liketypes is that, similarly to the first variant of λi without >, disjoint
intersections can have multiple function types.

3.

The λi Calculus and its Type System

This section presents the syntax, subtyping and type assignment of
λi : a calculus with intersection types and a merge operator. This
calculus is inspired by Dunfield’s calculus [14], without considering union types. Moreover, since we are only interested in disjoint
intersections, λi also has different typing rules for intersections
from those in Dunfield’s calculus. Sections 4 and 5 will present
the more fundamental contributions of this paper by showing otherrequired changes for supporting disjoint intersection types and ensuring coherence. The calculus in this section does not include theTypes

Terms

Contexts

A, B, C

e

Γ

::=
|
|
|

Int
A→B
A×B
A&B

::=
|
|
|
|
|
|

i
x
λx. e
e1 e2
(e1 , e2 )projk e k ∈ {1, 2}
e1 , , e2::=· | Γ, x : A

Figure 1. λi syntax.

A ordinary
A → B ordinary

A × B ordinary

Int ordinary

A <: B ,→ E
SZ

Int <: Int ,→ λx. x
A1 <: B1 ,→ E1

A2 <: B2 ,→ E2
S×

A1 × A2 <: B1 × B2 ,→ λp. (E1 (proj1 p), E2 (proj2 p))
B1 <: A1 ,→ E1

A2 <: B2 ,→ E2
S→> type, since it brings additional complications. Section 6 presents
two variants of λi with a > type, while preserving coherence.
3.1

SyntaxFigure 1 shows the syntax of λi . The difference from the λ-calculus(with pairs), highlighted in gray, are intersection types (A&B) at the
type-level, and merges (e1 , , e2 ) at the term level.
Types. Meta-variables A, B range over types. Types include function types A → B and product types A×B. A&B denotes the intersection of types A and B. We also include integer types Int. Notethat & has higher precedence than →, meaning that A&B → C is
equivalent to (A&B) → C.
Terms. Meta-variables e range over terms. Terms include standard constructs: variables x; abstraction of terms over variables
λx. e; application of terms e1 to terms e2 , written e1 e2 ; pairingof two terms (denoted as (e1 , e2 )); and both projections of a paire, written projk e (with k ∈ {1, 2}). The expression e1 , , e2 is themerge of two terms e1 and e2 . Merges of terms correspond to intersections of types A&B. In addition, we also include integer literalsi.
Contexts. Typing contexts are standard: Γ tracks bound variables
x with their type A.
In order to focus on the key features that make this language interesting, we do not include other forms such as type constants andfixpoints here. However they can be included in the formalizationin standard ways.
3.2

Subtyping

The subtyping rules of the form A <: B are shown in the top part of
Figure 2. At the moment, the reader is advised to ignore the grayshaded part in the rules, which will be explained later. The ruleS→ says that a function is contravariant in its parameter type andcovariant in its return type. The three rules dealing with intersection
types are just what one would expect when interpreting types as
sets. Under this interpretation, for example, the rule S&R says that
if A1 is both the subset of A2 and the subset of A3 , then A1 is also
the subset of the intersection of A2 and A3 .
Note that the notion of ordinary types, which is used in rules
S&L1 and S&L2 , was introduced by Davies and Pfenning [12]to provide an algorithmic version of subtyping. In our system
ordinary types are used for a different purpose as well: they playa fundamental role in ensuring that subtyping produces uniquecoercions. Section 5 will present a detailed discussion on this. The
subtyping relation, is known to be reflexive and transitive [12].

A1 → A2 <: B1 → B2 ,→ λf. λx. E2 (f (E1 x))
A1 <: A2 ,→ E1

A1 <: A3 ,→ E2
S&R

A1 <: A2 &A3 ,→ λx. (E1 x, E2 x)
A1 <: A3 ,→ E

A3 ordinary

A1 &A2 <: A3 ,→ λx. E (proj1 x)
A2 <: A3 ,→ E

S&L1

A3 ordinary

A1 &A2 <: A3 ,→ λx. E (proj2 x)

S&L2

Γ `A

Γ ` Int

WFZ

Γ `A
Γ `B
WF×
Γ `A×B

Γ `A
Γ `B
WF→
Γ `A→BΓ `A

Γ `BΓ ` A&B

A∗B

WF&

Γ `e : A
x:A ∈ ΓT-VAR
Γ `x :AΓ `AΓ, x : A ` e : B
T-L AMΓ ` λx. e : A → B

T-I NTΓ ` e1 : AΓ ` e2 : B
T-P RODΓ ` (e1 , e2 ) : A × BΓ ` i : IntΓ ` e1 : A1 → A2
Γ ` e2 : A1
T-A PPΓ ` e1 e2 : A2
Γ ` e1 : AΓ ` e2 : BΓ ` e1 , , e2 : A&BΓ ` e : A1 × A2
T-P ROJΓ ` projk e : Ak

A∗B

T-M ERGEΓ `e : A
A <: B
T-S UBΓ `e : B

Figure 2. Declarative type system of λi .

3.3

Declarative Type System

The well-formedness of types and the typing relation are shown inthe middle and bottom of Figure 2, respectively. Importantly, thedisjointness judgment, which is highlighted using a box, appears
in the well-formedness rule for intersection types (WF&) and thetyping rule for merges (T-M ERGE). The presence of the disjointness judgment, as well as the use of ordinary types in the subtyping
relation, are the most essential differences between our type systemand the original type system by Dunfield.
Apart from WF&, the remaining rules for well-formedness are
standard. The typing judgment is of the form:Γ `e : A
It reads: “in the typing context Γ , the term e is of type A”. The
standard rules are those for variables T-VAR; lambda abstractions
T-L AM; application T-A PP; integer literals T-I NT; products TP ROD; and projections T-P ROJ. T-M ERGE means that a merge
e1 , , e2 , is assigned an intersection type composed of the resulting
types of e1 and e2 , as long as the types of the two expressions are
disjoint. Finally, T-S UB states that for any types A and B, if A <: B
then any expression e with assigned type A can also be assigned thetype B.

A first reason why such rule would not work in λi is that it does not
restrict A&B to be disjoint. Therefore, in the presence of such anunrestricted rule it would be possible to create non-disjoint intersections types. It is easy enough to have an additional disjointness
restriction, which would ensure the disjointness between A and B.
However, even if that issue is fixed, the rule would be counterintuitive. If A and B are disjoint then, by definition, no expressions
should ever have types A and B at the same time. In contrast, in
λi , the rule T-M ERGE captures the fact that two disjoint pieces ofevidence are needed to create a (disjoint) intersection type.

4.

Semantics, Disjointness and CoherenceThis section discusses the elaboration semantics of λi , and shows abidirectional type system that guarantees coherence and type safety.
Moreover the bidirectional type system is shown to be sound andcomplete with respect to the type system presented in Section 3(provided that terms have some additional type annotations). The
coherence theorem presented in this section, relies on two key
aspects of the calculus:• Uniqueness of subtyping coercions: the notion of ordinary

types and well-formed disjoint intersection types ensures thatcoercions produced by subtyping relation are unique.
• No type ambiguity: the bidirectional type system does not havetype-ambiguity, and it infers a unique type for every well-typed
expression.
4.1

Target of Elaboration

The dynamic semantics of the call-by-value λi is defined via a typedirected translation into the simply typed λ-calculus with pair andunit types. The syntax and typing of our target language is unsurprising. The syntax of the target language is shown in Figure 3.
The highlighted part shows its difference with the λ-calculus. We
included a unit type () and its only inhabitant (), but they will only

T

Terms

E

Contexts

G

::=
|
|
|
::=
|
|
|
|
|

Int
()
T1 → T2
T1 × T 2
x
i
()
λx. E
E1 E2
(E1 , E2 )|::=projk E
· | G, x : T

k ∈ {1, 2}

Figure 3. Target language syntax.
|A| = T
|Int| = Int|A1 → A2 | = |A1 | → |A2 |Typing disjoint intersections Dunfield’s calculus has different
typing rules for intersections. However, his rules make less sense
in a system with disjoint intersections. For example, they include
the following typing rule, for introducing intersection types:Γ `e :AΓ `e :BΓ ` e : A&B

Types|A1 × A2 | = |A1 | × |A2 ||A1 &A2 | = |A1 | × |A2 ||Γ | = G|·| = ·
|Γ, α : A| = |Γ |, α : |A|
Figure 4. Type and context translation.
used in Section 6. The typing rules can be found in our Coq development.
Type and Context Translation. Figure 4 defines the type translation function |·| from λi types A to target language types T . The
notation |·| is also overloaded for context translation from λi contexts Γ to target language contexts G.
4.2

Coercive Subtyping and Coherence

The λi calculus uses coercive subtyping, where subtyping derivations produce a coercion that is used to transform values of one
type to another type. Our calculus ensures that the coercions produced by subtyping are unique. Unique coercions are fundamental
for proving our coherence result of the semantics of λi .
Coercive subtyping. The judgment
A1 <: A2 ,→ E
extends the subtyping judgment in Figure 2 with a coercion on theright hand side of ,→ . A coercion E is just a term in the target
language and is ensured to have type |A1 | → |A2 | (by Lemma 1).
For example,
Int&Bool <: Bool ,→ λx. proj2 x
generates a coercion function with type: Int&Bool → Bool.
Note that, in contrast to Dunfield’s elaboration approach, wheresubtyping produces coercions that are source language terms, in
λi , coercions are produced directly on the target language.

The rule SZ generates the identity function as the coercion in
the target language. Rule S× says that one pair is a subtype ofanother, as long as the first and second component of the former
are a subtype of the first and second component of the latter,
respectively. The generated coercion extracts both components ofthe pair, applies the respective coercion, and creates a new pairusing both results. In S→, we elaborate the subtyping of parameterand return types by η-expanding f to λx. f x, applying E1 tothe argument and E2 to the result. Rules S&L1 , S&L2 , and S&R
elaborate intersection types. S&R uses both coercions to form apair. Rules S&L1 and S&L2 reuse the coercion from the premises
and create new ones that cater to the changes of the argument typein the conclusions. Note that the two rules are overlapping andhence a program can be elaborated differently, depending on which
rule is used. Finally, all rules produce type-correct coercions:also include, for example, record types. In the left decomposition
rules for intersections we introduce a requirement that A3 is ordinary. The consequence of this requirement is that when A3 is anintersection type, then the only rule that can be applied is S&R.
Unique coercions. Well-formedness and ordinary types guarantee that at any moment during the derivation of a subtyping relation,
at most one rule can be used. Consequently, the coercion of a subtyping relation A <: B is uniquely determined. This fact is capturedby the following lemma:
Lemma 3 (Unique coercion). If A <: B ,→ E1 and A <:B ,→ E2 , where A and B are well-formed types, then E1 ≡ E2 .
4.3

Bidirectional Type System with Elaboration

1. The left decomposition rules for intersections (S&L1 andS&L2 ) overlap with each other.

In order to prove the coherence result we first introduce a bidirectional type system, which is closely related to the type systempresented in Section 3. The bidirectional type system is elaborating, producing a term in the target language while performing thetyping derivation.
The bidirectional type system is useful for two different reasons.
Firstly, the presence of the subsumption rule (T-S UB) makes thetype system not syntax directed, which presents a challenge for an
implementation. Bidirectional type-checking makes the rules syntax directed again. Secondly, and more importantly, the subsumption rule also creates type ambiguity: the same term can have multiple types. This is problematic because there can be different semantics for a term, depending on the type of the term. Bidirectional
type-checking comes to the rescue again, by ensuring that with theadditional type annotations only one type is inferred for a term.

2. The left decomposition rules for intersections (S&L1 andS&L2 ) overlap with the right decomposition rules for intersections S&R.

Key Idea of the elaboration. The key idea in the elaboration is
to turn merges into usual pairs, similar to Dunfield’s elaboration
approach [14]. For example,

Well-formedness and disjointness The fact that in λi all intersection types are disjoint is useful to deal with problem 1). Recall thedefinition of disjointness:

1, , "one"Lemma 1 (Subtyping rules produce type-correct coercions). If
A1 <: A2 ,→ E , then · ` E : |A1 | → |A2 |.
Proof. By a straightforward induction on the derivation.
Overlapping subtyping rules The key problem with the subtyping rules in Figure 2 is that all three rules dealing with intersection types (S&L1 and S&L2 and S&R) overlap. Unfortunately, thismeans that different coercions may be given when checking thesubtyping between two types, depending on which derivation ischosen. This is the ultimate reason for incoherence. There are two
important types of overlap:

Definition 3 (Simple disjointness). Two types A and B are disjoint(written A ∗ B) if there is no type C such that both A and B are
subtypes of C:

becomes (1, "one"). In usage, the pair will be coerced according totype information. For example, consider the function application:(λx. x : String → String) (1, , "one")
This expression will be translated toA ∗ B ≡6 ∃C. A <: C and B <: C

(λx. x) ((λx. proj2 x) (1, "one"))

Disjoint intersections are enforced by well-formedness of types.
Since the two types in an intersection are disjoint, it is impossiblethat both of the preconditions of the left decompositions are satisfied at the same time. Therefore, only one of the two left decomposition rules can be chosen for a disjoint intersection type. Moreformally, with disjoint intersections, we have the following theorem:

The coercion in this case is (λx. proj2 x). It extracts the second
item from the pair, since the function expects a String but thetranslated argument is of type (Int, String).

Lemma 2 (Unique subtype contributor). If A1 &A2 <: B, where
A1 &A2 and B are well-formed types, then it is not possible thatboth of the following hold at the same time:
1. A1 <: B
2. A2 <: B
Unfortunately, disjoint intersections alone are insufficient todeal with problem 2). In order to deal with problem 2), we introduce
a distinction between types, and ordinary types.
Ordinary types. Ordinary types are just those which are not intersection types, and are asserted by the judgment

The elaboration judgments and rules. Figure 5 presents the elaborating bidirectional type system, which is closely related to thedeclarative type-system, presented in Figure 2. The key differences
between them are that all :’s are replaced with ⇒ or ⇐. There are
two check-mode rules: T-L AM and T-S UB. The remaining rules are
all in the synthesis mode. Moreover there is one additional rule forannotation expressions (T-A NN). The syntax of source terms also
needs to be extended with annotation expressions e : A. The reader
might notice that the choice for this type-system does not follow
the convention of making introduction forms as checked and elimination forms as synthesized [12, 16]. We use this design because:
1. We aim at maximizing type-inference: annotations becomesless of a burden as there are only two checked premises in ourrules (excluding T-A NN);A ordinary

2. Most of the language is simple enough to rely on type inference(i.e. it is decidable);

Since types in λi are simple, the only ordinary types are function
type, integers and pairs. But in richer systems, ordinary types can

3. The simplicity of this design allows us to concentrate on its key
property, which is the coherence of the type-system.

bAc = TΓ ` e ⇒ A ,→ E

e synthesizes type A
bic = ix:A ∈ ΓT-VAR
Γ ` x ⇒ A ,→ x

Γ ` i ⇒ Int ,→ i

T-I NTbλx. ec = λx. bec
be1 e2 c = be1 cbe2 cΓ ` e2 ⇐ A1 ,→ E2

Γ ` e1 ⇒ A1 → A2 ,→ E1

T-A PPΓ ` e1 e2 ⇒ A2 ,→ E1 E2
Γ ` e1 ⇒ A ,→ E1

bxc = xb(e1 , e2 )c = (be1 c, be2 c)bprojk ec = projk bec (k ∈ 1, 2)
be1 , , e2 c = be1 c , , be2 cΓ ` e2 ⇒ B ,→ E2
T-P ROD

be : Ac = bec

Γ ` (e1 , e2 ) ⇒ A × B ,→ (E1 , E2 )Figure 6. Type annotation erasure.
Γ ` e ⇒ A1 × A2 ,→ EΓ ` projk e ⇒ Ak ,→ projk E

T-P ROJ

Proof. (Sketch) By structural induction on the term and the corresponding inference rule.

Γ ` e1 ⇒ A ,→ E1
A∗BΓ ` e2 ⇒ B ,→ E2

T-M ERGEΓ ` e1 , , e2 ⇒ A&B ,→ (E1 , E2 )Γ ` e ⇐ A ,→ EΓ ` e : A ⇒ A ,→ EΓ ` e ⇐ A ,→ EΓ `Ae checks against given type AΓ ` λx. e ⇐ A → B ,→ λx. EΓ ` e ⇒ A ,→ E

Proof. Since we define the dynamic semantics of λi in terms ofthe composition of the type-directed translation and the dynamic
semantics of λ-calculus, type safety follows immediately.

T-A NNΓ, x : A ` e ⇐ B ,→ E

T-L AMA <: B ,→ EsubΓ ` e ⇐ B ,→ Esub E

T-S UB

Figure 5. Bidirectional type system of λi .
Having this in mind, we do not claim this bidirectional typesystem is the optimal choice for the system, and other design
choices could be equally justified had our intentions been different.
We may now explain in more detail this elaborating bidirectional type-system. The two elaboration judgments Γ ` e ⇒A ,→ E and Γ ` e ⇐ A ,→ E extend the usual typing judgments with an elaborated term on the right hand side of the arrows.
The elaboration ensures that E has type |A|. Noteworthy are the TM ERGE and T-S UB rules. The T-M ERGE straightforwardly translates merges into pairs. The T-S UB accounts for the type coercions
arising from subtyping. The additional coercions are necessary toensure that the target terms are correctly typed, since the target language lacks subtyping. Note that the elaboration judgments can bemodeled as a single relation, where the mode is an additional parameter of the relation. Thus for theorems that need both judgments
simple induction is sufficient (mutual induction is not needed).
Type-safety The type-directed elaboration is type-safe. This
property is captured by the following two theorems.
Theorem 1 (Type preservation). We have that:• If Γ ` e ⇒ A ,→ E , then |Γ | ` E : |A| .
• If Γ ` e ⇐ A ,→ E , then |Γ | ` E : |A|.

Theorem 2 (Type safety). If e is a well-typed λi term, then eevaluates to some λ-calculus value v.

Soundness and Completeness The declarative type system presented in Figure 2 is closely related to the bidirectional type system in Figure 5. We can prove that the bidirectional type system
is sound and complete with respect to the declarative specification,
modulo some additional type-annotations. To relate terms which
are typeable in both systems, we use the definition of erasure shownin Figure 6.
Theorem 3 (Soundness of bidirectional type-checking). We havethat:
• If Γ ` e ⇒ A ,→ E , then Γ ` bec : A.
• If Γ ` e ⇐ A ,→ E , then Γ ` bec : A.

Proof. (Sketch) By structural induction on the term and the corresponding inference rule.
Theorem 4 (Completeness of bidirectional type-checking). If Γ `e : A, then Γ ` e 0 ⇒ A ,→ E , where be 0 c = e.
Proof. (Sketch) By structural induction on the term and the corresponding inference rule.
Uniqueness of type-inference An important property of the bidirectional type-checking in Figure 5 is that, given an expression e,
if it is possible to infer a type for e, then e has a unique type.
Theorem 5 (Uniqueness of type-inference). If Γ ` e ⇒ A1 ,→ E1
and Γ ` e ⇒ A2 ,→ E2 then A1 = A2 .
Proof. (Sketch) By structural induction on the term and the corresponding inference rule.
In contrast, as illustrated in Section 2.3, in the declarative typesystem some terms may have multiple, incompatible types. Therefore there is no uniqueness of types for the declarative type system,and the same term can have different semantics depending on its
type.

4.4

Coherency of Elaboration

A ∗i B

Combining the previous results, we show the central theorem:
Theorem 6 (Unique elaboration). We have that:• If Γ ` e ⇒ A1 ,→ E1 and Γ ` e ⇒ A2 ,→ E2 , thenE1 ≡ E2 .
• If Γ ` e ⇐ A1 ,→ E1 and Γ ` e ⇐ A2 ,→ E2 , thenE1 ≡ E2 .
(“≡” means syntactical equality, up to α-equality.)A ∗ax BInt ∗ax A → B ∗A X(Z →)Int ∗ax A × B ∗A X(Z×)

A × B ∗ax C → D ∗A X(× →)T-A PP

we need to show the uniqueness of A1 using Theorem 5, in order
to apply the induction hypothesis.

Algorithmic Disjointness

Section 4 presented a type system with disjoint intersection types
that is both type-safe and coherent. Unfortunately the type system
is not yet algorithmic because the specification of disjointness does
not lend itself to an implementation directly. This is a problem,
because we need an algorithm for checking whether two types are
disjoint or not in order to implement the type-system.
This section presents the set of rules for determining whether
two types are disjoint. The set of rules is algorithmic and an implementation is easily derived from them. The derived set of rules for
disjointness is proved to be sound and complete with respect to thedefinition of disjointness in Section 4.
Algorithmic Rules

The rules for the disjointness judgment are shown in Figure 7,
which consists of two judgments.
Main Judgment. The judgment A ∗i B says two types A and B
are disjoint. The rules dealing with intersection types (∗&L and∗&R) are quite intuitive. The intuition is that if two types A and B
are disjoint to some type C, then their intersection (A&B) is also
clearly disjoint to C. The rules capture this intuition by inductively
distributing the relation itself over the intersection constructor (&).
Although those two rules overlap, the order of applying them in
an implementation does not matter as applying either of them will
eventually leads to the same conclusion, that is, if two types are
disjoint or not.
The rule for functions (∗→) is more interesting. It says thattwo function types are disjoint if and only if their return types are
disjoint (regardless of their parameter types!). At first this rule may
look surprising because the parameter types play no role in thedefinition of disjointness. To see the reason for this consider thetwo function types:
Int → StringA ∗ax B∗AX
A ∗i BB ∗ax A∗A XSYM
A ∗ax BΓ ` e2 ⇐ A1 ,→ E2

Γ ` e1 e2 ⇒ A2 ,→ E1 E2

5.1

A2 ∗i B2
∗π2
A1 × A2 ∗i B1 × B2

T-S UB

we need to show not only that Esub is unique (by Lemma 3), butalso that A is unique (by Theorem 5). Uniqueness of A is needed
to apply the induction hypothesis. For T-A PP:

5.

A1 ∗i B1
∗π1
A1 × A2 ∗i B1 × B2

A <: B ,→ EsubΓ ` e ⇐ B ,→ Esub EΓ ` e1 ⇒ A1 → A2 ,→ E1

A ∗i B1
A ∗i B2∗&R
A ∗i B1 &B2A2 ∗i B2∗→
A1 → A2 ∗i B1 → B2

Proof. By induction on the first derivation. Note that two cases
need special attention: T-S UB and T-A PP. In the T-S UB rule:Γ ` e ⇒ A ,→ E

A1 ∗i BA2 ∗i B∗&L
A1 &A2 ∗i B

Bool → String

Even though their parameter types are disjoint, we are still able
to think of a type which is a supertype for both of them. For
example, Int&Bool → String. Therefore, two function types

Figure 7. Algorithmic Disjointness.

with the same return type are not disjoint. Essentially, due to thecontravariance of function types, functions of the form A → C and
B → C always have a common supertype (for example A&B →C). The lesson from this example is that the parameter types of two
function types do not have any influence in determining whether
those two function types are disjoint or not: only the return types
matter.
Finally, the rules for pairs (∗π1 and ∗π2 ) say that either the firstcomponents or the second components must be disjoint. This is due
to product subtyping being covariant: disjointness of either component is enough to make it impossible to construct a supertype. For
instance, take the following two product types:(Int, String)(Bool, String)

We can never come up with a common supertype for these because
it does not exist a type C which is both a supertype of Int andBool.
Axioms. Up till now, the rules of A ∗i B have only taken care of
two types with the same language constructs. But how can the factthat Int and Int → Int are disjoint be decided? That is exactly
the place where the judgment A ∗ax B comes in handy. It provides
the axioms for disjointness. What is captured by the set of rules isthat A ∗ax B holds for all two types of different constructs unless
any of them is an intersection type.
5.2

Meta-theory

The following two theorems together say that the algorithmic judgment and the definition of disjointness are equivalent.
Theorem 7 (Soundness of algorithmic disjointness). For any two
types A and B, A ∗i B implies A ∗ B.
Proof. By induction on the derivation of A ∗i B.
Theorem 8 (Completeness of algorithmic disjointness). For any
two well-formed types A and B, A ∗ B implies A ∗i B.
Proof. By a case analysis on the shape of A and B.

TypesA, B, C::=... | >

Terms

e

::=

... | >

A <: B ,→ E
ST OP

A <: > ,→ λx. ()6.2

As discussed in Section 2, the definition of simple disjointness isuseless when λi is extended with >. For these reasons, we differentiate top-like types from the rest of the types, so that restrictions
may be imposed based on the former. For now, the formal definitionof a top-like type is omitted, and we informally define it as a typethat resembles > in some way. Having this in mind, >-disjointness
is defined as follows:
Definition 4 (>-Disjointness). Given two types A and B we havethat:
A ∗> B = (not eAd) and (not eBd) and(∀C. if A <: C and B <: C then eCd)

Γ `A
Γ `>

Disjointness

WFT OP

where eCd means that C is a top-like type.
Informally, given two types A and B:Γ ` e ⇒ A ,→ E

e synthesizes type A• A and B cannot be top-like types (i.e. preventing types such as

T &T to be well-formed).
T-T OP• If there is any common supertype of A and B, that is not top-Γ ` > ⇒ > ,→ ()|A| = T|>| = ()

Figure 8. Extending λi with >.

6.

Disjoint Intersection Types with >This section shows how to add a > type to λi . Introducing >
poses some important challenges. Most prominently, the simple
definition of disjointness is useless in the presence of >. Since
all types now have a common supertype, it is impossible for any
two types to satisfy a simple notion of disjointness. To address thisproblem a notion of >-disjointness is proposed. The definition of>-disjointness depends on a notion of a top-like type. We formalize
two different variants of λi , based on two different definitions of a
top-like type, while discussing their expressiveness. Both variants
retain coherence, and all other key properties of λi . Since theproperties are essentially the same as those stated in Sections 4 and
5, we do not restate them here. Also we omit pairs from the twovariants of λi presented in this section, as they do not impose any
important challenge and their introduction is quite straightforward.
Mechanized Coq proofs for both variants are available online.
6.1

Introducing >Introducing the > type in the λi calculus is not difficult. We extended our system following Dunfield’s calculus [14], as shown in
Figure 8. Existing types are extended with > and, correspondingly,
we add the canonical inhabitant of type >: the term >. The subtyping relation is extended with ST OP, declaring that any type is asubtype of >. The coercion in the target language, is a function thatalways returns the term (), regardless of its argument. We also add> to the set of well-formed types by extending the well-formedness
relation with WFT OP. Finally, the typing rule T-T OP states that,
under type inference, the term > has type > and generates the term() in the target language.

like, then intersection of these types is forbidden, as there might
be an overlap between them.
Another problem arising from the introduction of > is that
Lemma 2 no longer holds. For example, given A1 &A2 <: > (forany type A1 and A2 ), both A1 or A2 can be coerced to > (because
any type is a subtype of >). Thus, in this case, the type A1 &A2has two subtype contributors violating Lemma 2. Nevertheless, it
is still possible to prove a weaker result. Namely:
Lemma 4 (Unique subtype contributor (with >)). If A1 &A2 <: B,
where A1 &A2 and B are well-formed types, and B is not top-like,then it is not possible that the following holds at the same time:
1. A1 <: B
2. A2 <: B
This suggests that we will need to take special care to preserve
coherence in the presence of top-like types.
6.3

A Simple Calculus with >In the first variant of λi with > the basic idea is to have a definitionof top-like types, which captures all syntactically distinct top types:>, >&>, >&>&>. The resulting system has only one syntactic >,namely > itself. Moreover, coherence is preserved.
Top-Like Types A top-like type can be formalized as a unary
relation on a type A, denoted as eAd, as shown in Figure 9. The rule
T OPLIKE -T OP states that > is a top-like type; the rule T OPLIKE I NTER indicates that any intersection composed of just top-liketypes is also a top-like type.
Algorithmic disjointness rules Similarly to the original system,
the definition of >-disjointness does not lead to an implementation.
Fortunately, the algorithmic disjointness rules, shown in Figure 9,
remain the almost same as described in Section 5. The only significant difference is the absence of the ∗→ rule. The reason for thisis that, in this variant of λi , two functions always have non-top-likecommon supertypes. For example, consider the function types:
Bool → Int

String → String

Although both the domains and co-domains of the functions seemto be unrelated, there are still non-top-like common supertypes in
the presence of >. For example, Bool&String → > is a common
supertype of the previous function types. In general, in this variantof λi , any two function types are never disjoint.

eAd

e>d

eAd

eAd
eBd
T OPLIKE -I NTER
eA&Bd

T OPLIKE -T OP

e>d

eBd
T OPLIKE -F UN
eA → Bd

A ∗i BA 1 ∗i B
A 2 ∗i B∗&L
A1 &A2 ∗i B

eAd
eBd
T OPLIKE -I NTER
eA&Bd

T OPLIKE -T OP

A ∗i B1
A ∗i B2∗&R
A ∗i B1 &B2
A <: B ,→ E

A ∗ax B∗AX
A ∗i BA1 <: A3 ,→ E

A1 &A2 <: A3 ,→ λx. JA3 K(E (proj1 x))

A ∗ax BInt ∗ax A → B ∗A X(Z →)A3 ordinary

A2 <: A3 ,→ E

B ∗ax A∗A XSYM
A ∗ax B

A3 ordinary

A1 &A2 <: A3 ,→ λx. JA3 K(E (proj2 x))

Figure 9. Top-like types and Algorithmic Disjointness.

Finally, note that this variant of λi excludes all types of the form
A&B, where A and B are top-like. Thus, the system is left with only
one well-formed syntactic > type.
6.4

An Improved Calculus with >The definition of top-like types in Section 6.3 is, unfortunately,
quite restrictive: multiple function types are not allowed within intersection types. This is in contrast with the original λi calculus,
where multiple function types can co-exist in an intersection. To address this limitation, we generalize the definition of top-like types.
The generalization introduces a new ambiguity in our subtyping
rules, which requires some changes on the generation of target language coercions.
Top-Like Types The extended top-like definitions and resulting system are formalized in Figure 10. Note how we just added
T OPLIKE -F UN to the top-like relation, by stating that a function is
top-like whenever its return type is also top-like. Although function
types that return a top-like type are not strictly speaking top-types,
they can be viewed as pre-top-types: applying a value of this type
results in a value of type >, regardless of the application’s argument(s). In general, any type of the form Ak → > (with k ∈ N),
is considered a top-like type in the new variant of λi . The consequence of allowing this more liberal notion of top-like types is thatnow disjoint intersections such as

Coercive Subtyping The new definition of top-like types introduces a new problem when generating coercions. Introducing functions within intersection types leads to ambiguity between subtype
contributors under intersection types. Let us demonstrate this using

S&L2

A ∗i BA1 ∗i BA2 ∗i B∗&L
A1 &A2 ∗i B

A ∗i B1
A ∗i B2∗&R
A ∗i B1 &B2A2 ∗i B2∗→
A1 → A2 ∗i B1 → B2

A ∗ax B∗AX
A ∗i BA ∗ax B¬eBd
∗A XINT-F UN
Int ∗ax A → B

B ∗ax A∗A XSYM
A ∗ax B

Figure 10. Top-like types, Subtyping (changed rules only) and
Algorithmic Disjointness for the improved calculus.

JAKC = T
JAKC =

JAK = TJAK =(Bool → Int)&(String → String)
are well-formed: both functions types are not top-like types according to the new definition; and the only common supertypes that theyshare are top-like types (for example: Bool&String → >).
Note that the notion of a pre-top-type is not novel amongst intersection type-systems. For example, Coppo et al. [9] refer to function types where the codomain is not > as tail-proper types. However we have not investigated whether the definitions are deeply
connected and doing so is left as future work.

S&L1

eAd
JAK
otherwise CA=>
A = A1 → A2()
λx. JA2 K

Figure 11. Coercion generation considering Top-like types.

an example. Suppose that we want to build a derivation for:(Int → Int)&(Char → Char) <: (Int&Char) → >There are two possible derivations:• one using Int → Int <: (Int&Char) → > (via S&L1 );• another using Char → Char <: (Int&Char) → > (via

S&L2 ).

Unfortunately the two derivations generate different coercions.
Thus, without further changes in λi , this would be a source ofincoherence.
To address this new source of incoherence, we change the way
coercions are generated in S&L1 and S&L2 . The changes areshown in Figure 10. The basic idea is to look at the form of A3
in both rules:• when A3 is top-like (eA3 d), the coercion is a function with thesame arity of A3 , returning ();• when A3 is not top-like: the same coercion (as in the previous

systems) is generated.
This behavior is formalized with a meta-function, denoted as JAKC ,and described in Figure 11.
Finally, the reader may notice how the modified rules still overlap when eA3 d. However, in this case, both rules can be used interchangeably as they both lead to the same coercion. With thischange in the subtyping rules we are able to retain coherence.
Algorithmic disjointness rules The algorithmic disjointness rules
are, again, similar to the ones presented in the original system. In
relation to the simple system with > we placed back ∗→, since welifted the restriction of intersections with function types. We also
had to modify ∗A X(Z →) to include the premise ¬eBd. This is dueto the specification of >-disjointness, which requires two types not
to be top-like in order for them to be disjoint.

7.

Related Work

Merge Operator. Reynolds invented Forsythe [28] in the 1980s.
Forsythe has a merge operator operator p1 , p2 and a coherent semantics. The result was proved formally by Reynolds [27] in alambda calculus with intersection types and a merge operator. He
has four different typing rules for the merge operator, each accounting for various possibilities of what the types of the first and second components are. With those four rules, a merge can only beconstructed when the second component of the merge is either afunction or a (one-field) record. The set of rules is restrictive andit forbids, for instance, the merge of two functions. In λi a merge
can contain, for example two primitive values (which is disallowedin Forsythe). Moreover, except for the variant presented in Section 6.3, multiple functions can co-exist in a merge as long as
they are provably disjoint. The treatment of disjointness of functions is particularly challenging, specially in combination with a >type, and supporting multiple functions (as well as other types) ina merge is a significant innovation over Reynolds’ approach.
Castagna et al. [6] proposed λ& to study the overloading problem for functions. Their calculus contains a special merge operator
that works only for functions. The calculus is coherent. Similarly
to us they impose well-formedness conditions on the formation ofa (functional) merge. However, their well-formedness conditions
cannot be ported to a system with arbitrary intersections like λi ,since those conditions assume function types only. They also show
how to encode records, but it seems that encoding arbitrary merges
and intersections is not possible. For the special case of functional
merges, the conditions that are used in λ& are incomparable in expressive power to those in λi . That is, λ& accepts some functional
merges that λi rejects, and λi accepts some functional merges that
λ& rejects. For example, the functional merge

supertype of two functions that have non-disjoint co-domains. In
λ& the non-existence of arbitrary merges means that it is harder tofind common supertypes of functions, allowing for a more liberal
notion of coherent functional merges.
Our work is largely inspired by Dunfield [14], and throughout
the paper we have already made extensive comparisons with hiswork. He described a similar approach to ours: compiling a system with intersection types and a merge operator into ordinary λcalculus terms with pairs. One major difference is that our systemdoes not include unions. As acknowledged by Dunfield, his calculus lacks coherence. Dunfield also mechanically formalized his
proofs, using the Twelf proof assistant [21]. However he did notprove any results about coherence, so his meta-theoretical results
were not immediately useful to us. Since we were also not familiar
with Twelf, we decided to start a new formalization in Coq (which
we are familiar with), while proving many new results related tocoherence.
Pierce [23] made a comprehensive review of coherence, especially on Curien and Ghelli [10] and Reynolds’ methods of proving coherence; but he was not able to prove coherence for his F∧
calculus. He introduced a primitive glue function as a language
extension which corresponds to our merge operator. However, in
his system users can “glue” two arbitrary values, which can lead toincoherence.
Coherence without Merge. Recently, Castagna et al. [7] studied
a very interesting and coherent calculus that has polymorphismand set-theoretic type connectives (such as intersections, unions,and negations). Unfortunately their calculus does not include amerge operator like ours, which is our major source of difficulty
for achieving coherence.
Going in the direction of higher kinds, Compagnoni and Pierce [8]added intersection types to System Fω and used a new calculus,Fω∧ , to model multiple inheritance. In their system, types include
the construct of intersection of types of the same kind K. Davies
and Pfenning [12] studied the interactions between intersection
types and effects in call-by-value languages. And they proposed a“value restriction” for intersection types, similar to value restriction
on parametric polymorphism. We borrowed the notion of ordinary
types from Davies and Pfenning. Ordinary types play a fundamental role in ensuring coherence in λi . In contrast to λi , none of those
calculi include a merge operator.
There have been attempts to provide a foundational calculus
for Scala that incorporates intersection types [1, 2]. However, thetype-soundness of a minimal Scala-like calculus with intersection
types and parametric polymorphism is not yet proven. Recently,
some form of intersection types has been adopted in object-oriented
languages such as Scala, Ceylon, and Grace. Generally speaking,the most significant difference to λi is that in all those languages
there is no explicit introduction construct like our merge operator.

(Int → Char)&(Int → Bool)

Other Type Systems with Intersection Types. Refinement intersection [11, 13, 17] is the more conservative approach of adoptingintersection types. Refinement intersections usually have a restriction on the formation of an intersection type A&B. In refinement
intersections A&B is a well-formed type if A and B are refinementsof the same simple (unrefined) type. However this is a different restriction from disjointness. Refinement intersection increases only
the expressiveness of types but not terms. But without a term-level
construct like “merge”, it is not possible to encode various language
features.

is accepted in λi but not in λ&. One reason why λi also rejects
some functional intersections, which are accepted in λ&, seems
to be related to the presence of arbitrary merges. As discussed
in Section 5, the combination of contravariance and the presenceof arbitrary merges means that we can always find a common

Coherence in other Type-Directed Mechanisms Other typedirected mechanisms such as type classes [31] and, more generally,
qualified types [19] also require special care to ensure coherence.
For example, in Haskell, a well-known example of ambiguity [18]that could lead to incoherence is:f :: String -> Stringf s = show (read s)
Here the functions read and show have, respectively the types
Read a => String -> a and Show a => a -> String. The
constraints Read a and Show a represent requirements that thecompiler should implicitly infer. That is the compiler should finda suitable implementation of the read and show functions for theparticular type a. The problem is that there is not enough type
information to determine what the type a should be. An arbitrarychoice of a could lead to different code being inferred depending on
the particular choice of a. In this case the behavior of the program
would be dependent on the particular choice made by the compiler.
As a result Haskell compilers, reject programs like the above.
Jones [18] provided a formal treatment of coherence for qualified
types and type classes, designing suitable restrictions that ensurethat incoherent programs are not accepted. In recent versions of
Haskell compilers, it is possible to use type annotations to remove
type ambiguity:
f :: String -> Stringf s = (show :: Int -> String) (read s)
Here the type annotation instantiates a to Int, removing the ambiguity and allowing the program to be accepted. In λi we also useannotations to remove type ambiguity. The bidirectional type system ensures that the additional annotations required in terms are
sufficient to remove any type ambiguity in λi programs.

8.

Conclusion and Future Work

This paper described λi : a coherent and type-safe core calculus thatcombines intersection types and a merge operator. We investigatedthree different variants of λi : two variants with a > type; and another one without. To ensure coherence the type system accepts
only disjoint intersections. For each variant of λi there is a different definition of disjointness. Nevertheless all definitions of disjointness follow the same principle: they are defined in terms of thesubtyping relation; and they describe which common supertypes
are allowed in order for two types to be considered disjoint.
For the future, we would like to study the addition of union
types. This will also require changes in our notion of disjointness,since with union types there always exists a type A|B, which is thecommon supertype of two types A and B, and that is not a top-like
type. Another interesting challenge is to address the combination
between disjoint intersection types and polymorphism. A naive
combination does not seem to be difficult. Since an expression witha polymorphic type can be instantiated to any type, a simple option
is simply to forbid polymorphic variables in intersections. However
this has limited expressiveness, and would prevent many usefulprograms. More thought is needed to achieve more expressiveness.
Finally more work is needed to illustrate the practical applicabilityof this calculus. One direction that we started exploring is thedesign of object-oriented languages with sophisticated multiple
inheritance mechanisms. The idea is to use the merge operator,
combined with fixpoints, to encode multiple inheritance. The roleof disjointness is then to remove the ambiguity caused by multiple
inheritance.

Acknowledgments
We would like to thank the ICFP reviewers for their helpful comments. This work has been sponsored by the Hong Kong Research
Grant Council Early Career Scheme project number 27200514.

References[1] N. Amin, A. Moors, and M. Odersky. Dependent object types. In
19th International Workshop on Foundations of Object-Oriented Languages, 2012.
[2] N. Amin, T. Rompf, and M. Odersky. Foundations of path-dependent
types. In Proceedings of the 2014 ACM International Conference
on Object Oriented Programming Systems Languages & Applications,
2014.
[3] B. E. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and
S. Weirich. Engineering formal metatheory. In G. C. Necula andP. Wadler, editors, Proceeding of the 35th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL), pages
3–15. ACM, 2008.
[4] V. Benzaken, G. Castagna, and A. Frisch. CDuce: An XML-centric
general-purpose language. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP
’03, 2003.
[5] L. Cardelli. A semantics of multiple inheritance. Information andComputation, 76:138–164, 1988.
[6] G. Castagna, G. Ghelli, and G. Longo. A calculus for overloadedfunctions with subtyping. In Proceedings of the 1992 ACM Conferenceon LISP and Functional Programming, LFP ’92, 1992.
[7] G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet, and L. Padovani.
Polymorphic functions with set-theoretic types: Part 1: Syntax, semantics, and evaluation. In Proceedings of the 41st ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL
’14, 2014.
[8] A. B. Compagnoni and B. C. Pierce. Higher-order intersection types
and multiple inheritance. Mathematical Structures in Computer Science, 1996.
[9] M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Mathematical Logic Quarterly, 27(2–6):45–58,
1981.
[10] P.-L. Curienl and G. Ghelli. Coherence of subsumption. In CAAP’90:
15th Colloquium on Trees in Algebra and Programming, Copenhagen,Denmark, May 15-18, 1990, Proceedings, volume 431, page 132.
Springer Science & Business Media, 1990.
[11] R. Davies. Practical refinement-type checking. PhD thesis, Carnegie
Mellon University, 2005.
[12] R. Davies and F. Pfenning. Intersection types and computational
effects. In Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP’00), 2000.
[13] J. Dunfield. Refined typechecking with Stardust. In A. Stump andH. Xi, editors, Programming Languages meets Program Verification(PLPV ’07), Freiburg, Germany, Oct. 2007.
[14] J. Dunfield. Elaborating intersection and union types. Journal of
Functional Programming, 2014.
[15] J. Dunfield and F. Pfenning. Type assignment for intersections andunions in call-by-value languages. In A. Gordon, editor, Foundationsof Software Science and Computation Structures (FOSSACS ’03),
pages 250–266, Warsaw, Poland, Apr. 2003. Springer-Verlag LNCS
2620.
[16] J. Dunfield and F. Pfenning. Tridirectional typechecking. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL ’04, 2004.
[17] T. Freeman and F. Pfenning. Refinement types for ML. In Proceedingsof the SIGPLAN ’91 Symposium on Language Design and Implementation, Toronto, Ontario, June 1991. ACM Press.
[18] M. P. Jones. Coherence for Qualified Types. Technical ReportYALEU/DCS/RR-989, Yale University, 1993.
[19] M. P. Jones. Qualified Types: Theory and Practice. Cambridge
University Press, Cambridge, England, 1994.
[20] M. Odersky et al. An overview of the Scala programming language.
Technical Report IC/2004/64, EPFL Lausanne, Switzerland, 2004.
[21] F. Pfenning and C. Schürmann. System description: Twelf — A metalogical framework for deductive systems. In H. Ganzinger, editor,

Proceedings of the International Conference on Automated Deduction,
pages 202–206, 1999.
[22] B. C. Pierce. Programming with intersection types, union types, andpolymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon
University, 1991.
[23] B. C. Pierce. Programming with Intersection Types and Bounded
Polymorphism. PhD thesis, Carnegie Mellon University, December
1991.
[24] B. C. Pierce. Intersection types and bounded polymorphism. Mathematical Structures in Computer Science, 1997.
[25] B. C. Pierce and D. N. Turner. Local type inference. ACM Trans.
Program. Lang. Syst., 22(1), Jan. 2000.
[26] G. Pottinger. A type assignment for the strongly normalizable λ-terms.
In To H. B. Curry: essays on combinatory logic, lambda calculus andformalism, pages 561–577. Academic Press, London, 1980.
[27] J. C. Reynolds. The coherence of languages with intersection types. In
Proceedings of the International Conference on Theoretical Aspects ofComputer Software, TACS ’91, 1991.
[28] J. C. Reynolds. Design of the Programming Language Forsythe, pages
173–233. Birkhäuser Boston, Boston, MA, 1997.
[29] J. C. Reynolds. Separation logic: A logic for shared mutable data
structures. In Logic in Computer Science, 2002. Proceedings. 17th
Annual IEEE Symposium on, pages 55–74. IEEE, 2002.
[30] S. van Bakel. Complete restrictions of the intersection type discipline.
Theoretical Comput. Sci., 99, 1992.
[31] P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad
hoc. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL ’89, 1989.