Distributive Disjoint Polymorphism for
Compositional Programming
Xuan Bi1 , Ningning Xie1 , Bruno C. d. S. Oliveira1 , and Tom Schrijvers2
1

The University of Hong Kong, Hong Kong, China{xbi,nnxie,bruno}@cs.hku.hk
2
KU Leuven, Leuven, Belgium
tom.schrijvers@cs.kuleuven.be

Abstract. Popular programming techniques such as shallow embeddingsof Domain Specific Languages (DSLs), finally tagless or object algebras
are built on the principle of compositionality. However, existing programming languages only support simple compositional designs well, and have
limited support for more sophisticated ones.
This paper presents the F+i calculus, which supports highly modular andcompositional designs that improve on existing techniques. These improvements are due to the combination of three features: disjoint intersection types with a merge operator ; parametric (disjoint) polymorphism;
and BCD-style distributive subtyping. The main technical challenge isF+
i ’s proof of coherence. A naive adaptation of ideas used in System F’s
parametricity to canonicity (the logical relation used by F+
i to prove coherence) results in an ill-founded logical relation. To solve the problem
our canonicity relation employs a different technique based on immediate
substitutions and a restriction to predicative instantiations. Besides coherence, we show several other important meta-theoretical results, suchas type-safety, sound and complete algorithmic subtyping, and decidability of the type system. Remarkably, unlike F<: ’s bounded polymorphism,
disjoint polymorphism in F+
i supports decidable type-checking.

1

Introduction

Compositionality is a desirable property in programming designs. Broadly defined, it is the principle that a system should be built by composing smaller subsystems. For instance, in the area of programming languages, compositionality
is a key aspect of denotational semantics [48, 49], where the denotation of a program is constructed from the denotations of its parts. Compositional definitions
have many benefits. One is ease of reasoning: since compositional definitions arerecursively defined over smaller elements they can typically be reasoned about
using induction. Another benefit is that compositional definitions are easy toextend, without modifying previous definitions.
Programming techniques that support compositional definitions include: shallow embeddings of Domain Specific Languages (DSLs) [20], finally tagless [11],polymorphic embeddings [26] or object algebras [35]. These techniques allow us

2

X. Bi et al.

to create compositional definitions, which are easy to extend without modifications. Moreover, when modeling semantics, both finally tagless and object algebras support multiple interpretations (or denotations) of syntax, thus offering asolution to the well-known Expression Problem [53]. Because of these benefits
these techniques have become popular both in the functional and object-oriented
programming communities.
However, programming languages often only support simple compositional
designs well, while support for more sophisticated compositional designs is lacking. For instance, once we have multiple interpretations of syntax, we may wish
to compose them. Particularly useful is a merge combinator, which composes twointerpretations [35, 37, 42] to form a new interpretation that, when executed,
returns the results of both interpretations.
The merge combinator can be manually defined in existing programming
languages, and be used in combination with techniques such as finally tagless orobject algebras. Moreover variants of the merge combinator are useful to model
more complex combinations of interpretations. A good example are so-called
dependent interpretations, where an interpretation does not depend only on
itself, but also on a different interpretation. These definitions with dependencies
are quite common in practice, and, although they are not orthogonal to theinterpretation they depend on, we would like to model them (and also mutuallydependent interpretations) in a modular and compositional style.
Defining the merge combinator in existing programming languages is verbose
and cumbersome, requiring code for every new kind of syntax. Yet, that codeis essentially mechanical and ought to be automated. While using advanced
meta-programming techniques enables automating the merge combinator to alarge extent in existing programming languages [37, 42], those techniques haveseveral problems: error messages can be problematic, type-unsafe reflection isneeded in some approaches [37] and advanced type-level features are requiredin others [42]. An alternative to the merge combinator that supports modular
multiple interpretations and works in OO languages with support for some formof multiple inheritance and covariant type-refinement of fields has also been
recently proposed [55]. While this approach is relatively simple, it still requires
a lot of manual boilerplate code for composition of interpretations.
This paper presents a calculus and polymorphic type system with (disjoint)+intersection types [36], called F+
i . Fi supports our broader notion of compositional designs, and enables the development of highly modular and reusable
programs. F+
i has a built-in merge operator and a powerful subtyping relationthat are used to automate the composition of multiple (possibly dependent)
interpretations. In F+
i subtyping is coercive and enables the automatic generation of coercions in a type-directed fashion. This process is similar to that ofother type-directed code generation mechanisms such as type classes [52], which
eliminate boilerplate code associated to the dictionary translation [52].
F+i continues a line of research on disjoint intersection types. Previous work on
disjoint polymorphism (the Fi calculus) [2] studied the combination of parametricpolymorphism and disjoint intersection types, but its subtyping relation does

Distributive Disjoint Polymorphism3

not support BCD-style distributivity rules [3] and the type system also preventsunrestricted intersections [16]. More recently the NeColus calculus (or λ+i ) [5]
introduced a system with disjoint intersection types and BCD-style distributivity
rules, but did not account for parametric polymorphism. F+
i is unique in that it
combines all three features in a single calculus: disjoint intersection types and amerge operator ; parametric (disjoint) polymorphism; and a BCD-style subtyping
relation with distributivity rules. The three features together allow us to improveupon the finally tagless and object algebra approaches and support advanced
compositional designs. Moreover previous work on disjoint intersection types
has shown various other applications that are also possible in F+
i , including:first-class traits and dynamic inheritance [4], extensible records and dynamic
mixins [2], and nested composition and family polymorphism [5].
Unfortunately the combination of the three features has non-trivial complications. The main technical challenge (like for most other calculi with disjoint
intersection types) is the proof of coherence for F+
i . Because of the presence ofBCD-style distributivity rules, our coherence proof is based on the recent approach employed in λ+i [5], which uses a heterogeneous logical relation calledcanonicity. To account for polymorphism, which λ+i ’s canonicity does not support, we originally wanted to incorporate the relevant parts of System F’s logicalrelation [43]. However, due to a mismatch between the two relations, this did
not work. The parametricity relation has been carefully set up with a delayed
type substitution to avoid ill-foundedness due to its impredicative polymorphism.
Unfortunately, canonicity is a heterogeneous relation and needs to account forcases that cannot be expressed with the delayed substitution setup of the homogeneous parametricity relation. Therefore, to handle those heterogeneous cases,
we resorted to immediate substitutions and predicative instantiations. We do notbelieve that predicativity is a severe restriction in practice, since many source
languages (e.g., those based on the Hindley-Milner type system like Haskell andOCaml) are themselves predicative and do not require the full generality of animpredicative core language. Should impredicative instantiation be required, we
expect that step-indexing [1] can be used to recover well-foundedness, though at
the cost of a much more complicated coherence proof.
The formalization and metatheory of F+
i are a significant advance over thatof Fi . Besides the support for distributive subtyping, F+i removes several restrictions imposed by the syntactic coherence proof in Fi . In particular F+
i supports
unrestricted intersections, which are forbidden in Fi . Unrestricted intersections
enable, for example, encoding certain forms of bounded quantification [39]. Moreover the new proof method is more robust with respect to language extensions.
For instance, F+i supports the bottom type without significant complications in
the proofs, while it was a challenging open problem in Fi . A final interesting
aspect is that F+
i ’s type-checking is decidable. In the design space of languages
with polymorphism and subtyping, similar mechanisms have been known tolead to undecidability. Pierce’s seminal paper “Bounded quantification is undecidable” [40] shows that the contravariant subtyping rule for bounded quantification in F<: leads to undecidability of subtyping. In F+
i the contravariant rule

4

X. Bi et al.

for disjoint quantification retains decidability. Since with unrestricted intersec+
tions F+i can express several use cases of bounded quantification, Fi could be
an interesting and decidable alternative to F<: .
In summary the contributions of this paper are:
– The F+i calculus, which is the first calculus to combine disjoint intersection types, BCD-style distributive subtyping and disjoint polymorphism. We
show several meta-theoretical results, such as type-safety, sound and complete algorithmic subtyping, coherence and decidability of the type system.
F+i includes the bottom type, which was considered to be a significant challenge in previous work on disjoint polymorphism [2].
– An extension of the canonicity relation with polymorphism, whichenables the proof of coherence of F+
i . We show that the ideas of System F’s
parametricity cannot be ported to F+
i . To overcome the problem we use atechnique based on immediate substitutions and a predicativity restriction.
– Improved compositional designs: We show that F+
i ’s combination offeatures enables improved compositional programming designs and supports
automated composition of interpretations in programming techniques like
object algebras and finally tagless.
– Implementation and proofs: All of the metatheory of this paper, except
some manual proofs of decidability, has been mechanically formalized in Coq.
Furthermore, F+
i is implemented and all code presented in the paper is available. The implementation, Coq proofs and extended version with appendicescan be found in https://github.com/bixuanzju/ESOP2019-artifact.

2

Compositional Programming

To demonstrate the compositional properties of F+
i we use Gibbons and Wu’s
shallow embeddings of parallel prefix circuits [20]. By means of several different
shallow embeddings, we first illustrate the short-comings of a state-of-the-art
compositional approach, popularly known as a finally tagless encoding [11], inHaskell. Next we show how parametric polymorphism and distributive intersection types provide a more elegant and compact solution in SEDEL [4], a source
language built on top of our F+
i calculus.
2.1

