Disjoint PolymorphismJoão Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi
The University of Hong Kong
{alpuim,bruno,zyshi}@cs.hku.hk

Abstract. The combination of intersection types, a merge operator andparametric polymorphism enables important applications for programming. However, such combination makes it hard to achieve the desirable
property of a coherent semantics: all valid reductions for the same expression should have the same value. Recent work proposed disjoint intersections types as a means to ensure coherence in a simply typed setting.
However, the addition of parametric polymorphism was not studied.
This paper presents Fi : a calculus with disjoint intersection types, a variant of parametric polymorphism and a merge operator. Fi is both typesafe and coherent. The key difficulty in adding polymorphism is that,when a type variable occurs in an intersection type, it is not staticallyknown whether the instantiated type will be disjoint to other components of the intersection. To address this problem we propose disjoint
polymorphism: a constrained form of parametric polymorphism, whichallows disjointness constraints for type variables. With disjoint polymorphism the calculus remains very flexible in terms of programs that canbe written, while retaining coherence.

1

Introduction

Intersection types [20,43] are a popular language feature for modern languages,
such as Microsoft’s TypeScript [4], Redhat’s Ceylon [1], Facebook’s Flow [3]and Scala [37]. In those languages a typical use of intersection types, which has
been known for a long time [19], is to model the subtyping aspects of OO-stylemultiple inheritance. For example, the following Scala declaration:
class A extends B with C

says that the class A implements both B and C. The fact that A implements twointerfaces/traits is captured by an intersection type between B and C (denoted in
Scala by B with C). Unlike a language like Java, where implements (which plays
a similar role to with) would be a mere keyword, in Scala intersection types are
first class. For example, it is possible to define functions such as:
def narrow(x : B with C) : B = xtaking an argument with an intersection type B with C.
The existence of first-class intersections has led to the discovery of otherinteresting applications of intersection types. For example, TypeScript’s documentation motivates intersection types1 as follows:1

https://www.typescriptlang.org/docs/handbook/advanced-types.html

You will mostly see intersection types used for mixins and other concepts
that don’t fit in the classic object-oriented mold. (There are a lot of thesein JavaScript!)
Two points are worth emphasizing. Firstly, intersection types are being used tomodel concepts that are not like the classical (class-based) object-oriented programming. Indeed, being a prototype-based language, JavaScript has a much
more dynamic notion of object composition compared to class-based languages:
objects are composed at run-time, and their types are not necessarily staticallyknown. Secondly, the use of intersection types in TypeScript is inspired by common programming patterns in the (dynamically typed) JavaScript. This hints
that intersection types are useful to capture certain programming patterns thatare out-of-reach for more conventional type systems without intersection types.
Central to TypeScript’s use of intersection types for modelling such a dynamic form of mixins is the function:function extend<T, U>(first: T, second: U) : T & U {...}The name extend is given as an analogy to the extends keyword commonly usedin OO languages like Java. The function takes two objects (first and second)and produces an object with the intersection of the types of the original objects.
The implementation of extend relies on low-level (and type-unsafe) features of
JavaScript. When a method is invoked on the new object resulting from theapplication of extend, the new object tries to use the first object to answer the
method call and, if the method invocation fails, it then uses the second object
to answer the method call.
The extend function is essentially an encoding of the merge operator. The
merge operator is used on some calculi [48,47,17,24,38] as an introduction form
for intersection types. Similar encodings to those in TypeScript have been proposed for Scala to enable applications where the merge operator also plays afundamental role [39,46]. Unfortunately, the merge operator is not directly supported by TypeScript, Scala, Ceylon or Flow. There are two possible reasons forsuch lack of support. One reason is simply that the merge operator is not wellknown: many calculi with intersection types in the literature do not have explicit
introduction forms for intersection types. The other reason is that, while powerful, the merge operator is known to introduce (in)coherence problems [47,24].
If care is not taken, certain programs using the merge operator do not have aunique semantics, which significantly complicates reasoning about programs.
Solutions to the problem of coherence in the presence of a merge operator
exist for simply typed calculi [48,47,17,38], but no prior work addresses polymorphism. Most recently, we proposed using disjoint intersection types [38] toguarantee coherence in λi : a simply typed calculus with intersection types anda merge operator. The key idea is to allow only disjoint types in intersections.
If two types are disjoint then there is no ambiguity in selecting a value of theappropriate type from an intersection, guaranteeing coherence.
Combining parametric polymorphism with disjoint intersection types, while
retaining enough flexibility for practical applications, is non-trivial. The key issue

is that when a type variable occurs in an intersection type it is not staticallyknown whether the instantiated types will be disjoint to other components of
the intersection. A naive way to add polymorphism is to forbid type variables inintersections, since they may be instantiated with a type which is not disjoint
to other types in an intersection. Unfortunately this is too conservative andprevents many useful programs, including the extend function, which uses anintersection of two type variables T and U.
This paper presents Fi : a core calculus with disjoint intersection types, avariant of parametric polymorphism and a merge operator. The key innovationin the calculus is disjoint polymorphism: a constrained form of parametric polymorphism, which allows programmers to specify disjointness constraints for typevariables. With disjoint polymorphism the calculus remains very flexible in terms
of programs that can be written with intersection types, while retaining coherence. In Fi the extend function is implemented as follows:
let extend T (U * T) (first : T, second : U) : T & U = first ,, second

From the typing point of view, the difference between extend in TypeScript and
Fi is that the type variable U now has a disjointness constraint. The notation
U * T means that the type variable U can be instantiated to any types thatis disjoint to the type T. Unlike TypeScript, the definition of extend is trivial,
type-safe and guarantees coherence by using the built-in merge operator (,,).
The applicability of Fi is illustrated with examples using extend ported fromTypeScript, and various operations on polymorphic extensible records [34,29,31].
The operations on polymorphic extensible records show that Fi can encode various operations of row types [52]. However, in contrast to various existing proposals for row types and extensible records, Fi supports general intersections andnot just record operations.
Fi and the proofs of coherence and type-safety are formalized in the Coq theorem prover [2]. The proofs are complete except for a minor (and trivially true)variable renaming lemma used to prove the soundness between two subtyping
relations used in the formalization. The problem arizes from the combination of
the locally nameless representation of binding [7] and existential quantification,
which prevents a Coq proof for that lemma.
In summary, the contributions of this paper are:
– Disjoint Polymorphism: A novel form of universal quantification wheretype variables can have disjointness constraints. Disjoint polymorphism enables a flexible combination of intersection types, the merge operator andparametric polymorphism.
– Coq Formalization of Fi and Proof of Coherence: An elaboration
semantics of System Fi into System F is given. Type-soundness and coherence
are proved in Coq. The proofs for these properties and all other lemmata
found in this paper are available at:https://github.com/jalpuim/disjoint-polymorphism– Applications: We show how Fi provides basic support for dynamic mixins
and various operations on polymorphic extensible records.

2

Overview

This section introduces Fi and its support for intersection types, parametric polymorphism and the merge operator. It then discusses the issue of coherence andshows how the notion of disjoint intersection types and disjoint quantificationachieves a coherent semantics. This section uses some syntactic sugar, as well as
standard programming language features, to illustrate the various concepts in
Fi . Although the minimal core language that we formalize in Section 4 does notpresent all such features and syntactic sugar, these are trivial to add.
2.1 Intersection Types and the Merge Operator
Intersection types. The intersection of type A and B (denoted by A & B in Fi )contains exactly those values which can be used as both values of type A and oftype B. For instance, consider the following program in Fi :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 anywhere where either avalue of type Int or a value of type Bool is expected. This means that, in the
program above the functions succ and not – simple functions on integers andbooleans, respectively – both accept x as an argument.
Merge operator. The previous program deliberately omitted the introductionof values of an intersection type. There are many variants of intersection types
in the literature. Our work follows a particular formulation, where intersection
types are introduced by a merge operator [48,47,17,24,38]. As Dunfield [24] hasargued a merge operator adds considerable expressiveness to a calculus. The
merge operator allows two values to be merged in a single intersection type. For
example, an implementation of x in Fi is 1,,True. Following Dunfield’s notation
the merge of v1 and v2 is denoted by v1 , , v2 .
2.2