A Finally Tagless Encoding in Haskell

The circuit DSL represents networks that map a number of inputs (known as thewidth) of some type A onto the same number of outputs of the same type. The
outputs combine (with repetitions) one or more inputs using a binary associative
operator ⊕ : A × A → A. A particularly interesting class of circuits that can be
expressed in the DSL are parallel prefix circuits. These represent computations
that take n > 0 inputs x1 , . . . , xn and produce n outputs y1 , . . . , yn , whereyi = x1 ⊕ x2 ⊕ . . . ⊕ xi .
The DSL features 5 language primitives: two basic circuit constructors andthree circuit combinators. These are captured in the Haskell type class Circuit:Distributive Disjoint Polymorphism

5

data Width = W { width :: Int }instance Circuit Width where
identity n
= W n
fan n
= W n
beside c1 c2 =W (width c1 + width c2)
above c1 c2 = c1
stretch ws c = W (sum ws)

data Depth = D { depth :: Int }instance Circuit Depth where
identity n
= D 0
fan n
= D 1
beside c1 c2 =D (max (depth c1) (depth c2))
above c1 c2 = D (depth c1 + depth c2)
stretch ws c = c(a) Width embedding(b) Depth embedding

Fig. 1: Two finally tagless embeddings of circuits.

class Circuit c where
identity :: Int → cfan:: Int → cbeside:: c → c → c
above:: c → c → cstretch :: [Int] → c → c

An identity circuit with n inputs xi , has n outputs yi = xi . A fan circuit
has n inputs xi and n outputs yi , where y1 = x1 and yj = x1 ⊕ xj (j > 1).
The binary beside combinator puts two circuits in parallel; the combined circuittakes the inputs of both circuits to the outputs of both circuits. The binary above
combinator connects the outputs of the first circuit to the inputs of the second;
the width of both circuits has to be same. Finally, stretch ws c interleaves thewires of circuit c with bundles of additional wires that map their input straighton their output. The ws parameter specifies the width of the consecutive bundles;
the ith wire of c is preceded by a bundle of width wsi − 1.
Basic width and depth embeddings. Figure 1 shows two simple shallow embeddings, which represent a circuit respectively in terms of its width and its depth.
The former denotes the number of inputs/outputs of a circuit, while the latteris the maximal number of ⊕ operators between any input and output. Bothdefinitions follow the same setup: a new Haskell datatype (Width/Depth) wraps
the primitive result value and provides an instance of the Circuit type classthat interprets the 5 DSL primitives accordingly. The following code creates a
so-called Brent-Kung parallel prefix circuit [9]:e1 :: Widthe1 = above (beside (fan 2) (fan 2))(above (stretch [2, 2] (fan 2))(beside (beside (identity 1) (fan 2)) (identity 1)))

Here e1 evaluates to W {width = 4}. If we want to know the depth of the circuit,we have to change type signature to Depth.

6

X. Bi et al.

Interpreting multiple ways. Fortunately, with the help of polymorphism we candefine a type of circuits that support multiple interpretations at once.
type DCircuit = forall c. Circuit c ⇒ cThis way we can provide a single Brent-Kung parallel prefix circuit definition
that can be reused for different interpretations.
brentKung :: DCircuit
brentKung = above (beside (fan 2) (fan 2))(above (stretch [2, 2] (fan 2))(beside (beside (identity 1) (fan 2)) (identity 1)))

A type annotation then selects the desired interpretation. For instance, brentKung:: Width yields the width and brentKung :: Depth the depth.
Composition of embeddings. What is not ideal in the above code is that thesame brentKung circuit is processed twice, if we want to execute both interpretations. We can do better by processing the circuit only once, computing bothinterpretations simultaneously. The finally tagless encoding achieves this with aboilerplate instance for tuples of interpretations.
instance (Circuit c1, Circuit c2) ⇒ Circuit (c1, c2) where
identity n= (identity n, identity n)
fan n= (fan n, fan n)beside c1 c2 = (beside (fst c1) (fst c2), beside (snd c1) (snd c2))
above c1 c2= (above (fst c1) (fst c2), above (snd c1) (snd c2))
stretch ws c = (stretch ws (fst c), stretch ws (snd c))

Now we can get both embeddings simultaneously as follows:
e12 :: (Width, Depth)
e12 = brentKung

This evaluates to (W {width = 4}, D {depth = 2}).
Composition of dependent interpretations. The composition above is easy because the two embeddings are orthogonal. In contrast, the composition of dependent interpretations is rather cumbersome in the standard finally tagless setup.
An example of the latter is the interpretation of circuits as their well-sizedness,
which captures whether circuits are well-formed. This interpretation depends on
the interpretation of circuits as their width.3
data WellSized = WS { wS :: Bool, ox :: Width }instance Circuit WellSized where
identity n= WS True (identity n)
fan n= WS True (fan n)beside c1 c2 = WS (wS c1 && wS c2) (beside (ox c1) (ox c2))
3

Dependent recursion schemes are also known as zygomorphism [18] after the ancient
Greek word ζυγον for yoke. We have labeled the Width field with ox because it ispulling the yoke.

Distributive Disjoint Polymorphism

7

above c1 c2= WS (wS c1 && wS c2 && width (ox c1) == width (ox c2))
(above (ox c1) (ox c2))
stretch ws c = WS (wS c && length ws==width (ox c)) (stretch ws (ox c))

The WellSized datatype represents the well-sizedness of a circuit with a Boolean,
and also keeps track of the circuit’s width. The 5 primitives compute the wellsizedness in terms of both the width and well-sizedness of the subcomponents.
What makes the code cumbersome is that it has to explicitly delegate to theWidth interpretation to collect this additional information.
With the help of a substantially more complicated setup that features adozen Haskell language extensions, and advanced programming techniques, we
can make the explicit delegation implicit (see the appendix). Nevertheless, thatapproach still requires a lot of boilerplate that needs to be repeated for each
DSL, as well as explicit projections that need to be written in each interpretation. Another alternative Haskell encoding that also enables multiple dependentinterpretations is proposed by Zhang and Oliveira [55], but it does not eliminate the explicit delegation and still requires substantial amounts of boilerplate.
A final remark is that adding new primitives (e.g., a “right stretch” rstretch
combinator [25]) can also be easily achieved [46].
2.2

The SEDEL Encoding

SEDEL is a source language that elaborates to F+
i , adding a few convenientsource level constructs. The SEDEL setup of the circuit DSL is similar to thefinally tagless approach. Instead of a Circuit c type class, there is a Circuit[C]type that gathers the 5 circuit primitives in a record. Like in Haskell, the typeparameter C expresses that the interpretation of circuits is a parameter.
type Circuit[C] = {identity : Int → C, fan : Int → C, beside : C → C → C,
above : C → C → C, stretch : List[Int] → C → C };As a side note if a new constructor (e.g., rstretch) is needed, then this is doneby means of intersection types (& creates an intersection type) in SEDEL:
type NCircuit[C] = Circuit[C] & { rstretch : List[Int] → C → C };Figure 2 shows the two basic shallow embeddings for width and depth.
In both cases, a named SEDEL definition replaces the corresponding unnamed
Haskell type class instance in providing the implementations of the 5 language
primitives for a particular interpretation.
The use of the SEDEL embeddings is different from that of their Haskell counterparts. Where Haskell implicitly selects the appropriate type class instancebased on the available type information, in SEDEL the programmer explicitly
selects the implementation following the style used by object algebras. The following code does this by building a circuit with l1 (short for language1).
l1 = language1;
e1 = l1.above (l1.beside (l1.fan 2) (l1.fan 2))

8

X. Bi et al.
type Width = { width : Int };language1 : Circuit[Width] = {identity (n : Int) = { width = n },fan
(n : Int) = { width = n },beside(c1 : Width) (c2 : Width) = { width = c1.width + c2.width },above(c1 : Width) (c2 : Width) = { width = c1.width },stretch (ws : List[Int]) (c : Width) = { width = sum ws } };type Depth = { depth : Int };language2 : Circuit[Depth] = {identity (n : Int) = { depth = 0 },fan(n : Int) = { depth = 1 },beside(c1 : Depth) (c2 : Depth) = { depth = max c1.depth c2.depth},above(c1 : Depth) (c2 : Depth) = { depth = c1.depth + c2.depth},
stretch (ws : List[Int]) (c : Depth) = { depth = c.depth } };Fig. 2: Two SEDEL embeddings of circuits.

(l1.above (l1.stretch (cons 2 (cons 2 nil)) (l1.fan 2))(l1.beside (l1.beside (l1.identity 1) (l1.fan 2)) (l1.identity 1)));

Here e1 evaluates to {width = 4}. If we want to know the depth of the circuit,we have to replicate the code with language2.
Dynamically reusable circuits. Just like in Haskell, we can use polymorphism todefine a type of circuits that can be interpreted with different languages.
type DCircuit = { accept : forall C. Circuit[C] → C };In contrast to the Haskell solution, this implementation explicitly accepts theimplementation.
brentKung : DCircuit = {accept C l = l.above (l.beside (l.fan 2) (l.fan 2))(l.above (l.stretch (cons 2 (cons 2 nil)) (l.fan 2))(l.beside (l.beside (l.identity 1) (l.fan 2)) (l.identity 1))) };e1 = brentKung.accept Width language1;e2 = brentKung.accept Depth language2;

Automatic composition of languages. Of course, like in Haskell we can also compute both results simultaneously. However, unlike in Haskell, the composition of
the two interpretation requires no boilerplate whatsoever—in particular, there
is no SEDEL counterpart of the Circuit (c1, c2) instance. Instead, we can justcompose the two interpretations with the term-level merge operator (,,) andspecify the desired type Circuit[Width & Depth].
language3 : Circuit[Width & Depth] = language1 ,, language2;e3 = brentKung.accept (Width & Depth) language3;

Distributive Disjoint Polymorphism

9

Here the use of the merge operator creates a term with the intersection typeCircuit[Width] & Circuit[Depth]. Implicitly, the SEDEL type system takes careof the details, turning this intersection type into Circuit[Width & Depth]. Thisis possible because intersection (&) distributes over function and record types (adistinctive feature of BCD-style subtyping).
Composition of dependent interpretations. In SEDEL the composition scales
nicely to dependent interpretations. For instance, the well-sizedness interpretation can be expressed without explicit projections.
type WellSized = { wS : Bool };language4 = {identity (n : Int) = { wS = true },fan(n : Int) = { wS = true },above (c1 : WellSized & Width) (c2 : WellSized & Width) ={ wS = c1.wS && c2.wS && c1.width == c2.width },beside (c1 : WellSized) (c2 : WellSized) = { wS = c1.wS && c2.wS
stretch (ws : List[Int]) (c : WellSized & Width) ={ wS = c.wS && length ws == c.width } };},Here the WellSized & Width type in the above and stretch cases expresses thatboth the well-sizedness and width of subcircuits must be given, and that thewidth implementation is left as a dependency—when language4 is used, then
the width implementation must be provided. Again, the distributive propertiesof & in the type system take care of merging the two interpretations.
e4= brentKung.accept (WellSized & Width) (language1 ,, language4);
main = e4.wS -- Output: true

Disjoint polymorphism and dynamic merges. While it may seem from the above
examples that definitions have to be merged statically, SEDEL in fact supports
dynamic merges. For instance, we can encapsulate the merge operator in the
combine function while abstracting over the two components x and y that are
merged as well as over their types A and B.
combine A [B * A] (x : A) (y : B) = x ,, y;This way the components x and y are only known at runtime and thus the merge
can only happen at that time. The types A and B cannot be chosen entirely freely.
For instance, if both components would contribute an implementation for thesame method, which implementation is provided by the combination would be
ambiguous. To avoid this problem the two types A and B have to be disjoint.
This is expressed in the disjointness constraint * A on the quantifier of the typevariable B. If a quantifier mentions no disjointness constraint, like that of A, it
defaults to the trivial * > constraint which implies no restriction.

3

Semantics of the F+
i Calculus

This section gives a formal account of F+i , the first typed calculus combining disjoint polymorphism [2] (and disjoint intersection types) with BCD subtyping [3].

10

X. Bi et al.

A, B , C ::= Int | > | ⊥ | A → B | A & B | {l : A} | α | ∀(α ∗ A). B::= x | i | > | λx . E | E1 E2 | E1 , , E2 | E : A | {l = E } | E .lE
| Λ(α ∗ A). E | E A::= • | Γ, x : A
Term contexts Γ::= • | ∆, α ∗ A
Type contexts ∆Types
Expressions

Fig. 3: Syntax of F+i
The main differences to Fi are in the subtyping, well-formedness and disjointness
relations. F+
i adds BCD subtyping and unrestricted intersections, and also closes
an open problem of Fi by including the bottom type. The dynamic semantics
of F+
i is given by elaboration to the target calculus Fco —a variant of System F
extended with products and explicit coercions.
3.1

Syntax and Semantics

Figure 3 shows the syntax of F+i . Metavariables A, B , C range over types. Types
include standard constructs from prior work [2, 36]: integers Int, the top type >,arrows A → B , intersections A & B , single-field record types {l : A} and disjoint
quantification ∀(α ∗ A). B . One novelty in F+
i is the addition of the uninhabitedbottom type ⊥. Metavariable E ranges over expressions. Expressions are integer
literals i, the top value >, lambda abstractions λx . E , applications E1 E2 , merges
E1 , , E2 , annotated terms E : A, single-field records {l = E }, record projections
E .l , type abstractions Λ(α ∗ A). E and type applications E A.
Well-formedness and unrestricted intersections. F+
i ’s well-formedness judgmentof types ∆ ` A is standard, and only enforces well-scoping. This is one of the key
differences from Fi , which uses well-formedness to also ensure that all intersection
types are disjoint. In other words, while in Fi all valid intersection types must
be disjoint, in F+
i unrestricted intersection types such as Int & Int are allowed.
More specifically, the well-formedness of intersection types in F+
i and Fi is:
∆`A

∆`B

∆ ` A&B

wf-F+
i

∆`A

∆`B
∆ ` A&B

∆`A∗B
wf-Fi

Notice that Fi has an extra disjointness condition ∆ ` A ∗ B in the premise. Thisis crucial for Fi ’s syntactic method for proving coherence, but also burdens thecalculus with various syntactic restrictions and complicates its metatheory. For
example, it requires extra effort to show that Fi only produces disjoint intersection types. As a consequence, Fi features a weaker substitution lemma (note thegray part in Proposition 1) than F+i (Lemma 1).
Proposition 1 (Type substitution in Fi ). If ∆ ` A, ∆ ` B , (α ∗ C ) ∈ ∆,∆ ` B ∗ C and well-formed context [B /α]∆, then [B /α]∆ ` [B /α]A.
Lemma 1 (Type substitution in F+i ). If ∆ ` A, ∆ ` B , (α ∗ C ) ∈ ∆ andwell-formed context [B /α]∆, then [B /α]∆ ` [B /α]A.

Distributive Disjoint Polymorphism
A <: Bco(Declarative subtyping)
S-trans
A2 <: A3

S-reflA <: Aid

S-rcd
A <: Bco1

A1 <: A2A1 <: A3

co1 ◦ co2

co1

A <: >

A2 <: B2

A1 → A2 <: B1 → B2

π1

S-and
A1 <: A2

co2

A1 & A2 <: A2

π2

A1 <: A3

co2

co1

A1 <: A2 & A3

co1 → co2

hco1 , co2 i

S-topArr

S-distArr(A1 → A2 ) & (A1 → A3 ) <: A1 → A2 & A3

> <: > → >dist→
S-topRcd

S-distRcd{l : A} & {l : B } <: {l : A & B }S-forallB1 <: B2

top

S-andr

A1 & A2 <: A1

co

S-top

co2

S-andlco{l : A} <: {l : B }S-arr
B1 <: A1

11

co

> <: {l : >}

id

S-bot
id

⊥ <: Abot

S-topAll

A2 <: A1∀(α ∗ A1 ). B1 <: ∀(α ∗ A2 ). B2

top→

co∀

> <: ∀(α ∗ >). >top∀

S-distAll(∀(α ∗ A). B1 ) & (∀(α ∗ A). B2 ) <: ∀(α ∗ A). B1 & B2

dist∀

Fig. 4: Declarative subtyping

Declarative subtyping. F+
i ’s subtyping judgment is another major difference toFi , because it features BCD-style subtyping and a rule for the bottom type. The
full set of subtyping rules are shown in Fig. 4. The reader is advised to ignore thegray parts for now. Our subtyping rules extend the BCD-style subtyping rules
from λ+i [5] with a rule for parametric (disjoint) polymorphism (rule S-forall).
Moreover, we have three new rules: rule S-bot for the bottom type, and rules SdistAll and S-topAll for distributivity of disjoint quantification. The subtyping relation is a partial order (rules S-refl and S-trans). Most of the rules
are quite standard. ⊥ is a subtype of all types (rule S-bot). Subtyping of disjoint quantification is covariant in its body, and contravariant in its disjointness
constraints (rule S-forall). Of particular interest are those so-called “distributivity” rules: rule S-distArr says intersections distribute over arrows; rule SdistRcd says intersections distribute over records. Similarly, rule S-distAll
dictates that intersections may distribute over disjoint quantifiers.

12

X. Bi et al.

∆; Γ ` E ⇒ A
T-top
`∆

e

(Inference)
T-nat
`∆

∆`Γ

∆; Γ ` > ⇒ >

hi

T-var
`∆

∆`Γ

∆; Γ ` i ⇒ Int∆`Γ(x : A) ∈ Γ∆; Γ ` x ⇒ A

i

T-app
e1
∆; Γ ` E1 ⇒ A1 → A2∆; Γ ` E2 ⇐ A1
e2

T-merge∆; Γ ` E1 ⇒ A1
e2∆; Γ ` E2 ⇒ A2∆; Γ ` E1 E2 ⇒ A2

e1 e2∆; Γ ` E1 , , E2 ⇒ A1 & A2

e