Coherence and Disjointness

Coherence is a desirable property for a semantics. A semantics is coherent if any
valid program has exactly one meaning [47] (that is, the semantics is not ambiguous). Unfortunately the implicit nature of elimination for intersection types builtwith a merge operator can lead to incoherence. This is due to intersections withoverlapping types, as in Int&Int. The result of the program ((1,,2) : Int) canbe either 1 or 2, depending on the implementation of the language.
Disjoint intersection types One option to restore coherence is to reject programs
which may have multiple meanings. The λi calculus [38] – a simply-typed calculus
with intersection types and a merge operator – solves this problem by using theconcept of disjoint intersections. The incoherence problem with the expression
1, , 2 happens because there are two overlapping integers in the merge. Generally
speaking, if both terms can be assigned some type C then both of them can bechosen as the meaning of the merge, which in its turn leads to multiple meanings
of a term. Thus a natural option is to forbid such overlapping values of the same
type in a merge. In λi intersections such as Int&Int are forbidden, since the types
in the intersection overlap (i.e. they are not disjoint). However an intersection
such as Char&Int is ok because the set of characters and integers are disjoint toeach other.
2.3

Parametric Polymorphism

Unfortunately, combining parametric polymorphism with disjoint intersection
types is non-trivial. Consider the following program (uppercase Latin lettersdenote type variables):let merge3 A (x : A) : A & Int = x,,3 in

The merge3 function takes an argument x of some type (A) and merges x with
3. Thus the return type of the program is A & Int. merge3 is unproblematic formany possible instantiations of A. However, if merge3 instantiates A with a typethat overlaps (i.e. is not disjoint) with Int, then incoherence may happen. For
example:merge3 Int 2

can evaluate to both 2 or 3.
Forbidding type variables in intersections A naive way to ensure that only programs with disjoint types are accepted is simply to forbid type variables in intersections. That is, an intersection type such as Char&Int would be accepted, but
an intersection such as A&Int (where A is some type variable) would be rejected.
The reasoning behind this design is that type variables can be instantiated to any
types, including those already in the intersection. Thus forbidding type variablesin the intersection will prevent invalid intersections arising from instantiations
with overlapping types. Such design does guarantee coherence and would prevent
merge3 from type-checking. Unfortunately the big drawback is that the design is
too conservative and many other (useful) programs would be rejected. In particular, the extend function from Section 1 would also be rejected.
Other approaches Another option to mitigate the issues of incoherence, without
the use of disjoint intersection types, is to allow for a biased choice: multiple values of the same type may exist in an intersection, but an implementation gives
preference to one of them. The encodings of merge operators in TypeScript andScala [39,46] use such an approach. A first problem with this approach, which has
already been pointed out by Dunfield [24], is that the choice of the corresponding value is tied up to a particular choice in the implementation. In other words
incoherence still exists at the semantic level, but the implementation makes it
predictable which overlapping value will be chosen. From the theoretical pointof-view it would be much better to have a clear, coherent semantics, which is
independent from concrete implementations. Another problem is that the interaction between biased choice and polymorphism can lead to counter-intuitive
programs, since instantiation of type-variables affects the type-directed lookup
of a value in an intersection.

2.4

Disjoint Polymorphism

To avoid being overly conservative, while still retaining coherence in the presence of parametric polymorphism and intersection types, Fi uses disjoint polymorphism. Inspired by bounded quantification [14], where a type variable isconstrained by a type bound, disjoint polymorphism allows type variables to beconstrained so that they are disjoint to some given types.
With disjoint quantification a variant of the program merge3, which is accepted by Fi , is written as:
let merge3 ( A * Int ) (x : A) : A & Int = x,,3 in

In this variant the type A can be instantiated to any types disjoint to Int. Such
restriction is expressed by the notation A * Int, where the left-side of * denotes
the type variable being declared (A), and the right-side denotes the disjointness
constraint (Int). For example,
merge3 Bool Trueis accepted. However, instantiating A with Int fails to type-check.
Multiple constraints Disjoint quantification allows multiple constraints. For example, the following variant of merge3 has an additional boolean in the merge:
let merge3b ( A * Int & Bool ) (x : A) : A & Int & Bool = x,,3,,True in

Here the type variable A needs to be disjoint to both Int and Bool. In Fi such
constraint is specified using an intersection type Int & Bool. In general, multiple
constraints are specified with an intersection of all required constraints.
Type variable constraints Disjoint quantification also allows type variables to be
disjoint to previously defined type variables. For example, the following programis accepted by Fi :let fst A ( B * A ) (x: A & B) : A = x in . . .

The program has two type variables A and B. A is unconstrained and can beinstantiated with any type. However, the type variable B can only be instantiatedwith types that are disjoint to A. The constraint on B ensures that the intersection
type A & B is disjoint for all valid instantiations of A and B. In other words, only
coherent uses of fst will be accepted. For example, the following use of fst:
fst Int Char (1,,’c’)is accepted since Int and Char are disjoint, thus satisfying the constraint on thesecond type parameter of fst. Furthermore, problematic uses of fst, such as:
fst Int Int (1,,2)

are rejected because Int is not disjoint with Int, thus failing to satisfy the disjointness constraint on the second type parameter of fst.

Empty constraint The type variable A in the fst function has no constraint. In
Fi this actually means that A should be associated with the empty constraint,
which raises the question: which type should be used to represent such empty
constraint? Or, in other words, which type is disjoint to every other type? It
is obvious that this type should be one of the bounds of the subtyping lattice:either ⊥ or >. The essential intuition here is that the more specific a type in thesubtyping relation is, the less types exist that are disjoint to it. For example,
Int is disjoint to all types except the n-ary intersections that contain Int, and⊥; while Int&Char is disjoint to all types that do not contain Int or Char, and⊥. This reasoning implies that > should be treated as the empty constraint.
Indeed, in Fi , a single type variable A is only syntactic sugar for A ∗ >.

3

Applications

Fi is illustrated with two applications. The first application shows how to mimic
some of TypeScript’s examples of dynamic mixins in Fi . The second applicationshows how Fi enables a powerful form of polymorphic extensible records.
3.1

Dynamic Mixins

TypeScript is a language that adds static type checking to JavaScript. Amongst
numerous static typing constructs, TypeScript supports a form of intersection
types, without a merge operator. However, it is possible to define a function
extend that mimics the merge operator:
function extend<T, U>(first: T, second: U): T & U {let result = <T & U>{};for (let id in first) {(<any>result)[id] = (<any>first)[id];}for (let id in second) {if (!result.hasOwnProperty(id)) {(<any>result)[id] = (<any>second)[id];}}return result;}class Person { constructor(public name : string, public male : boolean){ } }interface Loggable { log() : void; }class ConsoleLogger implements Loggable { log() {...} }var jim = extend(new Person("Jim",true), new ConsoleLogger());
var n = jim.name;jim.log();

In this example, taken from TypeScript’s documentation2 , an extend function
is defined for mixin composition. Two classes Person and ConsoleLogger are also2

We have added the field male to the class Person.

defined. Two instances of those classes are then composed in a variable jim withthe type of the intersection of both using extend. It is type-safe to access boththe properties from Person and ConsoleLogger in the object jim.
TypeScript’s implementation of extend relies on a biased choice. The function
starts by creating a variable result with the type of the intersection. It theniterates through first’s properties and copies them to result. Next, it iterates
through second’s properties but it only copies the properties that result does notpossess yet (i.e. the ones present in first). This means that the implementationis left-biased, as the properties of left type of the intersection are chosen infavor of the ones in the right. However, in TypeScript this may be a cause of
severe problems since that, at the time of writing, intersections at type-level areright-biased! For example, the following code is well-typed:class Dog { constructor(public name : string, public male : string) { } }var fool : Dog & Person = extend(new Dog("Pluto","yes"),new
Person("Arnold",true));boolean b = fool.male;/* Undetected type-error here! */There are a few problems here. Firstly both Dog and Person contain a name field,
and the use of extend will favour the name field in the first object. This could
be surprising for someone unfamiliar with the semantics of extend and, more
importantly, it could easily allow unintended name clashes to go undetected.
Secondly, note how fool.male is statically bound to a variable of type booleanbut, at run-time, it will contain a value of type String! Thus the example showssome run-time type errors can still occur when using extend.
Other problematic issues regarding the semantics of intersection types can
include the order of the types in an intersection, or even intersections including repeated types. This motivates the need to define a clear meaning for thepractical application of intersection types.
Dynamic mixins in Fi In Fi , the merge operator is built-in. Thus extend is simply
defined as follows:
let extend T (U * T) (first : T, second : U) : T & U = first ,, second in

The disjointness constraint on U ensures that no conflicts (such as duplicatedfields of the same type) exists when merging the two objects. In practice this approach is quite similar to trait-based OO approaches [50]. If conflicts exist when
two objects are composed, then they have to be resolved manually (by dropping
fields from some object, for example). Moreover if no existing implementation
can be directly reused, a new one must be provided via record extension, analogously to standard method overriding in OO languages.
For the previous TypeScript examples, assuming a straightforward translation from objects to (polymorphic) records, then the composition of person andconsoleLogger is well-typed in Fi :type Person = {name : String} & {male : Bool};type Loggable = {log : > → >};let person (n : String) (s : Bool) : Person = {name = n} ,, {male = s} inlet consoleLogger : Loggable = {log = ...} inlet jim = extend Person Loggable (person "Jim" true)
let n = jim.name in
jim.log >consoleLogger in

However, the intersection Dog & Person is not accepted. This is due to bothtypes sharing a field with the same name (name) and the same type (String).
Note that the name clash between male fields (which have different types) does
not impose any problem in this example: Fi allows and keeps duplicated fields
whose types are disjoint. This feature of Fi is further illustrated next.
3.2

Extensible Records

Fi can encode polymorphic extensible records. Describing and implementing
records within programming languages is certainly not novel and has been extensively studied in the past, including systems with row types [52,53]; predicates[30,29,28]; flags [45]; conditional constraints [42]; cases [10]; amongst others.
However, while most systems have non-trivial built-in constructs to model various aspects of records, Fi specializes the more general notion of intersection
types to encode complex records.
Records and record operations in Fi Systems with records usually rely on 3
basic operations: selection, restriction and extension/concatenation. Selection
and concatenation (via the merge operator) are built-in in the semantics of Fi .
Merges in Fi can be viewed as a generalization of record concatenation. In Fi ,following well-known encodings of multi-field records in systems with intersection
types and a merge operator [48,47], there are only three rather simple constructs
for records: 1) single field record types; 2) single field records; 3) field accessors.
Multi-field records in Fi are encoded with intersections and merges of single fieldrecords. An example is already illustrated in Section 3.1. The record type Personis the intersection of two single field record types. The record person "Jim" trueis built with a merge of two single field records. Finally, jim.name and jim.log
illustrates the use of field accessors. Note how, through the use of subtyping,accessors will accept any intersection type that contains the single record withthe corresponding field. This resembles systems with record subtyping [15,41].
Restriction via subtyping In contrast to most record systems, restriction is notdirectly embedded in Fi . Instead, Fi uses subtyping for restriction:
let remove (x : {age : Int} & {name : String}) : {name : String} = x in . . .

The function remove drops the field age from the record x.
Polymorphic extensible records Records in Fi can have polymorphic fields, anddisjointness enables encoding various operations expressible in systems withpolymorphic records. For example, the following variant of remove
let remove A (B * {l : A}) (x : { l : A } & B) : B = x in . . .

takes a value x which contains a record of type l : A, as well as some extra
information of type B. The disjointness constraint on B ensures that values oftype B do not contain a record with type l : A. This example shows that one
can use disjoint quantification to express negative field information, which is very
close to the system described by Harper and Pierce [29]. Note, however, that Fi
requires explicitly stating the type of field in the constraint, whereas systems
with a lacks (field) predicate only require the name of the field. The generalityof disjoint intersection types, which allows one to encode record types, is exactly
what forces us to add this extra type in the constraint. However, there is a slightgain with Fi ’s approach: remove allows B to contain fields with label l, as longas the field types are disjoint to A. Such fine-grained constraint is not possible
to express only with a lacks predicate.
Expressibility As noted by Leijen [34], systems can typically be categorized into
two distinct groups in what concerns extension: strict and free. The former does
not allow field overriding when extending a record (i.e. one can only extend arecord with a field that is not present in it); while the latter does account forfield overriding. Our system can be seen as hybrid of these two kinds of systems.
With lightweight extensible records [31] – a system with strict extension – anexample of a function that uses record types is the following:
let avg1 (R\x, R\y) => (r : {R | x:Int, y:Int}) = (r.x+r.y)/2

The type signature says that any record r, containing fields x and y and somemore information R (which lacks both fields x and y), can be accepted returning
an integer. Note how the bounded polymorphism is essential to ensure that R
does not contain x nor y.
On the other hand, in Leijen’s [34] system with free extension the moregeneral program would be accepted:
let avg2 R (r : {x:Int, y:Int | R}) = (r.x+r.y)/2

In this case, if R contains either field x or field y, they would be shadowed by thelabels present in the type signature. In other words, in a record with multiple x
fields, the most recent (i.e. left-most) is used in any function which accesses x.
In Fi the following program can written instead:
let avg3 (R*{x:Int}&{y:Int}) (r : {x:Int}&{y:Int}&R) = (r.x+r.y)/2

Since Fi accepts duplicated fields as long as the types of the overlapping fields
are disjoint, more inputs are accepted by this function than in the first system.
However, since Leijen’s system accepts duplicated fields even when types areoverlapping, avg3 accepts less types than avg2 . Another major difference between
Fi and the two other mentioned systems, is the ability to combine records with
arbitrary types. Our system does not account for well-formedness of record types
as the other two systems do (i.e. using a special row kind), since our encodingof records piggybacks on the more general notion of disjoint intersection types.

4

The Fi Calculus

This section presents the syntax, subtyping, and typing of Fi : a calculus with intersection types, parametric polymorphism, records and a merge operator. This
calculus is an extension of the λi calculus [38], which is itself inspired by Dunfield’s calculus [24]. Fi extends λi with (disjoint) polymorphism. Section 5 introduces the necessary changes to the definition of disjointness presented by
Oliveira et al. [38] in order to add disjoint polymorphism.
4.1

SyntaxThe syntax of Fi (with the differences to λi highlighted in gray) is:
Types

A, B::= > | Int | A → B | A&B | α | ∀(α ∗ A). B | {l : A}

Terms

e

Contexts Γ::= > | i | x | λx. e | e1 e2 | e1 , , e2 | Λ(α ∗ A). e | e A | {l = e} | e.l::= · | Γ, α ∗ A | Γ, x : A