T-rcd
∆; Γ ` E ⇒ A

T-anno∆; Γ ` E ⇐ A∆; Γ ` E : A ⇒ A
T-proj∆; Γ ` E ⇒ {l : A}∆; Γ ` E .l ⇒ A

T-tabs∆, α ∗ A; Γ ` E ⇒ Bee∆; Γ ` E A ⇒ [A/α]C

T-abs
∆`A

he1 , e2 i

e
e

∆`A

e

∆; Γ ` Λ(α ∗ A). E ⇒ ∀(α ∗ A). Be

T-tapp∆; Γ ` E ⇒ ∀(α ∗ B ). C∆; Γ ` E ⇐ A

e1∆ ` A1 ∗ A2∆; Γ ` {l = E } ⇒ {l : A}

e

x

∆`Γ
Λα. e

∆`A∗B
e |A|

e

(Checking)∆; Γ, x : A ` E ⇐ B∆; Γ ` λx . E ⇐ A → B

λx . ee

T-sub∆; Γ ` E ⇒ Be∆; Γ ` E ⇐ A

B <: Acoco eFig. 5: Bidirectional type system

Typing rules. F+
i features a bidirectional type system inherited from Fi . The
full set of typing rules are shown in Fig. 5. Again we ignore the gray partsand explain them in Section 3.3. The inference judgment ∆; Γ ` E ⇒ A saysthat we can synthesize the type A under the contexts ∆ and Γ . The checking
judgment ∆; Γ ` E ⇐ A asserts that E checks against the type A under thecontexts ∆ and Γ . Most of the rules are quite standard in the literature. The
merge expression E1 , , E2 is well-typed if both sub-expressions are well-typed,
and their types are disjoint (rule T-merge). The disjointness relation will be
explained in Section 3.2. To infer a type abstraction (rule T-tabs), we add
disjointness constraints to the type context. For a type application (rule Ttapp), we check that the type argument satisfies the disjointness constraints.
Rules T-merge and T-tapp are the only rules checking disjointness.

Distributive Disjoint PolymorphismeAd

13(Top-like types)

TL-topTL-andeAdeB d

TL-arreB d

TL-rcdeAd

TL-alleB deA & B deA → B de{l : A}de∀(α ∗ A). B d

e>d

∆`A∗B

(Disjointness)

D-topLeAd

D-topReB d

D-arr∆ ` A2 ∗ B2

∆`A∗B

∆`A∗B

∆ ` A1 → A2 ∗ B1 → B2

D-andL∆ ` A1 ∗ B∆ ` A2 ∗ B

D-andR∆ ` A ∗ B1

∆ ` A1 & A2 ∗ B
D-rcdEq∆`A∗B

D-rcdNeq
l1 6= l2

∆ ` {l : A} ∗ {l : B }∆ ` {l1 : A} ∗ {l2 : B }D-tvarR(α ∗ A) ∈ ∆A <: B∆`B ∗α∆ ` A ∗ B2

∆ ` A ∗ B1 & B2
D-tvarL(α ∗ A) ∈ ∆A <: B∆`α∗B

D-forall∆, α ∗ A1 & A2 ` B1 ∗ B2

D-ax
A ∗ax B∆ ` ∀(α ∗ A1 ). B1 ∗ ∀(α ∗ A2 ). B2∆`A∗B

Fig. 6: Selected rules for disjointness

3.2

Disjointness

We now turn to another core judgment of F+i —the disjointness relation, shownin Fig. 6. The disjointness rules are mostly inherited from Fi [2], but the newbottom type requires a notable change regarding disjointness with top-like types.
Top-like types. Top-like types are all types that are isomorphic to > (i.e., simultaneously sub- and supertypes of >). Hence, they are inhabited by a single
value, isomorphic to the > value. Fig. 6 captures this notion in a syntax-directedfashion in the eAd predicate. As a historical note, the concept of top-like types
was already known by Barendregt et al. [3]. The λi calculus [36] re-discovered it
and coined the term “top-like types”; the Fi calculus [2] extended it with universal quantifiers. Note that in both calculi, top-like types are solely employed forenabling a syntactic method of proving coherence, and due to the lack of BCD
subtyping, they do not have a type-theoretic interpretation of top-like types.
Disjointness rules. The disjointness judgment ∆ ` A ∗ B is helpful to check
whether the merge of two expressions of type A and B preserves coherence.
Incoherence arises when both expressions produce distinct values for the same

14

X. Bi et al.
τ ::= Int | hi | τ1 → τ2 | τ1 × τ2 | α | ∀α. τe ::= x | i | hi | λx . e | e1 e2 | he1 , e2 i | Λα. e | e τ | co e
co ::= id | co1 ◦ co2 | top | bot | co1 → co2 | hco1 , co2 i | π1 | π2
| co∀ | dist→ | top→ | top∀ | dist∀
Valuesv ::= i | hi | λx . e | hv1 , v2 i | Λα. e | (co1 → co2 ) v | co∀ v| dist→ v | top→ v | top∀ v | dist∀ v
Term contexts
Ψ ::= • | Ψ, x : τType contexts
Φ ::= • | Φ, αEvaluation contexts E ::= [·] | E e | v E | hE, ei | hv , Ei | co E | E τ

Types
Terms
CoercionsFig. 7: Syntax of Fcotype, either directly when they are both of that same type, or through implicit
upcasting to a common supertype. Of course we can safely disregard top-liketypes in this matter because they do not have two distinct values. In short, it
suffices to check that the two types have only top-like supertypes in common.
Because ⊥ and any another type A always have A as a common supertype,
it follows that ⊥ is only disjoint to A when A is top-like. More generally, if A isa top-like type, then A is disjoint to any type. This is the rationale behind thetwo rules D-topL and D-topR, which generalize and subsume ∆ ` > ∗ A and∆ ` A ∗ > from Fi , and also cater to the bottom type. Two other interesting
rules are D-tvarL and D-tvarR, which dictate that a type variable α is disjoint
with some type B if its disjointness constraints A is a subtype of B . Disjointness
axioms A∗ax B (appearing in rule D-ax) take care of two types with different type
constructors (e.g., Int and records). Axiom rules can be found in the appendix.
Finally we note that the disjointness relation is symmetric.
3.3

Elaboration and Type Safety

The dynamic semantics of F+
i is given by elaboration into a target calculus.
The target calculus Fco is the standard call-by-value System F extended withproducts and coercions. The syntax of Fco is shown in Fig. 7.
Type translation. Definition 1 defines the type translation function | · | fromF+
i types A to Fco types τ . Most cases are straightforward. For example, ⊥is mapped to an uninhabited type ∀α. α; disjoint quantification is mapped touniversal quantification, dropping the disjointness constraints. | · | is naturally
extended to work on contexts as well.
Definition 1. Type translation | · | is defined as follows:|Int| = Int|A & B | = |A| × |B ||⊥| = ∀α. α|>| = hi|{l : A}| = |A||∀(α ∗ A). B | = ∀α. |B ||A → B | = |A| → |B ||α| = αDistributive Disjoint Polymorphisme −→ e 0

15(Single-step reduction)r-forallr-topAllr-distAll(co∀ v ) τ −→ co (v τ )(top∀ hi) τ −→ hi(dist∀ hv1 , v2 i) τ −→ hv1 τ, v2 τ ir-tappr-app

r-ctxte −→ e 0(Λα. e) τ −→ [τ /α]e

(λx . e) v −→ [v /x ]eE[e] −→ E[e 0 ]Fig. 8: Selected reduction rules

Coercions and coercive subtyping. We follow prior work [5, 6] by having a syntactic category for coercions [22]. In Fig. 7, we have several new coercions: bot,co∀ , dist∀ and top∀ due to the addition of polymorphism and bottom type. As
seen in Fig. 4 the coercive subtyping judgment has the form A <: Bco,which says that the subtyping derivation for A <: B produces a coercion co thatconverts terms of type |A| to |B |.
Fco static semantics. The typing rules of Fco are quite standard. We have one
rule t-capp regarding coercion application, which uses the judgment co :: τ . τ 0
to type coercions. We show two representative rules ct-forall and ct-bot.
t-cappΦ; Ψ ` e : τ

co :: τ . τ 0

Φ; Ψ ` co e : τ0

ct-forallco :: τ1 . τ2

ct-botco∀ :: ∀α. τ1 . ∀α. τ2bot :: ∀α. α . τ

Fco dynamic semantics. The dynamic semantics of Fco is mostly unremarkable.
We write e −→ e 0 to mean one-step reduction. Figure 8 shows selected reduction
rules. The first line shows three representative rules regarding coercion reductions. They do not contribute to computation but merely rearrange coercions.
Our coercion reduction rules are quite standard but not efficient in terms ofspace. Nevertheless, there is existing work on space-efficient coercions [23, 50],
which should be applicable to our work as well. Rule r-app is the usual β-rulethat performs actual computation, and rule r-ctxt handles reduction under an
evaluation context. As usual, −→∗ is the reflexive, transitive closure of −→. Now
we can show that Fco is type safe:
Theorem 1 (Preservation). If •; • ` e : τ and e −→ e 0 , then •; • ` e 0 : τ .
Theorem 2 (Progress). If •; • ` e : τ , either e is a value, or ∃e 0 . e −→ e 0 .
Elaboration. Now consider the translation parts in Fig. 5. The key idea of thetranslation follows the prior work [2, 5, 16, 36]: merges are elaborated to pairs(rule T-merge); disjoint quantification and disjoint type applications (rules Ttabs and T-tapp) are elaborated to regular universal quantification and typeapplications, respectively. Finally, the following lemma connects F+
i to Fco :16

X. Bi et al.

Lemma 2 (Elaboration soundness). We have that:– If A <: B
co, then co :: |A| . |B |.
– If ∆; Γ ` E ⇒ A
e, then |∆|; |Γ | ` e : |A|.
– If ∆; Γ ` E ⇐ A
e, then |∆|; |Γ | ` e : |A|.

4

Algorithmic System and Decidability

The subtyping relation in Fig. 4 is highly non-algorithmic due to the presence ofa transitivity rule. This section presents an alternative algorithmic formulation.
Our algorithm extends that of λ+i , which itself was inspired by Pierce’s decision
procedure [38], to handle disjoint quantifiers and the bottom type. We then provethat the algorithm is sound and complete with respect to declarative subtyping.
Additionally we prove that the subtyping and disjointness relations are decidable. Although the proofs of this fact are fairly straightforward, it is nonetheless remarkable since it contrasts with the subtyping relation for (full) F<: [10],which is undecidable [40]. Thus while bounded quantification is infamous for its
undecidability, disjoint quantification has the nicer property of being decidable.
4.1

Algorithmic Subtyping Rules

While Fig. 4 is a fine specification of how subtyping should behave, it cannot
be read directly as a subtyping algorithm for two reasons: (1) the conclusionsof rules S-refl and S-trans overlap with the other rules, and (2) the premisesof rule S-trans mention a type that does not appear in the conclusion. Simply
dropping the two offending rules from the system is not possible without losing
expressivity [29]. Thus we need a different approach. Following λ+i , we intend
the algorithmic judgment Q ` A <: B to be equivalent to A <: Q ⇒ B , where Q
is a queue used to track record labels, domain types and disjointness constraints.
The full rules of the algorithmic subtyping of F+
i are shown Fig. 9.
Definition 2 (Q ::= [] | l , Q | B , Q | α ∗ B , Q). Q ⇒ A is defined as follows:[] ⇒ A = A(l , Q) ⇒ A = {l : Q ⇒ A}

(B , Q) ⇒ A = B → (Q ⇒ A)
(α ∗ B , Q) ⇒ A = ∀(α ∗ B ). Q ⇒ A

For brevity of the algorithm, we use metavariable c to mean type constants:
Type Constants c ::= Int | ⊥ | α
The basic idea of Q ` A <: B is to perform a case analysis on B until it reaches
type constants. We explain new rules regarding disjoint quantification and thebottom type. When a quantifier is encountered in B , rule A-forall pushes thetype variables with its disjointness constraints onto Q and continue with the
body. Correspondingly, in rule A-allConst, when a quantifier is encounteredin A, and the head of Q is a type variable, this variable is popped out and wecontinue with the body. Rule A-bot is similar to its declarative counterpart.
Two meta-functions JQK> and JQK& are meant to generate correct forms of
coercions, and their definitions are shown in the appendix. For other algorithmic
rules, we refer to λ+i [5] for detailed explanations.

Distributive Disjoint Polymorphism
Q ` A <: B

co

(Algorithmic subtyping)A-and
Q ` A <: B1

A-top
Q ` A <: >17>

JQK ◦ topco1

Q ` A <: B1 & B2

Q ` A <: B2

JQK ◦ hco1 , co2 iA-arr
Q, B1 ` A <: B2

co

A-rcd
Q, l ` A <: B

Q ` A <: B1 → B2co

Q ` A <: {l : B }A-forallQ, α ∗ B1 ` A <: B2

coA-constQ ` A <: ∀(α ∗ B1 ). B2

co[] ` c <: cA-arrConst[] ` A <: A1

Q ` A2 <: cco1

A, Q ` A1 → A2 <: cA-andConstco
Q ` Ai <: cQ ` A1 & A2 <: cco2

co1 → co2

co2

&

co
co

A-bot
Q ` ⊥ <: cid

A-rcdConst
Q ` A <: c

bot

co

l , Q ` {l : A} <: ccoi ∈ {1, 2}

A-allConst[] ` A <: A1

Q ` A2 <: ccoco ◦ πi(α ∗ A, Q) ` ∀(α ∗ A1 ). A2 <: cco∀Fig. 9: Algorithmic subtyping

Correctness of the algorithm. We prove that the algorithm is sound and completewith respect to the specification. We refer the reader to our Coq formalization
for more details. We only show the two major theorems:
Theorem 3 (Soundness). If Q ` A <: B

co then A <: Q ⇒ B

Theorem 4 (Completeness). If A <: B

co, then ∃co0 . [] ` A <: B

4.2

co.
co0 .

Decidability

Moreover, we prove that our algorithmic type system is decidable. To see this,first notice that the bidirectional type system is syntax-directed, so we only needto show decidability of algorithmic subtyping and disjointness. The full (manual)
proofs for decidability can be found in the appendix.
Lemma 3 (Decidability of algorithmic subtyping). Given Q, A and B ,it is decidable whether there exists co, such that Q ` A <: Bco.
Lemma 4 (Decidability of disjointness checking).
it is decidable whether ∆ ` A ∗ B .

Given ∆, A and B ,18

X. Bi et al.