Types. Metavariables A, B range over types. Types include all constructs in λi :a top type >; the type of integers Int; function types A → B; and intersection
types A&B. The main novelty are two standard constructs of System F used tosupport polymorphism: type variables α and disjoint (universal) quantification∀(α∗A). B. Unlike traditional universal quantification, the disjoint quantification
includes a disjointness constraint associated to a type variable α. Finally, Fi also
includes singleton record types, which consist of a label l and an associated type
A. We will use [α := A] B to denote the capture-avoiding substitution of A forα inside B and ftv(·) for sets of free type variables.
Terms. Metavariables e range over terms. Terms include all constructs in λi : acanonical top value >; integer literals i; variables x, lambda abstractions (λx. e);applications (e1 e2 ); and the merge of terms e1 and e2 denoted as e1, , e2.
Terms are extended with two standard constructs in System F: abstraction oftype variables over terms Λ(α ∗ A). e; and application of terms to types e A. The
former also includes an extra disjointness constraint tied to the type variable
α, due to disjoint quantification. Singleton records consists of a label l and an
associated term e. Finally, the accessor for a label l in term e is denoted as e.l.
Contexts. Typing contexts Γ track bound type variables α with disjointness
constraints A; and variables x with their type A. We will use [α := A] Γ todenote the capture-avoiding substitution of A for α in the co-domain of Γ where
the domain is a type variable (i.e all disjointness constraints). Throughout thispaper, we will assume that all contexts are well-formed. Importantly, besides
usual well-formedness conditions, in well-formed contexts type variables must
not appear free within its own disjointness constraint.
Syntactic sugar In Fi we may quantify a type variable and omit its constraint.
This means that its constraint is >. For example, the function type ∀α.α → α issyntactic sugar for ∀(α ∗ >). α → α. This is discussed in more detail in Section 6.

A ordinary
Int ordinary

A → B ordinary∀(α ∗ B). A ordinary

α ordinary{l : A} ordinary
A <: B ,→ E
A1 <: A2 ,→ E1
A <: > ,→ λx. ()S>

A1 <: A3 ,→ E2

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

Int <: Int ,→ λx. x

SZ

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

A <: B ,→ E
{l : A} <: {l : B} ,→ E

SRec

Sα

S&L1

A3 ordinary

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

α <: α ,→ λx. x

A3 ordinary

S&R

A2 <: B2 ,→ E2

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

B1 <: B2 ,→ E1

S&L2

S→

A2 <: A1 ,→ E2∀(α ∗ A1 ). B1 <: ∀(α ∗ A2 ). B2 ,→ λf. Λα. E1 (f α)S∀

Fig. 1. Subtyping rules of Fi .

4.2

Subtyping

The subtyping rules of the form A <: B are shown in Figure 1. At the moment,
the reader is advised to ignore the gray-shaded parts, which will be explainedlater. Some rules are ported from λi : S>, SZ, S→, S&R, S&L1 and S&L2 .
Polymorphism and Records. The subtyping rules introduced by Fi refer to polymorphic constructs and records. Sα defines subtyping as a reflexive relation ontype variables. In S∀ a universal quantifier (∀) is covariant in its body, andcontravariant in its disjointness constraints. The SRec rule says that records
are covariant within their fields’ types. The subtyping relation uses an auxiliary unary ordinary relation, which identifies types that are not intersections.
The ordinary conditions on two of the intersection rules are necessary to produce unique coercions [38]. The ordinary relation needs to be extended withrespect to λi . As shown at the top of Figure 1, the new types it contains aretype variables, universal quantifiers and record types.
Properties of Subtyping. The subtyping relation is reflexive and transitive.

Lemma 1 (Subtyping reflexivity). For any type A, A <: A.
Proof. By structural induction on A.



Lemma 2 (Subtyping transitivity). If A <: B and B <: C, then A <: C.
Proof. By double induction on both derivations.

4.3 Typing
Well-formedness. The well-formedness rules are shown in the top part of Figure 2. The new rules over λi are WFα and WF∀. Their definition is quite
straightforward, but note that the constraint in the latter must be well-formed.
Typing rules. Our typing rules are formulated as a bi-directional type-system.
Just as in λi , this ensures the type-system is not only syntax-directed, but alsothat there is no type ambiguity: that is, inferred types are unique. The typing
rules are shown in the bottom part of Figure 2. Again, the reader is advised
to ignore the gray-shaded parts, as these will be explained later. The typing
judgements are of the form: Γ ` e ⇐ A and Γ ` e ⇒ A. They read: “inthe typing context Γ , the term e can be checked or inferred to type A”, respectively. The rules ported from λi are the check rules for > (T-Top), integers(T-Int), variables (T-Var), application (T-App), merge operator (T-Merge),
annotations (T-Ann); and infer rules for lambda abstractions (T-Lam), and thesubsumption rule (T-Sub).
Disjoint quantification. The new rules, inspired by System F, are the infer rules
for type application T-TApp, and for type abstraction T-BLam. Type abstraction is introduced by the big lambda Λ(α ∗ A). e, eliminated by the usual typeapplication e A (T-TApp). The disjointness constraint is added to the context in
T-BLam. During a type application, the type system makes sure that the typeargument satisfies the disjointness constraint. Type application performs an extra check ensuring that the type to be instantiated is compatible (i.e. disjoint)with the constraint associated with the abstracted variable. This is important,as it will retain the desired coherence of our type-system; and it will be further
explained in Section 5. For ease of discussion, also in T-BLam, we require thetype variable introduced by the quantifier to be fresh. For programs with typevariable shadowing, this requirement can be met straightforwardly by variable
renaming.
Records. Finally, T-Rec and T-ProjR deal with record types. The former infers
a type for a record with label l if it can infer a type for the inner expression; thelatter says if one can infer a record type {l : A} from an expression e, then it issafe to access the field l, and inferring type A.

5

Disjointness

Section 4 presented a type system with disjoint intersection types and disjoint
quantification. In order to prove both type-safety and coherence (in Section 6),Γ `AΓ ` Int

Γ `>

α∗A∈Γ
WFα
Γ `α

WFZ

Γ `A
WFR
Γ ` {l : A}Γ ` A Γ, α ∗ A ` B
WF∀Γ ` ∀(α ∗ A). B

WF>Γ ` e ⇒ A ,→ EΓ ` > ⇒ > ,→ ()Γ `AΓ `A Γ `BWF→Γ `A→BΓ `B Γ `A∗B
WF&
Γ ` A&B

e synthesizes type A

T-TopΓ ` e ⇐ A ,→ E

x:A ∈ ΓT-Var
Γ ` x ⇒ A ,→ xΓ ` e : A ⇒ A ,→ EΓ ` e1 ⇒ A1 → A2 ,→ E1

Γ ` e2 ⇐ A1 ,→ E2Γ `AΓ ` e ⇒ ∀(α ∗ B). C ,→ E

T-Ann

T-App

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

T-TAppΓ ` e A ⇒ [α := A] C ,→ E |A|Γ ` e2 ⇒ B ,→ E2

Γ ` e1 ⇒ A ,→ E1

T-Int

Γ ` i ⇒ Int ,→ i

Γ `A∗B
T-MergeΓ ` e1 , , e2 ⇒ A&B ,→ (E1 , E2 )Γ ` e ⇒ A ,→ E
T-Rec

Γ ` {l = e} ⇒ {l : A} ,→ EΓ `A

Γ ` e ⇒ {l : A} ,→ EΓ ` e.l ⇒ A ,→ E

Γ, α ∗ A ` e ⇒ B ,→ E

α 6∈ ftv(Γ )T-BLamΓ ` Λ(α ∗ A). e ⇒ ∀(α ∗ A). B ,→ Λα. E
Γ ` e ⇐ A ,→ EΓ `Ae checks against given type A

Γ, x : A ` e ⇐ B ,→ EΓ ` λx. e ⇐ A → B ,→ λx. EΓ ` e ⇒ A ,→ E

T-ProjR

A <: B ,→ Esub

T-Lam

Γ `B

Γ ` e ⇐ B ,→ Esub E
Fig. 2. Well-formedness and type system of Fi .

T-SubΓ `A∗BΓ `>∗AD>Γ `A∗>

D>Sym

α∗A∈Γ
A <: BDαΓ `α∗BΓ, α ∗ A1 &A2 ` B ∗ CD∀Γ ` ∀(α ∗ A1 ). B ∗ ∀(α ∗ A2 ). Cα∗A∈ΓA <: BDαSymΓ `B∗αΓ `A∗BDRec=Γ ` {l : A} ∗ {l : B}