One interesting observation here is that although our disjointness quantification has a similar shape to bounded quantification ∀(α <: A). B in F<: [10],subtyping for F<: is undecidable [40]. In F<: , the subtyping relation between
bounded quantification is:∆ ` A2 <: A1∆, α <: A2 ` B1 <: B2∆ ` ∀(α <: A1 ). B1 <: ∀(α <: A2 ). B2

fsub-forall

Compared with rule S-forall, both rules are contravariant on bounded/disjoint types, and covariant on the body. However, with bounded quantification it
is fundamental to track the bounds in the environment, which complicates thedesign of the rules and makes subtyping undecidable with rule fsub-forall.
Decidability can be recovered by employing an invariant rule for bounded quantification (that is by forcing A1 and A2 to be identical). Disjoint quantification
does not require such invariant rule for decidability.

5

Establishing Coherence for F+i

In this section, we establish the coherence property for F+
i . The proof strategy
mostly follows that of λ+
,
but
the
constructionoftheheterogeneous
logical rei
lation is significantly more complicated. Firstly in Section 5.1 we discuss why
adding BCD subtyping to disjoint polymorphism introduces significant complications. In Section 5.2, we discuss why a natural extension of System F’s
logical relation to deal with disjoint polymorphism fails. The technical difficulty
is well-foundedness, stemming from the interaction between impredicativity anddisjointness. Finally in Section 5.3, we present our (predicative) logical relationthat is specially crafted to prove coherence for F+
i .
5.1

The Challenge

Before we tackle the coherence of F+i , let us first consider how Fi (and its predecessor λi ) enforces coherence. Its essentially syntactic approach is to make surethat there is at most one subtyping derivation for any two types. As an immediate consequence, the produced coercions are uniquely determined and thus thecalculus is clearly coherent. Key to this approach is the invariant that the typesystem only produces disjoint intersection types. As we mentioned in Section 3,
this invariant complicates the calculus and its metatheory, and leads to a weaker
substitution lemma. Moreover, the syntactic coherence approach is incompatible with BCD subtyping, which leads to multiple subtyping derivations withdifferent coercions and requires a more general substitution lemma. To accommodate BCD into λi , Bi et al. [5] have created the λ+i calculus and developed asemantically-founded proof method based on logical relations. Because λ+i doesnot feature polymorphism, the problem at hand is to incorporate support forpolymorphism in this semantic approach to coherence, which turns out to be
more challenging than is apparent.

Distributive Disjoint Polymorphism

19(v1 , v2 ) ∈ VJInt; IntK , ∃i. v1 = v2 = i(v1 , v2 ) ∈ VJτ1 → τ2 ; τ10 → τ20 K , ∀(v , v 0 ) ∈ VJτ1 ; τ10 K. (v1 v , v2 v 0 ) ∈ EJτ2 ; τ20 K(hv1 , v2 i, v3 ) ∈ VJτ1 × τ2 ; τ3 K , (v1 , v3 ) ∈ VJτ1 ; τ3 K ∧ (v2 , v3 ) ∈ VJτ2 ; τ3 K
(v3 , hv1 , v2 i) ∈ VJτ3 ; τ1 × τ2 K , (v3 , v1 ) ∈ VJτ3 ; τ1 K ∧ (v3 , v2 ) ∈ VJτ3 ; τ2 K

Fig. 10: Selected cases from λ+i ’s canonicity relation
5.2

Impredicativity and Disjointness at Odds

Figure 10 shows selected cases of canonicity, which is λ+i ’s (heterogeneous) logicalrelation used in the coherence proof. The definition captures that two values v1
and v2 of types τ1 and τ2 are in VJτ1 ; τ2 K iff either the types are disjoint or
the types are equal and the values are semantically equivalent. Because bothalternatives entail coherence, canonicity is key to λ+i ’s coherence proof.
Well-foundedness issues. For F+
i , we need to extend canonicity with additional
cases to account for universally quantified types. For reasons that will become
clear in Section 5.3, the type indices become source types (rather than target
types as in Fig. 10). A naive formulation of one case rule is:(v1 , v2 ) ∈ VJ∀(α ∗ A1 ). B1 ; ∀(α ∗ A2 ). B2 K ,∀C1 ∗ A1 , C2 ∗ A2 . (v1 |C1 |, v2 |C2 |) ∈ EJ[C1 /α]B1 ; [C2 /α]B2 K

This case is problematic because it destroys the well-foundedness of λ+i ’s logicalrelation, which is based on structural induction on the type indices. Indeed, thetype [C1 /α]B1 may well be larger than ∀(α ∗ A1 ). B1 .
However, System F’s well-known parametricity logical relation [43] provides
us with a means to avoid this problem. Rather than performing the type substitution immediately as in the above rule, we can defer it to a later point byadding it to an extra parameter ρ of the relation, which accumulates the deferred
substitutions. This yields a modified rule where the type indices in the recursive
occurrences are indeed smaller:(v1 , v2 ) ∈ VJ∀(α ∗ A1 ). B1 ; ∀(α ∗ A2 ). B2 Kρ ,∀C1 ∗ A1 , C2 ∗ A2 .(v1 |C1 |, v2 |C2 |) ∈ EJB1 ; B2 Kρ[α7→(C1 ,C2 )]Of course, the deferred substitution has to be performed eventually, to be precise
when the type indices are type variables.
(v1 , v2 ) ∈ VJα; αKρ , (v1 , v2 ) ∈ VJρ1 (α); ρ2 (α)K∅
Unfortunately, this way we have not only moved the type substitution to thetype variable case, but also the ill-foundedness problem. Indeed, this problem isalso present in System F. The standard solution is to not fix the relation R bywhich values at type α are related to VJρ1 (α); ρ2 (α)K, but instead to make it aparameter that is tracked by ρ. This yields the following two rules for disjoint
quantification and type variables:(v1 , v2 ) ∈ VJ∀(α ∗ A1 ). B1 ; ∀(α ∗ A2 ). B2 Kρ , ∀C1 ∗ A1 , C2 ∗ A2 , R ⊆ C1 × C2 .

(v1 |C1 |, v2 |C2 |) ∈ EJB1 ; B2 Kρ[α7→(C1 ,C2 ,R)]

(v1 , v2 ) ∈ VJα; αKρ , (v1 , v2 ) ∈ ρR (α)

20

X. Bi et al.

Now we have finally recovered the well-foundedness of the relation. It is again
structurally inductive on the size of the type indexes.
Heterogeneous issues. We have not yet accounted for one major difference between the parametricity relation, from which we have borrowed ideas, and thecanonicity relation, to which we have been adding. The former is homogeneous(i.e., the types of the two values is the same) and therefore has one type index, while the latter is heterogeneous (i.e., the two values may have different
types) and therefore has two type indices. Thus we must also consider cases like
VJα; IntK. A definition that seems to handle this case appropriately is:(v1 , v2 ) ∈ VJα; IntKρ , (v1 , v2 ) ∈ VJρ1 (α); IntK∅(1)

Here is an example to motivate it. Let E = Λ(α∗>). ((λx . x ) : α & Int → α & Int).
We expect that E Int 1 evaluates to h1, 1i. To prove that, we need to show (1, 1) ∈VJα; IntK[α7→(Int,Int,R)] . According to Eq. (1), this is indeed the case. However, we
run into ill-foundedness issue again, because ρ1 (α) could be larger than α. Alas,this time the parametricity relation has no solution for us.
5.3

The Canonicity Relation for F+i

In light of the fact that substitution in the logical relation seems unavoidable
in our setting, and that impredicativity is at odds with substitution, we turn topredicativity: we change rule T-tapp to its predicative version:∆; Γ ` E ⇒ ∀(α ∗ B ). Ce∆; Γ ` E t ⇒ [t/α]C∆`t ∗Be |t|T-tappMono

where metavariable t ranges over monotypes (types minus disjoint quantification). We do not believe that predicativity is a severe restriction in practice,since many source languages (e.g., those based on the Hindley-Milner type system [24, 32] like Haskell and OCaml) are themselves predicative and do not
require the full generality of an impredicative core language.
Luckily, substitution with monotypes does not prevent well-foundedness. Figure 11 defines the canonicity relation for F+
i . The canonicity relation is a familyof binary relations over Fco values that are heterogeneous, i.e., indexed by two F+
itypes. Two points are worth mentioning. (1) An apparent difference from λ+i ’slogical relation is that our relation is now indexed by source types. The reason isthat the type translation function (Definition 1) discards disjointness constraints,
which are crucial in our setting, whereas λ+i ’s type translation does not have information loss. (2) Heterogeneity allows relating values of different types, and inparticular values whose types are disjoint. The rationale behind the canonicity
relation is to combine equality checking from traditional (homogeneous) logicalrelations with disjointness checking. It consists of two relations: the value relation VJA; B K relates closed values; and the expression relation EJA; B K—definedin terms of the value relation—relates closed expressions.
The relation VJA; B K is defined by induction on the structures of A and B .
For integers, it requires the two values to be literally the same. For two records toDistributive Disjoint Polymorphism

21(v1 , v2 ) ∈ VJInt; IntK , ∃i. v1 = v2 = i(v1 , v2 ) ∈ VJ{l : A}; {l : B }K , (v1 , v2 ) ∈ VJA; B K(v1 , v2 ) ∈ VJA1 → B1 ; A2 → B2 K , ∀(v20 , v10 ) ∈ VJA2 ; A1 K. (v1 v10 , v2 v20 ) ∈ EJB1 ; B2 K
(hv1 , v2 i, v3 ) ∈ VJA & B ; C K , (v1 , v3 ) ∈ VJA; C K ∧ (v2 , v3 ) ∈ VJB ; C K(v3 , hv1 , v2 i) ∈ VJC ; A & B K , (v3 , v1 ) ∈ VJC ; AK ∧ (v3 , v2 ) ∈ VJC ; B K(v1 , v2 ) ∈ VJ∀(α ∗ A1 ). B1 ; ∀(α ∗ A2 ). B2 K , ∀• ` t ∗ A1 & A2 . (v1 |t|, v2 |t|) ∈ EJ[t/α]B1 ; [t/α]B2 K(v1 , v2 ) ∈ VJA; B K , true otherwise(e1 , e2 ) ∈ EJA; B K , ∃v1 , v2 . e1 −→∗ v1 ∧ e2 −→∗ v2 ∧ (v1 , v2 ) ∈ VJA; B Kρ ∈ DJ∆Kρ ∈ DJ∆K , ∅ ∈ DJ•K

(γ1 , γ2 ) ∈ GJΓ Kρ , (∅, ∅) ∈ GJ•Kρ• ` t ∗ ρ(B )ρ[α 7→ t] ∈ DJ∆, α ∗ B K(γ1 , γ2 ) ∈ GJΓ Kρ

(v1 , v2 ) ∈ VJρ(A); ρ(A)K(γ1 [x 7→ v1 ], γ2 [x 7→ v2 ]) ∈ GJΓ, x : AKρ

Fig. 11: The canonicity relation for F+ibehave the same, their fields must behave the same. For two functions to behave
the same, they are required to produce outputs related at B1 and B2 when given
related inputs at A1 and A2 . For the next two cases regarding intersection types,
the relation distributes over intersection constructor & . Of particular interest is
the case for disjoint quantification. Notice that it does not quantify over arbitrary
relations, but directly substitutes α with monotype t in B1 and B2 . This meansthat our canonicity relation does not entail parametricity. However, it suffices
for our purposes to prove coherence. Another noticeable thing is that we keep
the invariant that A and B are closed types throughout the relation, so we nolonger need to consider type variables. This simplifies things a lot. Note thatwhen one type is ⊥, two values are vacuously related because there simply areno values of type ⊥. We need to show that the relation is indeed well-founded:
Lemma 5 (Well-foundedness). The canonicity relation of F+
i is well-founded.
Proof. Let | · |∀ and | · |s be the number of ∀-quantifies and the size of types,
respectively. Consider the measure h| · |∀ , | · |s i, where h. . . i denotes lexicographic
order. For the case of disjoint quantification, the number of ∀-quantifiers decreases. For the other cases, the measure of | · |∀ does not increase, and themeasure of | · |s strictly decreases.
t
u

5.4

Establishing Coherence

Logical equivalence. The canonicity relation can be lifted to open expressions inthe standard way, i.e., by considering all possible interpretations of free type andterm variables. The logical interpretations of type and term contexts are foundin the bottom half of Fig. 11.

22

X. Bi et al.

Definition 3 (Logical equivalence wlog ).
∆; Γ ` e1 wlog e2 : A; B , |∆|; |Γ | ` e1 : |A| ∧ |∆|; |Γ | ` e2 : |B | ∧(∀ρ, γ1 , γ2 . ρ ∈ DJ∆K ∧ (γ1 , γ2 ) ∈ GJΓ Kρ =⇒ (γ1 (ρ1 (e1 )), γ2 (ρ2 (e2 ))) ∈ EJρ(A); ρ(B )K)

For conciseness, we write ∆; Γ ` e1 wlog e2 : A to mean ∆; Γ ` e1 wlog e2 : A; A.
Contextual equivalence. Following λ+i , the notion of coherence is based on contextual equivalence. The intuition is that two programs are equivalent if we cannot
tell them apart in any context. As usual, contextual equivalence is expressedusing expression contexts (C and D denote F+i and Fco expression contexts,
respectively), Due to the bidirectional nature of the type system, the typing
judgment of C features 4 different forms (full rules are in the appendix), e.g.,
C : (∆; Γ ⇒ A) 7→ (∆0 ; Γ 0 ⇒ A0 )D reads if ∆; Γ ` E ⇒ A then∆0 ; Γ 0 ` C{E } ⇒ A0 . The judgment also generates a well-typed Fco context
D. The following two definitions capture the notion of contextual equivalence:
Definition 4 (Kleene Equality w). Two complete programs (i.e., closed termsof type Int), e and e 0 , are Kleene equal, written e w e 0 , iff there exists an integer
i such that e −→∗ i and e 0 −→∗ i.
Definition 5 (Contextual Equivalence wctx ).
∆; Γ ` E1 wctx E2 : A , ∀e1 , e2 . ∆; Γ ` E1 ⇒ A(∀C , D. C : (∆; Γ ⇒ A) 7→ (•; • ⇒ Int)e1 ∧ ∆; Γ ` E2 ⇒ A

e2 ∧D =⇒ D{e1 } w D{e2 })Coherence. For space reasons, we directly show the coherence statement of F+i .
We need several technical lemmas such as compatibility lemmas, fundamental
property, etc. The interested reader can refer to our Coq formalization.
Theorem 5 (Coherence). We have that
– If ∆; Γ ` E ⇒ A then ∆; Γ ` E wctx E : A.
– If ∆; Γ ` E ⇐ A then ∆; Γ ` E wctx E : A.
That is, coherence is a special case of Definition 5 where E1 and E2 are the same.
At first glance, this appears underwhelming: of course E behaves the same as
itself! The tricky part is that, if we expand it according to Definition 5, it is not
E itself but all its translations e1 and e2 that behave the same!

6

Related Work

Coherence. In calculi featuring coercive subtyping, a semantics that interprets
the subtyping judgment by introducing explicit coercions is typically defined on
typing derivations rather than on typing judgments. A natural question thatarises for such systems is whether the semantics is coherent, i.e., distinct typing derivations of the same typing judgment possess the same meaning. Since
Reynolds [45] proved the coherence of a calculus with intersection types, many

Distributive Disjoint Polymorphism

23

researchers have studied the problem of coherence in a variety of typed calculi.
Two approaches are commonly found in the literature. The first approach is tofind a normal form for a representation of the derivation and show that normal
forms are unique for a given typing judgment [8, 15, 47]. However, this approachcannot be directly applied to Curry-style calculi (where the lambda abstractions
are not type annotated). Biernacki and Polesiuk [6] considered the coherence
problem of coercion semantics. Their criterion for coherence of the translationis contextual equivalence in the target calculus. Inspired by this approach, Bi etal. [5] proposed the canonicity relation to prove coherence for a calculus withdisjoint intersection types and BCD subtyping. As we have shown in Section 5,
constructing a suitable logical relation for F+
i is challenging. On the one hand,the original approach by Alpuim et al. [2] in Fi does not work any more due tothe addition of BCD subtyping. On the other hand, simply combining System
F’s logical relation with λ+i ’s canonicity relation does not work as expected, due
to the issue of well-foundedness. To solve the problem, we employ immediate
substitutions and a restriction to predicative instantiations.
BCD subtyping and decidability. The BCD type system was first introducedby Barendregt et al. [3] to characterize exactly the strongly normalizing terms.
The BCD type system features a powerful subtyping relation, which serves asa base for our subtyping relation. The decidability of BCD subtyping has beenshown in several works [27, 38, 41, 51]. Laurent [28] formalized the relation in
Coq in order to eliminate transitivity cuts from it, but his formalization does
not deliver an algorithm. Only recently, Laurent [30] presented a general wayof defining a BCD-like subtyping relation extended with generic contravariant/covariant type constructors that enjoys the “sub-formula property”. Our Coq
formalization extends the approach used in λ+i , which follows a different idea
based on Pierce’s decision procedure [38], with parametric (disjoint) polymorphism and corresponding distributivity rules. More recently, Muehlboeck andTate [34] presented a decidable algorithmic system (proved in Coq) with union
and intersection types. Similar to F+
i , their system also has distributive subtyping
rules. They also discussed the addition of polymorphism, but left a Coq formalization for future work. In their work they regard intersections of disjoint types(e.g., String & Int) as uninhabitable, which is different from our interpretation.
As a consequence, coherence is a non-issue for them.
Intersection types, the merge operator and polymorphism. Forsythe [44] has intersection types and a merge-like operator. However to ensure coherence, various
restrictions were added to limit the use of merges. In Forsythe merges cannot
contain more than one function. Castagna et al. [12] proposed a coherent calculus λ& to study overloaded functions. λ& has a special merge operator thatworks on functions only. Dunfield proposed a calculus [16] (which we call λ,, )that shows significant expressiveness of type systems with unrestricted intersection types and an (unrestricted) merge operator. However, because of his unrestricted merge operator (allowing 1 , , 2), his calculus lacks coherence. Blaauwbroek’s λ∨∧ [7] enriched λ,, with BCD subtyping and computational effects, but

24

X. Bi et al.
λ,, [16]λi [36]

λ∨
∧ [7]

λ+
i [5]

Fi [2]

F+i

Disjointness
Unrestricted intersections
BCD subtyping
Polymorphism
Coherence
Bottom typeFig. 12: Summary of intersection calculi ( = yes, = no, = syntactic coherence)

he did not address coherence. The coherence issue for a calculus similar to λ,,was first addressed in λi [36] with the notion of disjointness, but at the costof dropping unrestricted intersections, and a strict notion of coherence (basedon α-equivalence). Later Bi et al. [5] improved calculi with disjoint intersection
types by removing several restrictions, adopted BCD subtyping and a semantic
notion of coherence (based on contextual equivalence) proved using canonicity.
The combination of intersection types, a merge operator and parametric polymorphism, while achieving coherence was first studied in Fi [2], which serves asa foundation for F+
i . However, Fi suffered the same problems as λi . Additionallyin Fi a bottom type is problematic due to interactions with disjoint polymorphism and the lack of unrestricted intersections. The issues can be illustrated
with the well-typed F+
i expression Λ(α ∗ ⊥). λx : α. x , , x . In this expression thetype of x , , x is α & α. Such a merge does not violate disjointness because theonly types that α can be instantiated with are top-like, and top-like types do not
introduce incoherence. In Fi a type variable α can never be disjoint to anothertype that contains α, but (as the previous expression shows) the addition of abottom type allows expressions where such (strict) condition does not hold. In
this work, we removed those restrictions, extended BCD subtyping with polymorphism, and proposed a more powerful logical relation for proving coherence.
Figure 12 summarizes the main differences between the aforementioned calculi.
There are also several other calculi with intersections and polymorphism.
Pierce proposed F∧ [39], a calculus combining intersection types and bounded
quantification. Pierce translates F∧ to System F extended with products, but
he left coherence as a conjecture. More recently, Castagna et al. [14] proposed apolymorphic calculus with set-theoretic type connectives (intersections, unions,
negations). But their calculus does not include a merge operator. Castagna andLanvin also proposed a gradual type system [13] with intersection and union
types, but also without a merge operator.
Row polymorphism and bounded polymorphism. Row polymorphism was originally proposed by Wand [54] as a mechanism to enable type inference for a simple object-oriented language based on recursive records. These ideas were later
adopted into type systems for extensible records [19, 21, 31]. Our merge operator
can be seen as a generalization of record extension/concatenation, and selectionis also built-in. In contrast to most record calculi, restriction is not a primitive

Distributive Disjoint Polymorphism

25

operation in F+
i , but can be simulated via subtyping. Disjoint quantification cansimulate the lacks predicate often present in systems with row polymorphism.
Recently Morris and McKinna presented a typed language [33], generalizing andabstracting existing systems of row types and row polymorphism. Alpuim etal. [2] informally studied the relationship between row polymorphism and disjoint polymorphism, but it would be interesting to study such relationship moreformally. The work of Morris and McKinna may be interesting for such study inthat it gives a general framework for row type systems.
Bounded quantification is currently the dominant mechanism in major mainstream object-oriented languages supporting both subtyping and polymorphism.
F<: [10] provides a simple model for bounded quantification, but type-checking
in full F<: is proved to be undecidable [40]. Pierce’s thesis [39] discussed the relationship between calculi with simple polymorphism and intersection types andbounded quantification. He observed that there is a way to “encode” many formsof bounded quantification in a system with intersections and pure (unbounded)second-order polymorphism. That encoding can be easily adapted to F+i :∀(α <: A). B , ∀(α ∗ >). ([A & α/α]B )The idea is to replace bounded quantification by (unrestricted) universal quantification and all occurrences of α by A & α in the body. Such an encoding seems
to indicate that F+
i could be used as a decidable alternative to (full) F<: . It
is worthwhile to note that this encoding does not work in Fi because A & α is
not well-formed (α is not disjoint to A). In other words, the encoding requires
unrestricted intersections.