l1 6= l2
DRec6=
Γ ` {l1 : A} ∗ {l2 : B}Γ ` A2 ∗ B2
D→
Γ ` A1 → A2 ∗ B1 → B2

Γ ` A1 ∗ B
Γ ` A2 ∗ B
D&LΓ ` A1 &A2 ∗ B

Γ ` A ∗ B1
Γ ` A ∗ B2
D&R
Γ ` A ∗ B1 &B2A ∗ax BDAx
Γ `A∗BA ∗ax BB ∗ax ADAx SymA ∗ax BInt ∗ax A1 → A2

Int ∗ax ∀(α ∗ B1 ). B2
A1 → A2 ∗ax {l : B}

DAx (Z∀)

DAx (→ Rec)DAx (Z →)Int ∗ax {l : A}

A1 → A2 ∗ax ∀(α ∗ B1 ). B2∀(α ∗ A1 ). A2 ∗ax {l : B}

DAx (ZRec)

DAx (→ ∀)DAx (∀Rec)

Fig. 3. Algorithmic disjointness.

it is necessary to first introduce a notion of disjointness, considering polymorphism and disjointness quantification. This section presents an algorithmic setof rules for determining whether two types are disjoint. After, it will show a few
important properties regarding substitution, which will turn out to be crucial
to ensure both type-safety and coherence. Finally, it will discuss the bounds of
disjoint quantification and what implications they have on Fi .
5.1

Algorithmic Rules for Disjointness

The rules for the disjointness judgement are shown in Figure 3, which consistsof two judgements.
Main judgement. The judgement Γ ` A ∗ B says two types A and B are disjoint
in a context Γ . The rules are inspired in the disjointness algorithm described byλi . D> and D>Sym say that any type is disjoint to >. This is a major difference
to λi , where the notion of disjointness explicitly forbids the presence of > types
in intersections. We will further discuss this difference in Section 6.

Type variables are dealt with two rules: Dα is the base rule; and DαSym is
its twin symmetrical rule. Both rules state that a type variable is disjoint to some
type B, if Γ contains any subtype of the corresponding disjointness constraint.
This rule is a specialization of the more general lemma:
Lemma 3 (Covariance of disjointness). If Γ ` A ∗ B and B <: C, thenΓ ` A ∗ C.
Proof. By double induction, first on the disjointness derivation and then on thesubtyping derivation. The first induction case for Dα does not need the second
induction as it is a straightforward application of subtyping transitivity.
The lemma states that if a type A is disjoint to B under Γ , then it is also
disjoint to any supertype of B. Note how these two variable rules would allow one
to prove α ∗ α, for any variable α. However, under the assumption that contexts
are well-formed, such derivation is not possible as α cannot occur free in A.
The rule for disjoint quantification D∀ is the most interesting. To illustrate
this rule, consider the following two types:(∀(α ∗ Int). Int&α)(∀(α ∗ Char). Char&α)

When are these two types disjoint? In the first type α cannot be instantiatedwith Int and in the second case α cannot be instantiated with Char. Therefore for both bodies to be disjoint, α cannot be instantiated with either Int
or Char. The rule for disjoint quantification adds a constraint composed of theintersection of both constraints into Γ and checks for disjointness in the bodies
under that environment. The reader might notice how this intersection does notnecessarily need to be well-formed, in the sense that the types that compose it
might not be disjoint. This is not problematic because the intersections present
as constraints in the environment do not contribute directly to the (coherent)
coercions generated by the type-system. In other words, intersections play two
different roles in Fi , as:
1. Types: restricted (i.e. disjoint) intersections are required to ensure coherence.
2. Constraints: arbitrary intersections are sufficient to serve as constraints
under polymorphic instantiation.
The rules DRec= and DRec6= define disjointness between two single label
records. If the labels coincide, then the records are disjoint whenever their fields’
types are also disjoint; otherwise they are always disjoint. Finally, the remaining
rules are identical to the original rules.
Axioms. Axiom rules take care of two types with different language constructs.
These rules capture the set of rules is that A ∗ax B holds for all two types ofdifferent constructs unless any of them is an intersection type, a type variable,or >. Note that disjointness with type variables is already captured by Dα andDαSym, and disjointness with the > type is captured by D> and D>Sym.

5.2

Well-formed Types

In Fi it is important to show that the type-system only produces well-formed
types. This is crucial to ensure coherence, as shown in Section 6. However, inthe presence of both polymorphism and disjoint intersection types, extra effort
is needed to show that all types in Fi are well-formed. To achieve this, not only
we need to show that a weaker version of the general substitution lemma holds,
but also that disjointness between two types is preserved after substitution. To
motivate the former (i.e. why general substitution does not hold in Fi ), consider
the type ∀(α ∗ Int). (α&Int). The type variable α cannot be substituted by any
type: substituting with Int will lead to the ill-formed type Int&Int. To motivate
the latter, consider the judgement α∗Int ` α∗Int. After the substitution of Int
for α on the two types, the sentence α ∗ Int ` Int ∗ Int is no longer true, since
Int is clearly not disjoint with itself. Generally speaking, a careless substitution
can violate the constraints in the context. However, if appropriate disjointness
pre-conditions are met, then disjointness can be preserved. More formally, thefollowing lemma holds:
Lemma 4 (Disjointness is stable under substitution). If (α ∗ D) ∈ Γ andΓ ` C ∗ D and Γ ` A ∗ B and well-formed context [α := C] Γ , then [α := C] Γ `[α := C] A ∗ [α := C] B.
Proof. By induction on the disjointness derivation of C and D. Special attention is needed for the variable case, where it is necessary to prove stability of
substitution for the subtyping relation. It is also needed to show that, if C and
D do not contain any variable x, then it is safe to make a substitution in the
co-domain of the environment.

We can now prove a weaker version of the general substitution lemma:
Lemma 5 (Types are stable under substitution). If Γ ` A and Γ ` B and(α ∗ C) ∈ Γ and Γ ` B ∗ C and well-formed context [α := B] Γ , then [α := B] Γ `[α := B] A.
Proof. By induction on the well-formedness derivation of A. The intersection
case requires the use of Lemma 4. Also, the variable case required proving that
if α does not occur free in A, and it is safe to substitute it in the co-domain ofΓ , then it is safe to perform the substitution.

Now we can finally show that all types produced by the type-system are wellformed and, more specifically, justify that the disjointness premise on T-TApp
is sufficient for that purpose. More formally, we have that:
Lemma 6 (Well-formed typing). We have that:– If Γ ` e ⇐ A, then Γ ` A.
– If Γ ` e ⇒ A, then Γ ` A.
Proof. By induction on the derivation and applying Lemma 5 in the case of TTApp.
Even though the meta-theory is consistent, we can still ask: what are thebounds of disjoint quantification? In other words, which type(s) can be used toallow unrestricted instantiation, and which one(s) will completely restrict instantiation? As the reader might expect, the answer is tightly related to subtyping.
5.3

Bounds of Disjoint Quantification

Substitution raises the question of what range of types can be instantiated for agiven variable α, under a given context Γ . To answer this question, we ask thereader to recall the rule Dα, copied below:α∗A∈ΓA <: BDαΓ `α∗B
Given that the cardinality of Fi ’s types is infinite, for the sake of this example
we will restrict the type universe to a finite number of primitive types (i.e.
Int and String), disjoint intersections of these types, > and ⊥. Now we may
ask: how many suitable types are there to instantiate α with, depending on A?
The rule above tells us that the more super-types A has, the more types α has
to be disjoint with. In other words, the choices for instantiating α are inversely
proportional to the number of super-types of A. It is easy to see that the numberof super-types of A is directly proportional to the number of intersections in A.
For example, taking A as Int leads B to be either > or Int; whereas A as
Int&String leaves B as either >, Int or String. Thus, the choices of α areinversely proportional to the number of intersections in A. By analogy, one may
think of a disjointness constraint as a set of (forbidden) types, where primitive
types are the singleton set and each & is the set union. Following the same logic,
choosing > (i.e. the 0-ary intersection) as constraint leaves α with the mostoptions for instantiation; whereas ⊥ (i.e. the infinite intersection) will deliver the
least options. Consequently, we may conclude that > is the empty constraint:
a variable associated to it can be instantiated to any well-formed type. It is a
subtle but very important property, since Fi is a generalization of System F.
Any type variable quantified in System F, can be quantified equivalently in Fi
by assigning it a > disjointness constraint (as seen in Section 2.4).

6

Semantics, Coherence and Type-Safety

This section discusses the elaboration semantics of Fi and proves type-safety andcoherence. It will first show how the semantics is described by an elaboration
to System F. Then, it will discuss the necessary extensions to retain coherence,
namely in the coercions of top-like types; coercive subtyping, and bidirectional
type-system’s elaboration.
6.1

Target Language

The dynamic semantics of the call-by-value Fi is defined by means of a typedirected translation to an extension of System F with pairs. The syntax and

|Γ | = G

|A| = T|α| = α|>| = ()
|A1 → A2 | = |A1 | → |A2 ||∀(α ∗ A). B| = ∀α. |B||A1 &A2 | = (|A1 |, |A2 |)|{l : A}| = |A||·| = ·
|Γ, α ∗ A| = |Γ |, α|Γ, α : A| = |Γ |, α : |A|

Fig. 4. Type and context translation.

typing of our target language is unsurprising:Types

T ::= α | Int | T1 → T2 | ∀α. T | () | (T1 , T2 )Terms E ::= x | i | λx. E | E1 E2 | Λα. E | E T | () | (E1 , E2 ) | proj1 E | proj2 E
Contexts G ::= · | G, α | G, x : T
The highlighted part shows its difference with the standard System F. The interested reader can find the formalization of the full target language syntax andtyping rules in our Coq development.
Type and context translation. Figure 4 defines the type translation function |·|from Fi types A to target language types T . The notation |·| is also overloaded
for context translation from Fi contexts Γ to target language contexts G.
6.2 Coercive Subtyping and Coherence
Coercive subtyping. The judgement A1 <: A2 ,→ E present in Figure 1, extends
the subtyping relation with a coercion on the right hand side of ,→ . A coercion
E is just a term in the target language and is ensured to have type |A1 | → |A2 |(by Lemma 7). For example, Int&α <: α ,→ λx. proj2 x , generates a target
coercion function with type: (Int, α) → α.
Rules S>, Sα, SZ, S→, S&L1 , S&L2 , and S&R are taken directly from λi . In
rule Sα, the coercion is simply the identity function. Rule S∀ elaborates disjoint
quantification, reusing only the coercion of subtyping between the bodies of bothtypes. Rule SRec elaborates records by simply reusing the coercion generated
between the inner types. Finally, all rules produce type-correct coercions:Lemma 7 (Subtyping rules produce type-correct coercions). If A1 <:A2 ,→ E , then · ` E : |A1 | → |A2 |.
Proof. By a straightforward induction on the derivation.
Unique coercions In order to prove the type-system coherent, the subtyping
relation also needs to be shown coherent. In Fi the following lemma holds:
Lemma 8 (Unique subtype contributor). If A1 &A2 <: B, where A1 &A2and B are well-formed types, and B is not top-like, then it is not possible thatthe following holds at the same time:

eAd

e>d

T L>

eAd
eBd
T L&
eA&Bd

eBd
TL →
eA → BdeAd
T LRece{l : A}deAd
T L∀e∀(α ∗ B). Ad
JAKC = T
JAKC =

JAK = T
eAd
JAK
otherwise C

J>K = ()
JA1 → A2 K = λx. JA2 K
JA1 &A2 K = (JA1 K, JA2 K)
J{l : A}K = JAKJ∀(α ∗ B). AK = Λα. JAK

Fig. 5. Top-like types and their coercions.

1. A1 <: B
2. A2 <: B
Proof. By double induction: the first on the disjointness derivation (which follows
from A1 &A2 being well-formed); the second on type B. The variable cases Dα
and DαSym needed to show that, for any two well-formed and disjoint types A
and B, and B is not toplike, then A cannot be a subtype of B.
Using this lemma, we can show that the coercion of a subtyping relation
A <: B is uniquely determined. This fact is captured by the following lemma:
Lemma 9 (Unique coercion). If A <: B ,→ E1 and A <: B ,→ E2 , where
A and B are well-formed types, then E1 ≡ E2 .
Proof. By induction on the first derivation and case analysis on the second. 
6.3

Top-like Types and their Coercions

Lemma 8, which is fundamental in the proof of coherence of subtyping, holds
under the condition that B is not a top-like type. Top-like types in Fi include >as well as other syntactically different types that behave as > (such as >&>).
It is easy to see that the unique subtyping contributor lemma is invalidated if
no restriction on top-like types exists. Since every type is a subtype of > then,without the restriction, the lemma would never hold.
Rules. Fi ’s definition of top-like types extends that from λi . The rules thatcompose this unary relation, denoted as e.d, are presented at the top of Figure 5.
The new rules are T LRec and T L∀. Both rules say that their constructs are toplike whenever their enclosing expressions are also top-like.

Coercions for top-like types Coercions for top-like types require special treatment
for retaining coherence. Although Lemma 8 does not hold for top-like types,
we can still ensure that that any coercions for top-like types are unique, even
if multiple derivations exist. The meta-function JAK, shown at the bottom of
Figure 5, defines coercions for top-like types. With respect to λi the record and∀ cases are now defined, and there is also a change in the & case (covering
types such as >&>). With this definition, although two derivations exist for
type Char&Int <: >, they both generate the coercion λx.().
Allowing overlapping top-like types in intersections In Fi >&> is a well-formed
disjoint intersection type. This may look odd at first, since all other types cannot
appear more than once in an intersection. Indeed, in λi , >&> is not well-formed.
However, >-types are special in that they have a unique canonical top value,
which is translated to the unit value () in the target language. In other words
a merge of two >-types will always return the same value regardless of which
component of the merge is chosen. This is different from merges of non >-types,
which do not have this property. Thus, one may say that >-types are coherent
with every other type. This property makes >-types perfect candidates for theempty constraint, but such can only be achieved by allowing > in intersections.
This explains the more liberal treatment of top types Fi when compared to λi .
6.4

Elaboration of the Type-System and Coherence

In order to prove the coherence result, we refer to the bidirectional type-system
introduced in Section 4. The bidirectional type-system is elaborating, producing
a term in the target language while performing the typing derivation.
Key idea of the translation. This translation turns merges into usual pairs, similar to Dunfield’s elaboration approach [24]. It also translates the form of disjoint
quantification and disjoint type application into regular (polymorphic) quantification and type application. For example, Λ(α ∗ Int). λx. (x, , 1) in Fi will betranslated into System F’s Λα. λx. (x, 1).
The translation judgement. The translation judgement Γ ` e : A ,→ E extends
the typing judgement with an elaborated term on the right hand side of ,→ .
The translation ensures that E has type |A|. The two rules for type abstraction(T-BLam) and type application (T-TApp) generate the expected corresponding coercions in System F. The coercions generated for T-Rec and T-ProjR
simply erase the labels and translate the corresponding underlying term. All theremaining rules are ported from λi .
Type-safety The type-directed translation is type-safe. This property is capturedby 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|.

Proof. By structural induction on the term and the respective inference rule. 
Theorem 2 (Type safety). If e is a well-typed Fi term, then e evaluates tosome System F value v.
Proof. Since we define the dynamic semantics of Fi in terms of the compositionof the type-directed translation and the dynamic semantics of System F, typesafety follows immediately.
Uniqueness of type-inference An important property of the bidirectional typechecking is that, given an expression e, if it is possible to infer a type for it, thene has a unique type.
Theorem 3 (Uniqueness of type-inference). If Γ ` e ⇒ A1 ,→ E1 andΓ ` e ⇒ A2 ,→ E2 , then A1 = A2 .
Proof. By structural induction on the term and the respective inference rule. 
Coherency of Elaboration Combining the previous results, we are finally able toshow the central theorem:
Theorem 4 (Unique elaboration). We have that:– If Γ ` e ⇒ A ,→ E1 and Γ ` e ⇒ A ,→ E2 , then E1 ≡ E2 .
– If Γ ` e ⇐ A ,→ E1 and Γ ` e ⇐ A ,→ E2 , then E1 ≡ E2 .
(“≡” means syntactical equality, up to α-equality.)
Proof. By induction on the first derivation. The most important case is the
subsumption rule:Γ ` e ⇒ A ,→ E