7

Conclusion and Future Work

We have proposed F+
i , a type-safe and coherent calculus with disjoint intersection
types, BCD subtyping and parametric polymorphism. F+
i improves the state-ofart of compositional designs, and enables the development of highly modular andreusable programs. One interesting and useful further extension would be implicit polymorphism. For that we want to combine Dunfield and Krishnaswami’s
approach [17] with our bidirectional type system. We would also like to study theparametricity of F+
i . As we have seen in Section 5.2, it is not at all obvious how
to extend the standard logical relation of System F to account for disjointness,
and avoid potential circularity due to impredicativity. A promising solution is
to use step-indexed logical relations [1].

Acknowledgments
We thank the anonymous reviewers and Yaoda Zhou for their helpful comments. This work has been sponsored by the Hong Kong Research Grant Council projects number 17210617 and 17258816, and by the Research Foundation Flanders.

Bibliography[1] Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: European Symposium on Programming (ESOP) (2006)[2] Alpuim, J., Oliveira, B.C.d.S., Shi, Z.: Disjoint polymorphism. In: European
Symposium on Programming (ESOP) (2017)[3] Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda modeland the completeness of type assignment. The journal of symbolic logic
48(04), 931–940 (1983)[4] Bi, X., Oliveira, B.C.d.S.: Typed First-Class Traits. In: European Conference on Object-Oriented Programming (ECOOP) (2018)[5] Bi, X., Oliveira, B.C.d.S., Schrijvers, T.: The Essence of Nested Composition. In: European Conference on Object-Oriented Programming (ECOOP)(2018)[6] Biernacki, D., Polesiuk, P.: Logical relations for coherence of effect subtyping. In: International Conference on Typed Lambda Calculi and Applications (TLCA) (2015)[7] Blaauwbroek, L.: On the Interaction Between Unrestricted Union and Intersection Types and Computational Effects. Master’s thesis, Technical University Eindhoven (2017)[8] Breazu-Tannen, V., Coquand, T., Gunter, C.A., Scedrov, A.: Inheritance as
implicit coercion. Information and Computation 93(1), 172–221 (1991)[9] Brent, R.P., Kung, H.T.: The chip complexity of binary arithmetic. In: Proceedings of the twelfth annual ACM symposium on Theory of computing.
pp. 190–200 (1980)[10] Cardelli, L., Wegner, P.: On understanding types, data abstraction, andpolymorphism. ACM Computing Surveys 17(4), 471–523 (1985)[11] Carette, J., Kiselyov, O., Shan, C.C.: Finally tagless, partially evaluated:
Tagless staged interpreters for simpler typed languages. Journal of Functional Programming 19(05), 509 (2009)[12] Castagna, G., Ghelli, G., Longo, G.: A calculus for overloaded functions with
subtyping. In: Conference on LISP and Functional Programming (1992)[13] Castagna, G., Lanvin, V.: Gradual typing with union and intersection types.
Proceedings of the ACM on Programming Languages 1(ICFP), 1–28 (aug2017)[14] Castagna, G., Nguyen, K., Xu, Z., Im, H., Lenglet, S., Padovani, L.: Polymorphic functions with set-theoretic types: part 1: syntax, semantics, andevaluation. In: Principles of Programming Languages (POPL) (2014)[15] Curien, P.L., Ghelli, G.: Coherence of subsumption, minimum typing andtype-checking in f≤ . Mathematical Structures in Computer Science (MSCS)
2(01), 55 (1992)[16] Dunfield, J.: Elaborating intersection and union types. Journal of Functional
Programming (JFP) 24(2-3), 133–165 (2014)

Distributive Disjoint Polymorphism

27[17] Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higher-rank polymorphism. In: International Conference on
Functional Programming (ICFP) (2013)[18] Fokkinga, M.M.: Tupling and mutumorphisms. Squiggolist 1(4) (1989)[19] Gaster, B.R., Jones, M.P.: A polymorphic type system for extensible records
and variants. Tech. rep., University of Nottingham (1996)[20] Gibbons, J., Wu, N.: Folding domain-specific languages: deep and shallow
embeddings (functional pearl). In: ICFP. pp. 339–347. ACM (2014)[21] Harper, R., Pierce, B.: A record calculus based on symmetric concatenation.
In: Principles of Programming Languages (POPL) (1991)[22] Henglein, F.: Dynamic typing: syntax and proof theory. Science of Computer
Programming 22(3), 197–230 (6 1994)[23] Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. HigherOrder and Symbolic Computation 23(2), 167 (2010)[24] Hindley, R.: The principal type-scheme of an object in combinatory logic.
Transactions of the american mathematical society 146, 29–60 (1969)[25] Hinze, R.: An algebra of scans. In: International Conference on Mathematics
of Program Construction. pp. 186–210 (2004)[26] Hofer, C., Ostermann, K., Rendel, T., Moors, A.: Polymorphic embedding of
DSLs. In: International Conference on Generative Programming and Component Engineering (GPCE) (2008)[27] Kurata, T., Takahashi, M.: Decidable properties of intersection type systems. Typed Lambda Calculi and Applications pp. 297–311 (1995)[28] Laurent, O.: Intersection types with subtyping by means of cut elimination.
Fundamenta Informaticae 121(1-4), 203–226 (2012)[29] Laurent, O.: A syntactic introduction to intersection types (2012), unpublished note[30] Laurent, O.: Intersection subtyping with constructors. In: Proceedings of
the Ninth Workshop on Intersection Types and Related Systems (2018)[31] Leijen, D.: Extensible records with scoped labels. Trends in Functional Programming 5, 297–312 (2005)[32] Milner, R.: A theory of type polymorphism in programming. Journal ofcomputer and system sciences 17(3), 348–375 (1978)[33] Morris, J.G., McKinna, J.: Abstracting extensible data types. In: Principles
of Programming Languages (POPL) (2019)[34] Muehlboeck, F., Tate, R.: Empowering union and intersection types withintegrated subtyping. In: OOPSLA (2018)[35] Oliveira, B.C.d.S., Cook, W.R.: Extensibility for the masses. In: European
Conference on Object-Oriented Programming (ECOOP) (2012)[36] Oliveira, B.C.d.S., Shi, Z., Alpuim, J.: Disjoint intersection types. In: International Conference on Functional Programming (ICFP) (2016)[37] Oliveira, B.C.d.S., Van Der Storm, T., Loh, A., Cook, W.R.: Featureoriented programming with object algebras. In: European Conference on
Object-Oriented Programming (ECOOP) (2013)[38] Pierce, B.C.: A decision procedure for the subtype relation on intersection
types with bounded variables. Tech. rep., Carnegie Mellon University (1989)

28

X. Bi et al.

[39] Pierce, B.C.: Programming with intersection types and bounded polymorphism. Ph.D. thesis, University of Pennsylvania (1991)[40] Pierce, B.C.: Bounded quantification is undecidable. Information and Computation 112(1), 131–165 (1994)[41] Rehof, J., Urzyczyn, P.: Finite combinatory logic with intersection types.
In: International Conference on Typed Lambda Calculi and Applications(2011)[42] Rendel, T., Brachthäuser, J.I., Ostermann, K.: From object algebras toattribute grammars. In: Object-Oriented Programming, Systems Languages
and Applications (OOPSLA) (2014)[43] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Proceedings of the IFIP 9th World Computer Congress (1983)[44] Reynolds, J.C.: Preliminary design of the programming language forsythe.
Tech. rep., Carnegie Mellon University (1988)[45] Reynolds, J.C.: The coherence of languages with intersection types. In: Lecture Notes in Computer Science (LNCS), pp. 675–700. Springer Berlin Heidelberg (1991)[46] d. S. Oliveira, B.C., Hinze, R., Löh, A.: Extensible and modular generics forthe masses. In: Revised Selected Papers from the Seventh Symposium on
Trends in Functional Programming, TFP 2006, Nottingham, United Kingdom, 19-21 April 2006. pp. 199–216 (2006)[47] Schwinghammer, J.: Coherence of subsumption for monadic types. Journalof Functional Programming (JFP) 19(02), 157 (2008)[48] Scott, D.: Outline of a mathematical theory of computation. Oxford University Computing Laboratory, Programming Research Group (1970)[49] Scott, D.S., Strachey, C.: Toward a mathematical semantics for computer
languages, vol. 1. Oxford University Computing Laboratory, Programming
Research Group (1971)[50] Siek, J., Thiemann, P., Wadler, P.: Blame and coercion: together again
for the first time. In: Conference on Programming Language Design and
Implementation (PLDI) (2015)[51] Statman, R.: A finite model property for intersection types. Electronic Proceedings in Theoretical Computer Science 177, 1–9 (2015)[52] Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In:
Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages. POPL ’89 (1989)[53] Wadler, P.: The expression problem. Java-genericity mailing list (1998)[54] Wand, M.: Complete type inference for simple objects. In: Symposium on
Logic in Computer Science (LICS) (1987)[55] Zhang, W., d. S. Oliveira, B.C.: Shallow edls and object-oriented programming. To appear in Programming Journal (2019)