A <: B ,→ EsubΓ ` e ⇐ B ,→ Esub E

Γ `B
T-Sub

We need to show that Esub is unique (by Lemma 9), and thus to show that
A is well-formed (by Lemma 6). Note that this is the place where stability of
substitutions (used by Lemma 6) plays a crucial role in guaranteeing coherence.
We also need to show that A is unique (by Theorem 3). Uniqueness of A isneeded to apply the induction hypothesis.
7

Related WorkIntersection types, polymorphism and the merge operator. To our knowledge
no previous work presents a coherent calculus which includes parametric polymorphism, intersection types and a merge operator. Only Pierce’s F∧ [40] supports intersection types, polymorphism and, as an extension, the merge operator(called glue in F∧ ). However, with such extension, F∧ is incoherent. Various
simply typed systems with intersections types and a merge operator have beenstudied in the past. The merge operator was first introduced by Reynold’s in
the Forsythe [48] language. The merge operator in Forsythe is coherent [47],but it has various restrictions to ensure coherence. For example Forsythe merges
cannot contain more than one function. Many of those restrictions are lifted in
Fi . Castagna et al. [17] studied a coherent calculus with a special merge operator that works on functions only. The goal was to model function overloading.
Unlike Reynold’s operator, multiple functions are allowed in merges, but nonfunctional types are forbidden. More recently, Dunfield [24] formalised a systemwith intersection types and a merge operator with a type-directed translation
to the simply-typed lambda calculus with pairs. Although Dunfield’s calculus isincoherent, it was the inspiration for the λi calculus [38], which Fi extends.
λi solves the coherence problem for a calculus similar to Dunfield’s, by requiring that intersection types can only be composed of disjoint types. λi uses a
specification for disjointness, which says that two types are disjoint if they do notshare a common supertype. Fi does not use such specification as its adaptation
to polymorphic types would require using unification, making the specification
arguably more complex than the algorithmic rules (and defeating the purpose of
having a specification). Fi ’s notion of disjointness is based on λi ’s more general
notion of disjointness concerning > types, called >-disjointness. >-disjointness
states that two types A and B are disjoint if two conditions are satisfied:
1. (not eAd) and (not eBd)
2. ∀C. if A <: C and B <: C then eCd
A significant difference between the Fi and λi , is that >-disjointness does notallow > in intersections, while Fi allows this. In other words, condition (1) is
not imposed by Fi . As a consequence, the set of well-formed top-like types is asuperset of λi ’s. This is covered in greater detail in Section 6.3.
Intersection types and polymorphism, without the merge operator. Recently,
Castagna et al. [18] studied a coherent calculus that has polymorphism and settheoretic type connectives (such as intersections, unions, and negations). Theircalculus is based on a semantic subtyping relation due to their interpretationof intersection types. The difference to Fi , is that their intersections are used
between function types, allowing overloading (i.e. branching) of types. For example, they can express a function whose domain is defined on any type, but
executes different code depending on that type:λ(Int→Bool)∧(α\Int→α\Int) x.(x ∈ Int)?(x mod 2) = 0 : x
In our system we cannot express some of these intersections, namely the ones that
do not have disjoint co-domains. However, Fi accepts other kinds of intersections
which are not possible to express in their calculus. For example merges with
type (Int → Bool)&(Int → Int) are accepted in Fi . Similarly to Castagna
et al. previous work [17], their work is focused on combining intersections withfunctions (but without a merge operator), whereas Fi is concerned with merges
between arbitrary types. Nevertheless, both systems need to express negative
information about type variables. That is, which types a given variable cannot be
instantiated to. In their calculus, difference takes this role (i.e. α\Int); whereas
in Fi , one can express it using disjoint quantification (i.e. ∀(α ∗ Int). . . .).

Going in the direction of higher kinds, Compagnoni and Pierce [19] addedintersection types to System Fω and used a new calculus, Fω∧ , to model multiple
inheritance. In their system, types include the construct of intersection of typesof the same kind K. Davies and Pfenning [22] studied the interactions between
intersection types and effects in call-by-value languages. They proposed a “value
restriction” for intersection types, similar to value restriction on parametric polymorphism. None of these calculi has a merge operator.
Recently, some form of intersection types has been adopted in object-oriented
languages such as Scala [37], TypeScript [4], Flow [3], Ceylon [1], and Grace [9].
There is also a foundational calculus for Scala that incorporates intersection
types [49]. The most significant difference between Fi and those languages/calculi
is that they have no explicit introduction construct like our merge operator. The
lack of a native merge operator leads to several ad-hoc solutions for defining amerge operator in those languages, as discussed in Sections 1 and 3.1.
Extensible records. The encoding of multi-field records using intersection types
and the merge operator first appeared in Forsythe [48]. Castagna et al. [17]propose an alternative encoding for records. Similarly to Fi ’s treatment of elaborating records is Cardelli’s work [13] on translating a calculus with extensible
records (F<:ρ ) to a simpler calculus without records primitives (F<: ). However,
he does not encode multi-field records as intersections/merges hence his translation is more heavyweight. Crary [21] used intersection types and existential
types to address the problem arising from interpreting method dispatch as selfapplication, but he did not use intersection types to encode multi-field records.
Wand [52] started the work on extensible records and proposed row types [53]for records, together with a concatenation operator, which is used in many calculi with extensible records [29,44,53,51,35,42]. Cardelli and Mitchell [15] defined
three primitive operations on records that are also standard in type-systems withrecord types: selection, restriction, and extension. Several calculi are based onthese three primitive operators (especially extension) [45,28,31,33,34,10]. The
merge operator in Fi generalizes the concatenation operator for records, as its
components may contain any types (and not just records). Systems with concatenation typically use a set of constraints/filters (such as lacks and contains)which are useful to combine several, possibly polymorphic, records [34]. In Fi ,constraints on labels are encoded using disjoint quantification and intersections.
Although systems with records can model structurally typed OO languages, it
is harder to encode nominal objects. One advantage of the generality of intersections and merges is that it is easier to have nominal objects. Unlike systems
with records, which have been extensively studied, there is much less work on intersection type systems with a merge operator. An interesting avenue for future
work is to see whether some known compilation and type-inference techniques
for extensible records can be adapted to disjoint intersections and merges.
Traits and mixins. Traits [23,26,36] and mixins [11,6,27,25,5,8] have become
very popular in object-oriented languages. They enable restricted forms of multiple inheritance. One of the main differences between traits and mixins are theway in which ambiguity of names is dealt with. Traits reject programs which

compose classes with conflicting method implementations, whereas mixins assume a resolution strategy, which is usually language dependent. Our example
demonstrated in Section 3 suggests that disjointness in Fi enables a model witha philosophy similar to traits: merging multiple values of overlapping types isforbidden. However while our simple encodings of objects work for very dynamic
forms of prototype inheritance, the work on type systems for mixins/traits usually builds on more conventional class-based OO models.
Constrained types. The notion of disjoint quantification is inspired on boundedpolymorphism [16,12]. Such form of polymorphism typically uses types as subtyping bounds, whereas disjoint quantification uses types as disjoint (i.e. coherent) bounds. Another line of work are qualified types [32], which uses predicateson types to express constraints. However, qualified types are only applicable tothe class of Hindley-Milner languages and such predicates are only defined overmonotypes. Fi falls outside this class of languages, plus its constraints can be
expressed using any arbitrary type (and not just monotypes).

8

Conclusion and Future Work

This paper described Fi : a System F-based language that combines intersection
types, parametric polymorphism and a merge operator. The language is proved
to be type-safe and coherent. To ensure coherence the type system accepts only
disjoint intersections. To provide flexibility in the presence of parametric polymorphism, universal quantification is extended with disjointness constraints. We
believe that disjoint intersection types and disjoint quantification are intuitive,
and at the same time flexible enough to enable practical applications.
For the future, we intend to create a prototype-based statically typed source
language based on Fi . We are also interested in extending our work to systems
with union types and a ⊥ type. Union types are also widely used in languages
such as Ceylon or Flow, but preserving coherence in the presence of union types
is challenging. The naive addition of ⊥ seems to be problematic. The proofs for Fi
rely on the invariant that a type variable α can never be disjoint to another typethat contains α. The addition of ⊥ breaks this invariant, allowing us to derive,for example, Γ ` α ∗ α. Finally, we could study a similar system with implicit
polymorphism. Such system would require some changes in the subtyping anddisjointness relations. For instance, subtyping should allow ∀α. α → α <: Int →Int. Consequently, the disjointness relation would have to be modified, sincevalid statements in Fi such as Γ ` ∀α. α → α ∗ Int → Int would no longer holdunder the more powerful subtyping relation.

Acknowledgments
We would like to thank the ESOP 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. Ceylon, https://ceylon-lang.org/
2. The Coq Proof Assistant, https://coq.inria.fr/
3. Flow, https://flowtype.org/
4. TypeScript, https://www.typescriptlang.org/
5. Ancona, D., Lagorio, G., Zucca, E.: Jam—designing a Java extension with mixins.
ACM Trans. Program. Lang. Syst. 25(5), 641–712 (2003)
6. Ancona, D., Zucca, E.: An algebraic approach to mixins and modularity. In: ALP’96(1996)
7. Aydemir, B.E., Charguéraud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineeringformal metatheory. In: POPL’08 (2008)
8. Bettini, L., Bono, V., Likavec, S.: A core calculus of higher-order mixins and classes.
In: SAC’04 (2004)
9. Black, A.P., Bruce, K.B., Homer, M., Noble, J.: Grace: The absence of (inessential)difficulty. In: Onward! 2012 (2012)
10. Blume, M., Acar, U.A., Chae, W.: Extensible programming with first-class cases.
In: ICFP’06 (2006)
11. Bracha, G., Cook, W.: Mixin-based inheritance. In: OOPSLA/ECOOP ’90 (1990)
12. Canning, P., Cook, W., Hill, W., Olthoff, W., Mitchell, J.C.: F-bounded polymorphism for object-oriented programming. In: FPCA’89 (1989)
13. Cardelli, L.: Theoretical aspects of object-oriented programming. chap. Extensible
records in a pure calculus of subtyping. MIT Press (1994)
14. Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of System Fwith subtyping. Inf. Comput. 109(1-2), 4–56 (1994)
15. Cardelli, L., Mitchell, J.C.: Operations on records. In: Mathematical Foundationsof Programming Semantics (1990)
16. Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471–522 (1985)
17. Castagna, G., Ghelli, G., Longo, G.: A calculus for overloaded functions with subtyping. Information and Computation 117(1), 115–135 (1995)
18. Castagna, G., Nguyen, K., Xu, Z., Im, H., Lenglet, S., Padovani, L.: Polymorphic
functions with set-theoretic types: Part 1: Syntax, semantics, and evaluation. In:
POPL ’14 (2014)
19. Compagnoni, A.B., Pierce, B.C.: Higher-order intersection types and multiple inheritance. Math. Structures Comput. Sci. 6(5), 469–501 (1996)
20. Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable
terms. Mathematical Logic Quarterly 27(2–6), 45–58 (1981)
21. Crary, K.: Simple, efficient object encoding using intersection types. Tech. Rep.
CMU-CS-99-100, Cornell University (1998)
22. Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP’00(2000)
23. Ducasse, S., Nierstrasz, O., Schärli, N., Wuyts, R., Black, A.P.: Traits: A mechanism for fine-grained reuse. ACM Trans. Program. Lang. Syst. 28(2), 331–388(2006)
24. Dunfield, J.: Elaborating intersection and union types. In: ICFP’12 (2012)
25. Findler, R.B., Flatt, M.: Modular object-oriented programming with units andmixins. In: ICFP’98 (1998)
26. Fisher, K.: A typed calculus of traits. In: FOOL11 (2004)
27. Flatt, M., Krishnamurthi, S., Felleisen, M.: Classes and mixins. In: POPL’98 (1998)

28. Gaster, B.R., Jones, M.P.: A polymorphic type system for extensible records andvariants. Tech. Rep. NOTTCS-TR-96-3, University of Nottingham (1996)
29. Harper, R., Pierce, B.: A record calculus based on symmetric concatenation. In:
POPL’91 (1991)
30. Harper, R.W., Pierce, B.C.: Extensible records without subsumption. Tech. Rep.
CMU-C5-90-102 (1990)
31. Jones, M., Jones, S.P.: Lightweight extensible records for Haskell. Tech. Rep. UUCS-1999-28, Haskell Workshop (1999)
32. Jones, M.P.: Qualified Types: Theory and Practice. Cambridge University Press(1994)
33. Leijen, D.: First-class labels for extensible rows. Tech. Rep. UU-CS-2004-051,
Utrecht University (2004)
34. Leijen, D.: Extensible records with scoped labels. In: Trends in Functional Programming (2005)
35. Makholm, H., Wells, J.B.: Type inference, principal typings, and let-polymorphism
for first-class mixin modules. In: ICFP’05 (2005)
36. Odersky, M., Zenger, M.: Scalable component abstractions. In: OOPSLA ’05 (2005)
37. Odersky, M., et al.: An overview of the Scala programming language. Tech. Rep.
IC/2004/64, EPFL Lausanne, Switzerland (2004)
38. Oliveira, B.C.d.S., Shi, Z., Alpuim, J.: Disjoint intersection types. In: ICFP’16(2016)
39. Oliveira, B.C.d.S., Van Der Storm, T., Loh, A., Cook, W.R.: Feature-oriented
programming with object algebras. In: ECOOP’13 (2013)
40. Pierce, B.C.: Programming with intersection types and bounded polymorphism.
Ph.D. thesis, Carnegie Mellon University (1991)
41. Pierce, B.C., Turner, D.N.: Simple type-theoretic foundations for object-oriented
programming. J. Funct. Program. 4(2), 207–247 (1994)
42. Pottier, F.: A constraint-based presentation and generalization of rows. In: LICS’03(2003)
43. Pottinger, G.: A type assignment for the strongly normalizable λ-terms. In: To H.
B. Curry: essays on combinatory logic, lambda calculus and formalism (1980)
44. Rémy, D.: Typing record concatenation for free. In: POPL’92 (1992)
45. Rémy, D.: Theoretical aspects of object-oriented programming. chap. Type inference for records in natural extension of ML. MIT Press (1994)
46. Rendel, T., Brachthäuser, J.I., Ostermann, K.: From object algebras to attributegrammars. In: OOPSLA’14 (2014)
47. Reynolds, J.C.: The coherence of languages with intersection types. In: TACS’91(1991)
48. Reynolds, J.C.: Algol-like languages, chap. Design of the programming language
Forsythe. Birkhäuser Boston (1997)
49. Rompf, T., Amin, N.: Type soundness for dependent object types. In: OOPSLA’16(2016)
50. Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.P.: Traits: Composable units of
behaviour. In: ECOOP’03 (2003)
51. Sulzmann, M.: Designing record systems. Tech. Rep. YALEU/DCS/RR-1128, Yale
University (1997)
52. Wand, M.: Complete type inference for simple objects. In: LICS’87 (1987)
53. Wand, M.: Type inference for record concatenation and multiple inheritance. In:
LICS’89 (1989)