The Essence of Nested Composition
Xuan Bi1
The University of Hong Kong, Hong Kong, China
xbi@cs.hku.hk

Bruno C. d. S. Oliveira1
The University of Hong Kong, Hong Kong, China
bruno@cs.hku.hk

Tom Schrijvers2
KU Leuven, Belgium
tom.schrijvers@cs.kuleuven.be

Abstract
Calculi with disjoint intersection types support an introduction form for intersections called themerge operator, while retaining a coherent semantics. Disjoint intersections types have great
potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason
OO languages. This paper shows how to significantly increase the expressive power of disjoint
intersection types by adding support for nested subtyping and composition, which enables simple
forms of family polymorphism to be expressed in the calculus. The extension with nested subtyping and composition is challenging, for two different reasons. Firstly, the subtyping relationthat supports these features is non-trivial, especially when it comes to obtaining an algorithmic
version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint
intersection types is too inflexible, making it hard to extend those calculi with new features (suchas nested subtyping). We show how to address the first problem by adapting and extending the
Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by
Pierce’s work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations. Our work has been fully formalizedin Coq, and we have an implementation of our calculus.
2012 ACM Subject Classification Software and its engineering → Object oriented languages
Keywords and phrases nested composition, family polymorphism, intersection types, coherence
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2018.22
Acknowledgements We thank the anonymous reviewers for their helpful comments.

1

Introduction

Intersection types [49, 18] have a long history in programming languages. They wereoriginally introduced to characterize exactly all strongly normalizing lambda terms. Since
then, starting with Reynolds’s work on Forsythe [54], they have also been employed to express
useful programming language constructs, such as key aspects of multiple inheritance [17] inObject-Oriented Programming (OOP). One notable example is the Scala language [44] and its
DOT calculus [3], which make fundamental use of intersection types to express a class/trait

1
2

Funded by Hong Kong Research Grant Council projects number 17210617 and 17258816
Funded by The Research Foundation - Flanders© Xuan Bi, Bruno C. d. S. Oliveira and Tom Schrijvers;
licensed under Creative Commons License CC-BY
32nd European Conference on Object-Oriented Programming (ECOOP 2018).
Editor: Todd Millstein; Article No. 22; pp. 22:1–22:33
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

22:2

The Essence of Nested Composition

that extends multiple other traits. Other modern languages, such as TypeScript [39], Flow [28]and Ceylon [51], also adopt some form of intersection types.
Intersection types come in different varieties in the literature. Some calculi provide an
explicit introduction form for intersections, called the merge operator. This operator was
introduced by Reynolds in Forsythe [54] and adopted by a few other calculi [15, 23, 46, 2].
Unfortunately, while the merge operator is powerful, it also makes it hard to get a coherent(or unambiguous) semantics. Unrestricted uses of the merge operator can be ambiguous,leading to an incoherent semantics where the same program can evaluate to different values.
A far more common form of intersection types are the so-called refinement types [30, 21, 24].
Refinement types restrict the formation of intersection types so that the two types in anintersection are refinements of the same simple (unrefined) type. Refinement intersection
increases only the expressiveness of types and not of terms. For this reason, Dunfield [23]argues that refinement intersection is unsuited for encoding various useful language featuresthat require the merge operator (or an equivalent term-level operator).
Disjoint Intersection Types. λi is a recent calculus with a variant of intersection types
called disjoint intersection types [46]. Calculi with disjoint intersection types feature themerge operator, with restrictions that all expressions in a merge operator must have disjoint
types and all well-formed intersections are also disjoint. A bidirectional type system and the
disjointness restrictions ensure that the semantics of the resulting calculi remains coherent.
Disjoint intersection types have great potential to serve as a foundation for powerful,flexible and yet type-safe OO languages that are easy to reason about. As shown by Alpuim
et al. [2], calculi with disjoint intersection types are very expressive and can be used tostatically type-check JavaScript-style programs using mixins. Yet they retain both typesafety and coherence. While coherence may seem at first of mostly theoretical relevance, itturns out to be very relevant for OOP. Multiple inheritance is renowned for being tricky to
get right, largely because of the possible ambiguity issues caused by the same field/method
names inherited from different parents [9, 58]. Disjoint intersection types enforce that thetypes of parents are disjoint and thus that no conflicts exist. Any violations are staticallydetected and can be manually resolved by the programmer. This is very similar to existing
trait models [29, 22]. Therefore in an OO language modelled on top of disjoint intersection
types, coherence implies that no ambiguity arises from multiple inheritance. This makes
reasoning a lot simpler.
Family Polymorphism. One powerful and long-standing idea in OOP is family polymorphism [25]. In family polymorphism inheritance is extended to work on a whole family ofclasses, rather than just a single class. This enables high degrees of modularity and reuse,including simple solutions to hard programming language problems, like the Expression
Problem [64]. An essential feature of family polymorphism is nested composition [19, 27, 42],which allows the automatic inheritance/composition of nested (or inner) classes when the
top-level classes containing them are composed. Designing a sound type system that fully
supports family polymorphism and nested composition is notoriously hard; there are only afew, quite sophisticated, languages that manage this [27, 42, 16, 57].
NeColus. This paper presents an improved variant of λi called NeColus3 (or λ+i ): a simple
calculus with records and disjoint intersection types that supports nested composition. Nested
3

NeColus stands for Nested Composition calculus.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:3

composition enables encoding simple forms of family polymorphism. More complex forms offamily polymorphism, involving binary methods [11] and mutable state are not yet supported,
but are interesting avenues for future work. Nevertheless, in NeColus, it is possible, forexample, to encode Ernst’s elegant family-polymorphism solution [25] to the Expression
Problem. Compared to λi the essential novelty of NeColus are distributivity rules between
function/record types and intersection types. These rules are the delta that enable extending
the simple forms of multiple inheritance/composition supported by λi into a more powerfulform supporting nested composition. The distributivity rule between function types andintersections is common in calculi with intersection types aimed at capturing the set of allstrongly normalizable terms, and was first proposed by Barendregt et al. [4] (BCD). However
the distributivity rule is not common in calculi or languages with intersection types aimed at
programming. For example the rules employed in languages that support intersection types(such as Scala, TypeScript, Flow or Ceylon) lack distributivity rules. Moreover distributivity
is also missing from several calculi with a merge operator. This includes all calculi with disjoint
intersection types and Dunfield’s work on elaborating intersection types, which was theoriginal foundation for λi . A possible reason for this omission in the past is that distributivity
adds substantial complexity (both algorithmically and metatheoretically), without having
any obvious practical applications. This paper shows how to deal with the complications of
BCD subtyping, while identifying a major reason to include it in a programming language:
BCD enables nested composition and subtyping, which is of significant practical interest.
NeColus differs significantly from previous BCD-based calculi in that it has to deal withthe possibility of incoherence, introduced by the merge operator. Incoherence is a non-issue
in the previous BCD-based calculi because they do not feature this merge operator or any
other source of incoherence. Although previous work on disjoint intersection types proposesa solution to coherence, the solution imposes several ad-hoc restrictions to guarantee theuniqueness of the elaboration and thus allow for a simple syntactic proof of coherence. Most
importantly, it makes it hard or impossible to adapt the proof to extensions of the calculus,
such as the new subtyping rules required by the BCD system.
In this work we remove the brittleness of the previous syntactic method to prove coherence,by employing a more semantic proof method based on logical relations [63, 48, 61]. This new
proof method has several advantages. Firstly, with the new proof method, several restrictions
that were enforced by λi to enable the syntactic proof method are removed. For example
the work on λi has to carefully distinguish between so-called top-like types and other types.
In NeColus this distinction is not necessary; top-like types are handled like all other types.
Secondly, the method based on logical relations is more powerful because it is based on
semantic rather than syntactic equality. Finally, the removal of the ad-hoc side-conditions
makes adding new extensions, such as support for BCD-style subtyping, easier. In order todeal with the complexity of the elaboration semantics of NeColus, we employ binary logicalrelations that are heterogeneous, parameterized by two types; the fundamental property isalso reformulated to account for bidirectional type-checking.
In summary the contributions of this paper are:
NeColus: a calculus with (disjoint) intersection types that features both BCD-style
subtyping and the merge operator. This calculus is both type-safe and coherent, andsupports nested composition.
A more flexible notion of disjoint intersection types where only merges need to be checkedfor disjointness. This removes the need for enforcing disjointness for all well-formed types,
making the calculus more easily extensible.
An extension of BCD subtyping with both records and elaboration into coercions, and

ECOOP 2018

22:4

The Essence of Nested Composition

algorithmic subtyping rules with coercions, inspired by Pierce’s decision procedure [47].
A more powerful proof strategy for coherence of disjoint intersection types based on
logical relations.
Illustrations of how the calculus can encode essential features of family polymorphism
through nested composition.
A comprehensive Coq mechanization of all meta-theory. This has notably revealed
several missing lemmas and oversights in Pierce’s manual proof [47] of BCD’s algorithmic
subtyping. We also have an implementation of a language built on top of NeColus; itruns and type-checks all examples shown in the paper.4

2

Overview

This section illustrates NeColus with an encoding of a family polymorphism solution to theExpression Problem, and informally presents its salient features.

2.1

Motivation: Family Polymorphism

In OOP family polymorphism is the ability to simultaneously refine a family of related classes
through inheritance. This is motivated by a need to not only refine individual classes, butalso to preserve and refine their mutual relationships. Nystrom et al. [42] call this scalable
extensibility: “the ability to extend a body of code while writing new code proportional tothe differences in functionality”. A well-studied mechanism to achieve family inheritance isnested inheritance [42]. Nested inheritance combines two aspects. Firstly, a class can havenested class members; the outer class is then a family of (inner) classes. Secondly, when one
family extends another, it inherits (and can override) all the class members, as well as therelationships within the family (including subtyping) between the class members. However,
the members of the new family do not become subtypes of those in the parent family.
The Expression Problem, Scandinavian Style. Ernst [25] illustrates the benefits of nested
inheritance for modularity and extensibility with one of the most elegant and concise solutions
to the Expression Problem [64]. The objective of the Expression Problem is to extend adatatype, consisting of several cases, together with several associated operations in two
dimensions: by adding more cases to the datatype and by adding new operations for thedatatype. Ernst solves the Expression Problem in the gbeta language, which he adorns witha Java-like syntax for presentation purposes, for a small abstract syntax tree (AST) example.
His starting point is the code shown in Fig. 1a. The outer class Lang contains a family of
related AST classes: the common superclass Exp and two cases, Lit for literals and Add for
addition. The AST comes equipped with one operation, toString, which is implemented byboth cases.
Adding a New Operation. One way to extend the family is to add an additional evaluation
operation, as shown in the top half of Fig. 1b. This is done by subclassing the Lang classand refining all the contained classes by implementing the additional eval method. Notethat the inheritance between, e.g., Lang.Exp and Lang.Lit is transferred to LangEval.Exp
and LangEval.Lit. Similarly, the Lang.Exp type of the left and right fields in Lang.Add is
automatically refined to LangEval.Exp in LangEval.Add.

4

The Coq formalization and implementation are available at https://goo.gl/R5hUAp.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

class Lang {virtual class Exp {String toString() {}}virtual class Lit extends Exp {int value;Lit(int value) {this.value = value;}
String toString() {return value;}}
virtual class Add extends Exp {Exp left,right;
Add(Exp left, Exp right) {this.left = left;
this.right = right;}
String toString() {return left + "+" + right;}}}(a) Base family: the language Lang

22:5// Adding a new operation
class LangEval extends Lang {refine class Exp {int eval() {}}refine class Lit {int eval { return value; }}refine class Add {int eval { returnleft.eval() + right.eval();}}}// Adding a new caseclass LangNeg extends Lang {virtual class Neg extends Exp {Neg(Exp exp) { this.exp = exp; }String toString() {return "-(" + exp + ")";}Exp exp;}}(b) Extending in two dimensions

Figure 1 The Expression Problem, Scandinavian Style

Adding a New Case. A second dimension to extend the family is to add a case for negation,
shown in the bottom half of Fig. 1b. This is similarly achieved by subclassing Lang, and now
adding a new contained class Neg, for negation, that implements the toString operation.
Finally, the two extensions are naturally combined by means of multiple inheritance,
closing the diamond.
class LangNegEval extends LangEval & LangNeg {refine class Neg {int eval() { return -exp.eval(); }}}The only effort required is to implement the one missing operation case, evaluation of negatedexpressions.

2.2

The Expression Problem, NeColus Style

The NeColus calculus allows us to solve the Expression Problem in a way that is very similar
to Ernst’s gbeta solution. However, the underlying mechanisms of NeColus are quite different
from those of gbeta. In particular, NeColus features a structural type system in which we
can model objects with records, and object types with record types. For instance, we model
the interface of Lang.Exp with the singleton record type { print : String }. For the sake ofconciseness, we use type aliases to abbreviate types.
type IPrint = { print : String };ECOOP 2018

22:6

The Essence of Nested Composition

Similarly, we capture the interface of the Lang family in a record, with one field for eachcase’s constructor.
type Lang = { lit : Int → IPrint, add : IPrint → IPrint → IPrint };Here is the implementation of Lang.
implLang : Lang = {lit (value : Int) = { print = value.toString },add (left : IPrint) (right : IPrint) = {print = left.print ++ "+" ++ right.print}};

Adding Evaluation. We obtain IPrint & IEval, which is the corresponding type for LangEval.Exp,by intersecting IPrint with IEval wheretype IEval = { eval : Int };The type for LangEval is then:type LangEval = {
lit : Int → IPrint & IEval,
add : IPrint & IEval → IPrint & IEval → IPrint & IEval};

We obtain an implementation for LangEval by merging the existing Lang implementation
implLang with the new evaluation functionality implEval using the merge operator ,,.
implEval = {lit (value : Int) = { eval = value },add (left : IEval) (right : IEval) = {eval = left.eval + right.eval}};
implLangEval : LangEval = implLang ,, implEval;

Adding Negation.

Adding negation to Lang works similarly.

type NegPrint = { neg : IPrint → IPrint };type LangNeg = Lang & NegPrint;
implNegPrint : NegPrint = {neg (exp : IPrint) = { print = "-" ++ exp.print }};implLangNeg : LangNeg = implLang ,, implNegPrint;

Putting Everything Together. Finally, we can combine the two extensions and provide themissing implementation of evaluation for the negation case.
type NegEval = { neg : IEval → IEval};
implNegEval : NegEval = {neg (exp : IEval) = { eval = 0 - exp.eval }};type NegEvalExt = { neg : IPrint & IEval → IPrint & IEval };type LangNegEval = LangEval & NegEvalExt;
implLangNegEval : LangNegEval = implLangEval ,, implNegPrint ,, implNegEval;

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:7

We can test implLangNegEval by creating an object e of expression −2 + 3 that is able toprint and evaluate at the same time.
fac = implLangNegEval;e = fac.add (fac.neg (fac.lit 2)) (fac.lit 3);
main = e.print ++ " = " ++ e.eval.toString -- Output: "-2+3 = 1"

Multi-Field Records. One relevant remark is that NeColus does not have multi-field record
types built in. They are merely syntactic sugar for intersections of single-field record types.
Hence, the following is an equivalent definition of Lang:
type Lang = {lit : Int → IPrint} & {add : IPrint → IPrint → IPrint};

Similarly, the multi-field record expression in the definition of implLang is syntactic sugar forthe explicit merge of two single-field records.
implLang : Lang = { lit = ... } ,, { add = ... };Subtyping. A big difference compared to gbeta is that many more NeColus types are related
through subtyping. Indeed, gbeta is unnecessarily conservative [26]: none of the families isrelated through subtyping, nor is any of the class members of one family related to any of
the class members in another family. For instance, LangEval is not a subtype of Lang, nor is
LangNeg.Lit a subtype of Lang.Lit.
In contrast, subtyping in NeColus is much more nuanced and depends entirely on the
structure of types. The primary source of subtyping are intersection types: any intersection
type is a subtype of its components. For instance, IPrint & IEval is a subtype of both IPrint
and IEval. Similarly LangNeg = Lang & NegPrint is a subtype of Lang. Compare this to gbeta
where LangEval.Expr is not a subtype of Lang.Expr, nor is the family LangNeg a subtype ofthe family Lang.
However, gbeta and NeColus agree that LangEval is not a subtype of Lang. The NeColusside of this may seem contradictory at first, as we have seen that intersection types arise fromthe use of the merge operator, and we have created an implementation for LangEval with
implLang ,, implEval where implLang : Lang. That suggests that LangEval is a subtype ofLang. Yet, there is a flaw in our reasoning: strictly speaking, implLang ,, implEval is not oftype LangEval but instead of type Lang & EvalExt, where EvalExt is the type of implEval:
type EvalExt = { lit : Int → IEval, add : IEval → IEval → IEval };Nevertheless, the definition of implLangEval is valid because Lang & EvalExt is a subtype of
LangEval. Indeed, if we consider for the sake of simplicity only the lit field, we have that(Int → IPrint) & (Int → IEval) is a subtype of Int → IPrint & IEval. This follows froma standard subtyping axiom for distributivity of functions and intersections in the BCD
system inherited by NeColus. In conclusion, Lang & EvalExt is a subtype of both Lang and of
LangEval. However, neither of the latter two types is a subtype of the other. Indeed, LangEval
is not a subtype of Lang as the type of add is not covariantly refined and thus admitting thesubtyping is unsound. For the same reason Lang is not a subtype of LangEval.
Figure 2 shows the various relationships between the language components. Admittedly,
the figure looks quite complex because our calculus features a structural type system (asoften more foundational calculi do), whereas mainstream OO languages have nominal typesystems. This is part of the reason why we have so many subtyping relations in Fig. 2.

ECOOP 2018

22:8

The Essence of Nested Composition

NegEvalExt

LangEval

LangNegEval

NegEvalNegPrint

NegEval & NegPrint

implNegEval

implNegEval,,
implNegPrint

Lang

EvalExt

LangNeg

implNegPrint

Lang & EvalExt

implLangNeg

implLang

implLangEval

implEval

implLangNegEval
LEGEND:#Interface##composition

implmentation

subtype-of

impl-ofFigure 2 Summary diagram of the relationships between language components

Stand-Alone Extensions. Unlike in gbeta and other class-based inheritance systems, in
NeColus the extension implEval is not tied to LangEval. In that sense, it resembles trait andmixin systems that can apply the same extension to different classes. However, unlike thosesystems, implEval can also exist as a value on its own, i.e., it is not an extension per se.

2.3

Disjoint Intersection Types and Ambiguity

The above example shows that intersection types and the merge operator are closely related
to multiple inheritance. Indeed, they share a major concern with multiple inheritance,
namely ambiguity. When a subclass inherits an implementation of the same method fromtwo different parent classes, it is unclear which of the two methods is to be adopted by the
subclass. In the case where the two parent classes have a common superclass, this is known
as the diamond problem. The ambiguity problem also appears in NeColus, e.g., if we merge
two numbers to obtain 1 , , 2 of type Nat & Nat. Is the result of 1 , , 2 + 3 either 4 or 5?
Disjoint intersection types offer to statically detect potential ambiguity and to ask the
programmer to explicitly resolve the ambiguity by rejecting the program in its ambiguousform. In the previous work on λi , ambiguity is avoided by dictating that all intersection
types have to be disjoint, i.e., Nat & Nat is ill-formed because the first component has thesame type as the second.
Duplication is Harmless. While requiring that all intersections are disjoint is sufficient toguarantee coherence, it is not necessary. In fact, such requirement unnecessarily encumbers
the subtyping definition with disjointness constraints and an ad-hoc treatment of “top-like”
types. Indeed, the value 1 , , 1 of the non-disjoint type Nat & Nat is entirely unambiguous, and(1 , , 1) + 3 can obviously only result in 4. More generally, when the overlapping components
of an intersection type have the same value, there is no ambiguity problem. NeColus uses thisidea to relax λi ’s enforcement of disjointness. In the case of a merge, it is hard to statically

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:9

decide whether the two arguments have the same value, and thus NeColus still requires
disjointness. This is why in Fig. 2 we cannot define implLangNegEval by directly composing
the two existing implLangEval and implLangNeg, even though the latter two both containthe same implLang. Yet, disjointness is no longer required for the well-formedness of types
and overlapping intersections can be created implicitly through subtyping, which resultsin duplicating values at runtime. For instance, while 1 , , 1 is not expressible 1 : Nat & Nat
creates the equivalent value implicitly. In short, duplication is harmless and subtyping only
generates duplicated values for non-disjoint types.

2.4

Logical Relations for Coherence

Coherence is easy to establish for λi as its rigid rules mean that there is at most one possible
subtyping derivation between any two types. As a consequence there is only one possible
elaboration and thus one possible behavior for any program.
Two factors make establishing coherence for NeColus much more difficult: the relaxationof disjointness and the adoption of the more expressive subtyping rules from the BCD system(for which λi lacks). These two factors mean that subtyping proofs are no longer uniqueand hence that there are multiple elaborations of the same source program. For instance,
Nat & Nat is a subtype of Nat in two ways: by projection on either the first or second
component. Hence the fact that all elaborations yield the same result when evaluated has
become a much more subtle property that requires sophisticated reasoning. For instance, inthe example, we can see that coherence holds because at runtime any value of type Nat & Nat
has identical components, and thus both projections yield the same result.
For NeColus in general, we show coherence by capturing the non-ambiguity invariant in a
logical relation and showing that it is preserved by the operational semantics. A complicating
factor is that not one, but two languages are involved: the source language NeColus and thetarget language, essentially the simply-typed lambda calculus extended with coercions andrecords. The logical relation does not hold for target programs and program contexts ingeneral, but only for those that are the image of a corresponding source program or programcontext. Thus we must view everything through the lens of elaboration.

3

NeColus: Syntax and Semantics

In this section we formally present the syntax and semantics of NeColus. Compared toprior work [2, 46], NeColus has a more powerful subtyping relation. The new subtyping
relation is inspired by BCD-style subtyping, but with two noteworthy differences: subtyping
is coercive (in contrast to traditional formulations of BCD); and it is extended with records.
We also have a new target language with explicit coercions inspired by the coercion calculus
of Henglein [32]. A full technical comparison between λ+i and λi can be found in Section 3.5.

3.1

SyntaxFigure 3 shows the syntax of NeColus. For brevity of the meta-theoretic study, we do
not consider primitive operations on natural numbers, or other primitive types. They canbe easily added to the language, and our prototype implementation is indeed equippedwith common primitive types and their operations. Metavariables A, B, C range over types.
Types include naturals Nat, a top type >, function types A → B, intersection types A & B,
and singleton record types {l : A}. Metavariable E ranges over expressions. Expressions
include variables x, natural numbers i, a canonical top value >, lambda abstractions λx. E,

ECOOP 2018

22:10The Essence of Nested Composition

A, B, CEΓ

Types
Expressions
Typing contexts

::=
::=
::=

Nat | > | A → B | A & B | {l : A}x | i | > | λx. E | E1 E2 | E1 , , E2 | E : A | {l = E} | E.l• | Γ, x : A

Figure 3 Syntax of NeColus
A <: Bc(Declarative subtyping)
S-trans
A2 <: A3

S-reflA <: A

id

A <: Bc

S-rcd{l : A} <: {l : B}

c1

A1 <: A2A1 <: A3

c1 ◦ c2

S-arr
B1 <: A1{l : c}c1

S-and
A1 <: A2

S-andr
A1 & A2 <: A2

c1 → c 2

A1 & A2 <: A1

A1 <: A3

c1

top

S-andlc2

A1 <: A2 & A3

π2

π1

c2

hc1 , c2 i
S-topArr

S-distArr(A1 → A2 ) & (A1 → A3 ) <: A1 → A2 & A3
S-distRcd{l : A} & {l : B} <: {l : A & B}

A <: >

A2 <: B2

A1 → A2 <: B1 → B2

S-top

c2

dist→

> <: > → >top→

S-topRcd
dist{l}> <: {l : >}top{l}

Figure 4 Declarative specification of subtyping

applications E1 E2 , merges E1 , , E2 , annotated terms E : A, singleton records {l = E}, andrecord selections E.l.

3.2

Declarative Subtyping

Figure 4 presents the subtyping relation. We ignore the highlighted parts, and explainthem later in Section 3.4.
BCD-Style Subtyping. The subtyping rules are essentially those of the BCD type system [4],extended with subtyping for singleton records. Rules S-top and S-rcd for top types andrecord types are straightforward. Rule S-arr for function subtyping is standard. Rules Sandl, S-andr, and S-and for intersection types axiomatize that A & B is the greatest
lower bound of A and B. Rule S-distArr is perhaps the most interesting rule. This,so-called “distributivity” rule, describes the interaction between the subtyping relations forfunction types and those for intersection types. It can be shown5 that the other direction(A1 → A2 & A3 <: (A1 → A2 ) & (A1 → A3 )) and the contravariant distribution ((A1 →
A2 ) & (A3 → A2 ) <: A1 & A3 → A2 ) are both derivable from the existing subtyping rules.

5

The full derivations are found in the appendix.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

Γ`E⇒A

e

(Inference)

T-top

T-lit

Γ`>⇒>

22:11

hi

T-annoΓ`E⇐AΓ`E:A⇒AΓ ` i ⇒ Nat

i

T-var
x:A ∈ ΓT-app
Γ ` E1 ⇒ A1 → A2
e1
Γ ` E2 ⇐ A1
e2

Γ`x⇒A

Γ ` E1 E2 ⇒ A2

T-projΓ ` E ⇒ {l : A}eeΓ ` E.l ⇒ A
T-rcd

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

e

Γ`E⇒A

e 1 e2e1
A1 ∗ A2

Γ ` E1 , , E2 ⇒ A1 & A2e.l

he1 , e2 ieΓ ` {l = E} ⇒ {l : A}

Γ`E⇐A

x

{l = e}e(Checking)T-abs
Γ, x : A ` E ⇐ BeΓ ` λx. E ⇐ A → B

λx. e

T-sub
Γ`E⇒B

e

Γ`E⇐A

B <: Acce

Figure 5 Bidirectional type system of NeColus

Rule S-distRcd, which is not found in the original BCD system, prescribes the distributionof records over intersection types. The two distributivity rules are the key to enable nested
composition. The rule S-topArr is standard in BCD subtyping, and the new rule S-topRcd
plays a similar role for record types.
Non-Algorithmic. The subtyping relation in Fig. 4 is clearly no more than a specification
due to the two subtyping axioms: rules S-refl and S-trans. A sound and complete
algorithmic version is discussed in Section 5. Nevertheless, for the sake of establishingcoherence, the declarative subtyping relation is sufficient.

3.3

Typing of NeColus

The bidirectional type system for NeColus is shown in Fig. 5. Again we ignore the highlighted
parts for now.
Typing Rules and Disjointness. As with traditional bidirectional type systems, we employ
two modes: the inference mode (⇒) and the checking mode (⇐). The inference judgementΓ ` E ⇒ A says that we can synthesize a type A for expression E in the context Γ. The
checking judgement Γ ` E ⇐ A checks E against A in the context Γ. The disjointness
judgement A ∗ B used in rule T-merge is shown in Fig. 6, which states that the types A and
B are disjoint. The intuition of two types being disjoint is that their least upper bound is(isomorphic to) >. The disjointness judgement is important in order to rule out ambiguous
expressions such as 1 , , 2. Most of the typing and disjointness rules are standard and are
explained in detail in previous work [46, 2].

ECOOP 2018

22:12The Essence of Nested Composition

A∗B(Disjointness)

D-topL

D-topR

D-arr
A2 ∗ B2

D-andLA1 ∗ B>∗A

A∗>

A1 → A2 ∗ B1 → B2

A2 ∗ B

D-andRA ∗ B1A1 & A2 ∗ B

A ∗ B2A ∗ B1 & B2

D-rcdEq
A∗B

D-rcdNeq
l1 6= l2

D-axNatArr

D-axArrNat{l : A} ∗ {l : B}

{l1 : A} ∗ {l2 : B}Nat ∗ A1 → A2

A1 → A2 ∗ Nat

D-axNatRcd

D-axRcdNat

D-axArrRcd

D-axRcdArr

Nat ∗ {l : A}{l : A} ∗ Nat

A1 → A2 ∗ {l : A}{l : A} ∗ A1 → A2

Figure 6 Disjointness

Target types
Typing contexts
Target terms
Coercionsτ∆ecTarget values

v

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

Nat | hi | τ1 × τ2 | τ1 → τ2 | {l : τ }• | ∆, x : τ
x | i | hi | λx. e | e1 e2 | he1 , e2 i | {l = e} | e.l | c e
id | c1 ◦ c2 | top | top→ | top{l} | c1 → c2 | hc1 , c2 i
π1 | π2 | {l : c} | dist{l} | dist→
λx. e | hi | i | hv1 , v2 i | (c1 → c2 ) v | dist→ v | top→ v

Figure 7 λc types, terms and coercions

3.4

Elaboration Semantics

The operational semantics of NeColus is given by elaborating source expressions E into
target terms e. Our target language λc is the standard simply-typed call-by-value λ-calculus
extended with singleton records, products and coercions. The syntax of λc is shown in Fig. 7.
The meta-function | · | transforms NeColus types to λc types, and extends naturally to typing
contexts. Its definition is in the appendix.

Explicit Coercions and Coercive Subtyping. The separate syntactic category for explicit
coercions is a distinct difference from the prior works (in which they are regular terms).
Our coercions are based on those of Henglein [32], and we add more forms due to our extra
subtyping rules. Metavariable c ranges over coercions.6 Coercions express the conversion ofa term from one type to another. Because of the addition of coercions, the grammar contains
explicit coercion applications c e as a term, and various unsaturated coercion applications asvalues. The use of explicit coercions is useful for the new semantic proof of coherence basedon logical relations. The subtyping judgement in Fig. 4 has the form A <: Bc, whichsays that the subtyping derivation of A <: B produces a coercion c that converts terms oftype |A| to type |B|. Each subtyping rule has its own specific form of coercion.

6

Coercions π1 and π2 subsume the first and second projection of pairs, respectively.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:13

c ` τ1 . τ2
cotyp-refl(Coercion typing)
cotyp-transc1 ` τ2 . τ3

id ` τ . τ

c2 ` τ1 . τ2

c1 ◦ c2 ` τ1 . τ3

cotyp-top

cotyp-topArr

top ` τ . hi

top→ ` hi . hi → hi

cotyp-topRcd

cotyp-arr
c1 ` τ10 . τ1

top{l} ` hi . {l : hi}

c1 → c2 ` τ1 → τ2 . τ10 → τ20

cotyp-pairc1 ` τ1 . τ2c2 ` τ2 . τ20

c2 ` τ1 . τ3

hc1 , c2 i ` τ1 . τ2 × τ3

cotyp-projl

cotyp-projr

cotyp-rcdc ` τ1 . τ2

π1 ` τ1 × τ2 . τ1

π2 ` τ1 × τ2 . τ2

{l : c} ` {l : τ1 } . {l : τ2 }cotyp-distRcd

cotyp-distArr

dist{l} ` {l : τ1 } × {l : τ2 } . {l : τ1 × τ2 }dist→ ` (τ1 → τ2 ) × (τ1 → τ3 ) . τ1 → τ2 × τ3

Figure 8 Coercion typing

Target Typing. The typing of λc has the form ∆ ` e : τ , which is entirely standard. Only
the typing of coercion applications, shown below, deserves attention:∆`e:τc ` τ . τ0

∆ ` c e : τ0

typ-capp

Here the judgement c ` τ1 . τ2 expresses the typing of coercions, which are essentiallyfunctions from τ1 to τ2 . Their typing rules correspond exactly to the subtyping rules of
NeColus, as shown in Fig. 8.
Target Operational Semantics and Type Safety. The operational semantics of λc is mostly
unremarkable. What may be interesting is the operational semantics of coercions. Figure 9shows the single-step (−→) reduction rules for coercions. Our coercion reduction rules arequite standard but not efficient in terms of space. Nevertheless, there is existing work on
space-efficient coercions [60, 33], which should be applicable to our work as well. As standard,−→∗ is the reflexive, transitive closure of −→. We show that λc is type safe:
I Theorem 1 (Preservation). If • ` e : τ and e −→ e 0 , then • ` e 0 : τ .
I Theorem 2 (Progress). If • ` e : τ , then either e is a value, or ∃e 0 such that e −→ e 0 .
Elaboration. We are now in a position to explain the elaboration judgements Γ ` E ⇒Ae and Γ ` E ⇐ A
e in Fig. 5. The only interesting rule is rule T-sub, which applies
the coercion c produced by subtyping to the target term e to form a coercion application c e.
All the other rules do straightforward translations between source and target expressions.
To conclude, we show two lemmas that relate NeColus expressions to λc terms.
I Lemma 3 (Coercions preserve types). If A <: Bc, then c ` |A| . |B|.

Proof. By structural induction on the derivation of subtyping.

J

I Lemma 4 (Elaboration soundness). We have that:

ECOOP 2018

22:14The Essence of Nested Compositione −→ e 0(Coercion reduction)

step-idstep-transstep-top

id v −→ v(c1 ◦ c2 ) v −→ c1 (c2 v)

top v −→ hi

step-topRcd
top{l} hi −→ {l = hi}

step-topArr(top→ hi) hi −→ hi

step-pairstep-arr

hc1 , c2 i v −→ hc1 v, c2 vi((c1 → c2 ) v1 ) v2 −→ c2 (v1 (c1 v2 ))step-distArr

step-projl

step-projr(dist→ hv1 , v2 i) v3 −→ hv1 v3 , v2 v3 i

π1 hv1 , v2 i −→ v1

π2 hv1 , v2 i −→ v2

step-crcd

step-distRcd{l : c} {l = v} −→ {l = c v}

dist{l} h{l = v1 }, {l = v2 }i −→ {l = hv1 , v2 i}

Figure 9 Coercion reduction

If Γ ` E ⇒ A
If Γ ` E ⇐ A

e, then |Γ| ` e : |A|.
e, then |Γ| ` e : |A|.

Proof. By structural induction on the derivation of typing.

3.5

JComparison with λi

Below we identify major differences between λ+i and λi , which, when taken together, yielda simpler and more elegant system. The differences may seem superficial, but they havefar-reaching impacts on the semantics, especially on coherence, our major topic in Section 4.
No Ordinary Types. Apart from the extra subtyping rules, there is an important difference
from the λi subtyping relation. The subtyping relation of λi employs an auxiliary unary
relation called ordinary, which plays a fundamental role for ensuring coherence and obtaining
an algorithm [21]. The NeColus calculus discards the notion of ordinary types completely; thisyields a clean and elegant formulation of the subtyping relation. Another minor difference isthat due to the addition of the transitivity axiom (rule S-trans), rules S-andl and S-andrare simplified: an intersection type A & B is a subtype of both A and B, instead of the moregeneral form A & B <: C.
No Top-Like Types. There is a notable difference from the coercive subtyping of λi . Becauseof their syntactic proof method, they have special treatment for coercions of top-like types inorder to retain coherence. For NeColus, as with ordinary types, we do not need this kind of
ad-hoc treatment, thanks to the adoption of a more powerful proof method (cf. Section 4).
No Well-Formedness Judgement. A key difference from the type system of λi is thecomplete omission of the well-formedness judgement. In λi , the well-formedness judgementΓ ` A appears in both rules T-abs and T-sub. The sole purpose of this judgement is toenforce the invariant that all intersection types are disjoint. However, as Section 4 will
explain, the syntactic restriction is unnecessary for coherence, and merely complicates theX. Bi, B. C. d. S. Oliveira and T. Schrijvers

λc contexts
NeColus contexts

D
C

::=
::=

22:15

[·] | λx. D | D e2 | e1 D | hD, e2 i | he1 , Di | c D | {l = D} | D.l[·] | λx. C | C E2 | E1 C | E1 , , C | C , , E2 | C : A | {l = C} | C.l

Figure 10 Expression contexts of NeColus and λc

type system. The NeColus calculus discards this well-formedness judgement altogether infavour of a simpler design that is still coherent. An important implication is that even
without adding BCD subtyping, NeColus is already more expressive than λi : an expression
such as 1 : Nat & Nat is accepted in NeColus but rejected in λi . This simplification is based on
an important observation: incoherence can only originate in merges. Therefore disjointness
checking is only necessary in rule T-merge.

4

Coherence

This section constructs logical relations to establish the coherence of NeColus. Finding asuitable definition of coherence for NeColus is already challenging in its own right. In what
follows we reproduce the steps of finding a definition for coherence that is both intuitive andapplicable. Then we present the construction of logical (equivalence) relations tailored tothis definition, and the connection between logical equivalence and coherence.

4.1

In Search of CoherenceIn λi the definition of coherence is based on α-equivalence. More specifically, their coherence
property states that any two target terms that a source expression elaborates into must be
exactly the same (up to α-equivalence). Unfortunately this syntactic notion of coherenceis very fragile with respect to extensions. For example, it is not obvious how to retain thisnotion of coherence when adding more subtyping rules such as those in Fig. 4.
If we permit ourselves to consider only the syntactic aspects of expressions, then very few
expressions can be considered equal. The syntactic view also conflicts with the intuition thatthe significance of an expression lies in its contribution to the outcome of a computation [31].
Drawing inspiration from a wide range of literature on contextual equivalence [41], we want acontext-based notion of coherence. It is helpful to consider several examples before presenting
the formal definition of our new semantically founded notion of coherence.
I Example 5. The same NeColus expression 3 can be typed Nat in many ways: for instance,by rule T-lit; by rules T-sub and S-refl; or by rules T-sub, S-trans, and S-refl,resulting in λc terms 3, id 3 and (id ◦ id) 3, respectively. It is apparent that these three λcterms are “equal” in the sense that all reduce to the same numeral 3.
Expression Contexts and Contextual Equivalence. To formalize the intuition, we introduce
the notion of expression contexts. An expression context D is a term with a single hole [·](possibly under some binders) in it. The syntax of λc expression contexts can be found in
Fig. 10. The typing judgement for expression contexts has the form D : (∆ ` τ )(∆0 ` τ 0 )where (∆ ` τ ) indicates the type of the hole. This judgement essentially says that plugging
a well-typed term ∆ ` e : τ into the context D gives another well-typed term ∆0 ` D{e} : τ 0 .
We define a complete program to mean any closed term of type Nat. The following two
definitions capture the notion of contextual equivalence.
I Definition 6 (Kleene Equality). Two complete programs, e and e 0 , are Kleene equal, writtene w e 0 , iff there exists i such that e −→∗ i and e 0 −→∗ i.

ECOOP 2018

22:16The Essence of Nested Composition

I Definition 7 (λc Contextual Equivalence).
∆ ` e1 wctx e2 : τ,∆ ` e1 : τ ∧ ∆ ` e2 : τ ∧∀D. D : (∆ ` τ )(• ` Nat) =⇒ D{e1 } w D{e2 }Regarding Example 5, it seems adequate to say that 3 and id 3 are contextually equivalent.
Does this imply that coherence can be based on Definition 7? Unfortunately it cannot, as
demonstrated by the following example.
I Example 8. It may be counter-intuitive that two λc terms λx. π1 x and λx. π2 x should
also be considered equal. To see why, first note that they are both translations of thesame NeColus expression: (λx. x) : Nat & Nat → Nat. What can we do with this lambda
abstraction? We can apply it to 1 : Nat & Nat for example. In that case, we get twotranslations (λx. π1 x) h1, 1i and (λx. π2 x) h1, 1i, which both reduce to the same numeral 1.
However, λx. π1 x and λx. π2 x are definitely not equal according to Definition 7, as one canfind a context [·] h1, 2i where the two terms reduce to two different numerals. The problem
is that not every well-typed λc term can be obtained from a well-typed NeColus expression
through the elaboration semantics. For example, [·] h1, 2i should not be considered because
the (non-disjoint) source expression 1 , , 2 is rejected by the type system of the source calculus
NeColus and thus never gets elaborated into h1, 2i.
NeColus Contexts and Refined Contextual Equivalence. Example 8 hints at a shift from
λc contexts to NeColus contexts C, whose syntax is shown in Fig. 10. Due to the bidirectional
nature of the type system, the typing judgement of C features 4 different forms:
C : (Γ ⇒ A) 7→ (Γ0 ⇒ A0 )D

C : (Γ ⇐ A) 7→ (Γ0 ⇒ A0 )D

C : (Γ ⇒ A) 7→ (Γ0 ⇐ A0 )D

C : (Γ ⇐ A) 7→ (Γ0 ⇐ A0 )D

We write C : (Γ ⇔ A) 7→ (Γ0 ⇔0 A0 )D to abbreviate the above 4 different forms. Take
C : (Γ ⇒ A) 7→ (Γ0 ⇒ A0 )D for example, it reads given a well-typed NeColus expression
Γ ` E ⇒ A, we have Γ0 ` C{E} ⇒ A0 . The judgement also generates a λc context D suchthat D : (|Γ| ` |A|)(|Γ0 | ` |A0 |) holds by construction. The typing rules appear in the
appendix. Now we are ready to refine Definition 7’s contextual equivalence to take into
consideration both NeColus and λc contexts.
I Definition 9 (NeColus Contextual Equivalence).
Γ ` E1 wctx E2 : A,∀e1 , e2 , C, D. Γ ` E1 ⇒ A
e1 ∧ Γ ` E 2 ⇒ A
e2 ∧C : (Γ ⇒ A) 7→ (• ⇒ Nat)D =⇒ D{e1 } w D{e2 }I Remark. For brevity we only consider expressions in the inference mode. Our Coq
formalization is complete with two modes.
Regarding Example 8, a possible NeColus context is [·] 1 : (• ⇒ Nat & Nat → Nat) 7→ (• ⇒Nat)[·] h1, 1i. We can verify that both λx. π1 x and λx. π2 x produce 1 in the context[·] h1, 1i. Of course we should consider all possible contexts to be certain they are truly equal.
From now on, we use the symbol wctx to refer to contextual equivalence in Definition 9.
With Definition 9 we can formally state that NeColus is coherent in the following theorem:
I Theorem 10 (Coherence). If Γ ` E ⇒ A then Γ ` E wctx E : A.
For the same reason as in Definition 9, we only consider expressions in the inference mode.
The rest of the section is devoted to proving that Theorem 10 holds.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:17(v1 , v2 ) ∈ VJNat; NatK , ∃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({l = v1 }, {l = v2 }) ∈ VJ{l : τ1 }; {l : τ2 }K , (v1 , v2 ) ∈ VJτ1 ; τ2 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
(v1 , v2 ) ∈ VJτ1 ; τ2 K , true

otherwise(e1 , e2 ) ∈ EJτ1 ; τ2 K , ∃v1 v2 , e1 −→∗ v1 ∧ e2 −→∗ v2 ∧ (v1 , v2 ) ∈ VJτ1 ; τ2 K

Figure 11 Logical relations for λc

4.2

Logical Relations

Intuitive as Definition 9 may seem, it is generally very hard to prove contextual equivalence
directly, since it involves quantification over all possible contexts. Worse still, two kinds ofcontexts are involved in Theorem 10, which makes reasoning even more tedious. The key tosimplifying the reasoning is to exploit types by using logical relations [63, 61, 48].
In Search of a Logical Relation. It is worth pausing to ponder what kind of relation we arelooking for. The high-level intuition behind the relation is to capture the notion of “coherent”
values. These values are unambiguous in every context. A moment of thought leads us to
the following important observations:
I Observation 1 (Disjoint values are unambiguous). The relation should relate values originatingfrom disjoint intersection types. Those values are essentially translated from merges, andsince rule T-merge ensures disjointness, they are unambiguous. For example, h1, {l = 1}icorresponds to the type Nat & {l : Nat}. It is always clear which one to choose (1 or {l = 1})
no matter how this pair is used in certain contexts.
I Observation 2 (Duplication is unambiguous). The relation should relate values originatingfrom non-disjoint intersection types, only if the values are duplicates. This may sound bafflingsince the whole point of disjointness is to rule out (ambiguous) expressions such as 1 , , 2.
However, 1 , , 2 never gets elaborated, and the only values corresponding to Nat & Nat arethose pairs such as h1, 1i, h2, 2i, etc. Those values are essentially generated from rule T-sub
and are also unambiguous.
To formalize values being “coherent” based on the above observations, Figure 11 defines
two (binary) logical relations for λc , one for values (VJτ1 ; τ2 K) and one for terms (EJτ1 ; τ2 K).
We require that any two values (v1 , v2 ) ∈ VJτ1 ; τ2 K are closed and well-typed. For succinctness,
we write VJτ K to mean VJτ ; τ K, and similarly for EJτ K.
I Remark. The logical relations are heterogeneous, parameterized by two types, one for eachargument. This is intended to relate values of different types.

I Remark. The logical relations resemble those given by Biernacki and Polesiuk [8], as bothare heterogeneous. However, two important differences are worth pointing out. Firstly, ourvalue relation for product types (VJτ1 × τ2 ; τ3 K and VJτ3 ; τ1 × τ2 K) is unusual. Secondly, theirvalue relation disallows relating functions with natural numbers, while ours does not. As we
explain shortly, both points are related to disjointness.

ECOOP 2018

22:18The Essence of Nested Composition

First let us consider VJτ1 ; τ2 K. The first three cases are standard: Two natural numbers
are related iff they are the same numeral. Two functions are related iff they map related
arguments to related results. Two singleton records are related iff they have the same label
and their fields are related. These cases reflect Observation 2: the same type corresponds tothe same value.
In the next two cases one of the parameterized types is a product type. In those cases,
the relation distributes over the product constructor ×. This may look strange at first, since
the traditional way of relating pairs is by relating their components pairwise. That is, hv1 , v2 iand hv10 , v20 i are related iff (1) v1 and v10 are related and (2) v2 and v20 are related. According
to our definition, we also require that (3) v1 and v20 are related and (4) v2 and v10 are related.
The design of these two cases is influenced by the disjointness of intersection types. Below
are two rules dealing with intersection types:
A1 ∗ BA2 ∗ B

A1 & A2 ∗ B

A ∗ B1
D-andLA ∗ B2A ∗ B1 & B2

D-andR

Notice the structural similarity between these two rules and the two cases. Now it is clear thatthe cases for products manifests disjointness of intersection types, reflecting Observation 1.
Together with the last case, we can show that disjointness and the value relation are connectedby the following lemma:
I Lemma 11 (Disjoint values are in a value relation). If A1 ∗ A2 and v1 : |A1 | and v2 : |A2 |,then (v1 , v2 ) ∈ VJ|A1 |; |A2 |K.
Proof. By induction on the derivation of disjointness.

J

Next we consider EJτ1 ; τ2 K, which is standard. Informally it expresses that two closed
terms e1 and e2 are related iff they evaluate to two values v1 and v2 that are related.
Logical Equivalence. The logical relations can be lifted to open terms in the usual way.
First we give the semantic interpretation of typing contexts:
I Definition 12 (Interpretation of Typing Contexts). (γ1 , γ2 ) ∈ GJ∆1 ; ∆2 K is defined as follows:(∅, ∅) ∈ GJ•; •K(v1 , v2 ) ∈ VJτ1 ; τ2 K
(γ1 , γ2 ) ∈ GJ∆1 ; ∆2 K
fresh x(γ1 [x 7→ v1 ], γ2 [x 7→ v2 ]) ∈ GJ∆1 , x : τ1 ; ∆2 , x : τ2 K

Two open terms are related if every pair of related closing substitutions makes them related:
I Definition 13 (Logical equivalence). Let ∆1 ` e1 : τ1 and ∆2 ` e2 : τ2 .
∆1 ; ∆2 ` e1 wlog e2 : τ1 ; τ2 , ∀γ1 , γ2 . (γ1 , γ2 ) ∈ GJ∆1 ; ∆2 K =⇒ (γ1 e1 , γ2 e2 ) ∈ EJτ1 ; τ2 K
For succinctness, we write ∆ ` e1 wlog e2 : τ to mean ∆; ∆ ` e1 wlog e2 : τ ; τ .

4.3

Establishing CoherenceWith all the machinery in place, we are now ready to prove Theorem 10. But we need several
lemmas to set the stage.
First we show compatibility lemmas, which state that logical equivalence is preservedby every language construct. Most are standard and thus are omitted. We show only one
compatibility lemma that is specific to our relations:

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:19

I Lemma 14 (Coercion Compatibility). Suppose that c ` τ1 . τ2 ,If ∆1 ; ∆2 ` e1 wlog e2 : τ1 ; τ0 then ∆1 ; ∆2 ` c e1 wlog e2 : τ2 ; τ0 .
If ∆1 ; ∆2 ` e1 wlog e2 : τ0 ; τ1 then ∆1 ; ∆2 ` e1 wlog c e2 : τ0 ; τ2 .
Proof. By induction on the typing derivation of the coercion c.

J

The “Fundamental Property” states that any well-typed expression is related to itself
by the logical relation. In our elaboration setting, we rephrase it so that any two λc terms
elaborated from the same NeColus expression are related by the logical relation. To prove it,
we require Theorem 15.
I Theorem 15 (Inference Uniqueness). If Γ ` E ⇒ A1 and Γ ` E ⇒ A2 , then A1 ≡ A2 .
I Theorem 16 (Fundamental Property). We have that:
If Γ ` E ⇒ A
e and Γ ` E ⇒ A
e 0 , then |Γ| ` e wlog e 0 : |A|.
If Γ ` E ⇐ A
e and Γ ` E ⇐ A
e 0 , then |Γ| ` e wlog e 0 : |A|.
Proof. The proof follows by induction on the first derivation. The most interesting case isrule T-sub where we need Theorem 15 to be able to apply the induction hypothesis. Then
we apply Lemma 14 to say that the coercion generated preserves the relation between terms.
For the other cases we use the appropriate compatibility lemmas.
J
I Remark. It is interesting to ask whether the Fundamental Property holds in the target
language. That is, if ∆ ` e : τ then ∆ ` e wlog e : τ . Clearly this does not hold for every
well-typed λc term. However, as we have emphasized, we do not need to consider every λcterm. Our logical relation is carefully formulated so that the Fundamental Property holds inthe source language.
We show that logical equivalence is preserved by NeColus contexts:
I Lemma 17 (Congruence). If C : (Γ ⇔ A) 7→ (Γ0 ⇔0 A0 )D, Γ ` E1 ⇔ A
Γ ` E2 ⇔ A
e2 and |Γ| ` e1 wlog e2 : |A|, then |Γ0 | ` D{e1 } wlog D{e2 } : |A0 |.

e1 ,Proof. By induction on the typing derivation of the context C, and applying the compatibility
lemmas where appropriate.
J
I Lemma 18 (Adequacy). If • ` e1 wlog e2 : Nat then e1 w e2 .
Proof. Adequacy follows easily from the definition of the logical relation.

J

Next up is the proof that logical relation is sound with respect to contextual equivalence:
I Theorem 19 (Soundness w.r.t. Contextual Equivalence). If Γ ` E1 ⇒ A
Γ ` E2 ⇒ A
e2 and |Γ| ` e1 wlog e2 : |A| then Γ ` E1 wctx E2 : A.

e1 andD. By
Proof. From Definition 9, we are given a context C : (Γ ⇒ A) 7→ (• ⇒ Nat)
Lemma 17 we have • ` D{e1 } wlog D{e2 } : Nat, thus D{e1 } w D{e2 } by Lemma 18.
J
Armed with Theorem 16 and Theorem 19, coherence follows directly.
I Theorem 10 (Coherence). If Γ ` E ⇒ A then Γ ` E wctx E : A.
Proof. Immediate from Theorem 16 and Theorem 19.

J

ECOOP 2018

22:20The Essence of Nested Composition

4.4

Some Interesting Corollaries

To showcase the strength of the new proof method, we can derive some interesting corollaries.
For the most part, they are direct consequences of logical equivalence which carry over tocontextual equivalence.
Corollary 20 says that merging a term of some type with something else does notaffect its semantics. Corollary 21 and Corollary 22 express that merges are commutative
and associative, respectively. Corollary 23 states that coercions from the same types are“coherent”.
I Corollary 20 (Merge is Neutral). If Γ ` E1 ⇒ A and Γ ` E1 , , E2 ⇒ A, then Γ ` E1 wctx
E1 , , E2 : A
I Corollary 21 (Merge is Commutative). If Γ ` E1 , , E2 ⇒ A and Γ ` E2 , , E1 ⇒ A, thenΓ ` E1 , , E2 wctx E2 , , E1 : A.
I Corollary 22 (Merge is Associative). If Γ ` (E1 , , E2 ) , , E3 ⇒ A and Γ ` E1 , , (E2 , , E3 ) ⇒A, then Γ ` (E1 , , E2 ) , , E3 wctx E1 , , (E2 , , E3 ) : A.
I Corollary 23 (Coercions Preserve Semantics). If A <: B
∆ ` λx. c1 x wlog λx. c2 x : |A| → |B|.

5

c1 and A <: B

c2 , then

Algorithmic Subtyping

This section presents an algorithm that implements the subtyping relation in Fig. 4. While
BCD subtyping is well-known, the presence of a transitivity axiom in the rules means thatthe system is not algorithmic. This raises an obvious question: how to obtain an algorithm
for this subtyping relation? Laurent [37] has shown that simply dropping the transitivity
rule from the BCD system is not possible without losing expressivity. Hence, this avenue forobtaining an algorithm is not available. Instead, we adapt Pierce’s decision procedure [47]for a subtyping system (closely related to BCD) to obtain a sound and complete algorithm
for our BCD extension. Our algorithm extends Pierce’s decision procedure with subtyping of
singleton records and coercion generation. We prove in Coq that the algorithm is sound andcomplete with respect to the declarative version. At the same time we find some errors andmissing lemmas in Pierce’s original manual proofs.

5.1

The Subtyping Algorithm

Figure 12 shows the algorithmic subtyping judgement L ` A ≺: B
c. This judgement
is the algorithmic counterpart of the declarative judgement A <: L → B
c, where thesymbol L stands for a queue of types and labels. Definition 24 converts a queue to a type:
I Definition 24. L → A is inductively defined as follows:[] → A = A(L, B) → A = L → (B → A)

(L, {l}) → A = L → {l : A}

For instance, if L = A, B, {l}, then L → C abbreviates A → B → {l : C}.
The basic idea of L ` A ≺: B
c is to first perform a structural analysis of B, which
descends into both sides of & ’s (rule A-and), into the right side of →’s (rule A-arr), andinto the fields of records (rule A-rcd) until it reaches one of the two base cases, Nat or >. If
the base case is >, then the subtyping holds trivially (rule A-top). If the base case is Nat,the algorithm performs a structural analysis of A, in which L plays an important role. The
left sides of →’s are pushed onto L as they are encountered in B and popped off again later,

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

L ` A ≺: B

c

A-and
L ` A ≺: B1

c1

22:21

(Algorithmic subtyping)L ` A ≺: B2

L ` A ≺: B1 & B2

JLK& ◦ hc1 , c2 i

A-top
L ` A ≺: >A-arr
L, B1 ` A ≺: B2

c2

c

L ` A ≺: {l : B}ccA-arrNat[] ` A ≺: A1

L ` A2 ≺: Nat

c1

A, L ` A1 → A2 ≺: Natc{l}, L ` {l : A} ≺: Nat

A-rcd
L, {l} ` A ≺: B

L ` A ≺: B1 → B2

JLK> ◦ top

A-rcdNatL ` A ≺: Natc{l : c}c2

c1 → c2

A-andN1
L ` A1 ≺: Natc

L ` A1 & A2 ≺: Natc ◦ π1

A-andN2
L ` A2 ≺: Nat

c

A-nat

L ` A1 & A2 ≺: Natc ◦ π2[] ` Nat ≺: Nat

id

Figure 12 Algorithmic subtyping of NeColusleft to right, as →’s are encountered in A (rule A-arrNat). Similarly, the labels are pushed
onto L as they are encountered in B and popped off again later, left to right, as records areencountered in A (rule A-rcdNat). The remaining rules are similar to their declarative
counterparts. Let us illustrate the algorithm with an example derivation (for space reasons
we use N and S to denote Nat and String respectively), which is essentially the one used by
the add field in Section 2. The readers can try to give a corresponding derivation using thedeclarative subtyping and see how rule S-trans plays an essential role there.
DD0{l}, N & S, N & S ` {l : N → N → N} & {l : S → S → S} ≺: N & S

A-and{l} ` {l : N → N → N} & {l : S → S → S} ≺: N & S → N & S → N & S

A-arr(twice){l : N → N → N} & {l : S → S → S} ≺: {l : N & S → N & S → N & S}

A-rcd

where the sub-derivation D is shown below (D0 is similar):
...

...

N & S ≺: N

N & S ` N → N ≺: N

N & S, N & S ` N → N → N ≺: N

A-arrNat{l}, N & S, N & S ` {l : N → N → N} ≺: N

A-rcdNat{l}, N & S, N & S ` {l : N → N → N} & {l : S → S → S} ≺: N

A-andN1

Now consider the coercions. Algorithmic subtyping uses the same set of coercions as
declarative subtyping. However, because algorithmic subtyping has a different structure, therules generate slightly more complicated coercions. Two meta-functions J·K> and J·K& usedin rules A-top and A-and respectively, are meant to generate correct forms of coercions.
They are defined recursively on L and are shown in Fig. 13.

5.2

Correctness of the Algorithm

To establish the correctness of the algorithm, we must show that the algorithm is both soundand complete with respect to the declarative specification. While soundness follows quite

ECOOP 2018

22:22The Essence of Nested Composition

J[]K> = top

J[]K& = id

J{l}, LK> = {l : JLK> } ◦ top{l}J{l}, LK& = {l : JLK& } ◦ dist{l}JA, LK> = (top → JLK> ) ◦ (top→ ◦ top)

JA, LK& = (id → JLK& ) ◦ dist→

Figure 13 Meta-functions of coercions

easily, completeness is much harder. The proof of completeness essentially follows that of
Pierce [47] in that we need to show the algorithmic subtyping is reflexive and transitive.
Soundness of the Algorithm.

The proof of soundness is straightforward.

I Theorem 25 (Soundness). If L ` A ≺: B

c then A <: L → B

c.

Proof. By induction on the derivation of the algorithmic subtyping.

J

Completeness of the Algorithm. Completeness, however, is much harder. The reason isthat, due to the use of L, reflexivity and transitivity are not entirely obvious. We need tostrengthen the induction hypothesis by introducing the notion of a set, U(A), of “reflexive
supertypes” of A, as defined below:
U(>) , {>}U(Nat) , {Nat}U({l : A}) , {{l : B} | B ∈ U(A)}U(A & B) , U(A) ∪ U(B) ∪ {A & B}

U(A → B) , {A → C | C ∈ U(B)}We show two lemmas about U(A) that are crucial in the subsequent proofs.
I Lemma 26. A ∈ U(A)Proof. By induction on the structure of A.

J

I Lemma 27. If A ∈ U(B) and B ∈ U(C), then A ∈ U(C).
Proof. By induction on the structure of B.

J

I Remark. Lemma 27 is not found in Pierce’s proofs [47], which is crucial in Lemma 28,
from which reflexivity (Lemma 29) follows immediately.
I Lemma 28. If L → B ∈ U(A) then there exists c such that L ` A ≺: Bc.

Proof. By induction on size(A) + size(B) + size(L).

J

Now it immediately follows that the algorithmic subtyping is reflexive.
I Lemma 29 (Reflexivity). For every A there exists c such that [] ` A ≺: Ac.

Proof. Immediate from Lemma 26 and Lemma 28.

J

We omit the details of the proof of transitivity.
I Lemma 30 (Transitivity). If [] ` A1 ≺: A2
c such that [] ` A1 ≺: A3c.

c1 and [] ` A2 ≺: A3

c2 , then there exists

With reflexivity and transitivity in position, we show the main theorem.
I Theorem 31 (Completeness). If A <: Bc then there exists c 0 such that [] ` A ≺: B

c0 .

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:23

Proof. By induction on the derivation of the declarative subtyping and applying Theorems 29
and 30 where appropriate.
J
I Remark. Pierce’s proof is wrong [47, pp. 20, Case F] in the caseB1 <: A1

c1

A2 <: B2

A1 → A2 <: B1 → B2

c2

c1 → c2

S-arr

where he concludes from the inductive hypotheses [] ` B1 ≺: A1 and [] ` A2 ≺: B2 that[] ` A1 → A2 ≺: B1 → B2 (rules 6a and 3). However his rule 6a (our rule A-arrNat) only
works for primitive types, and is thus not applicable in this case. Instead we need a few
technical lemmas to support the argument.
I Remark. It is worth pointing out that the two coercions c and c 0 in Theorem 31 arecontextually equivalent, which follows from Theorem 25 and Corollary 23.

6

Related Work

Coherence. In calculi that feature coercive subtyping, a semantics that interprets thesubtyping judgement by introducing explicit coercions is typically defined on typing derivations rather than on typing judgements. A natural question that arises for such systems
is whether the semantics is coherent, i.e., distinct typing derivations of the same typing
judgement possess the same meaning. Since Reynolds [55] proved the coherence of a calculus
with intersection types, based on the denotational semantics for intersection types, many
researchers have studied the problem of coherence in a variety of typed calculi. Below wesummarize two commonly-found approaches in the literature.
Breazu-Tannen et al. [10] proved the coherence of a coercion translation from Fun [13]extended with recursive types to System F by showing that any two typing derivations of
the same judgement are normalizable to a unique normal derivation. Ghelli [20] presented
a translation of System F≤ into a calculus with explicit coercions and showed that any
derivations of the same judgement are translated to terms that are normalizable to a uniquenormal form. Following the same approach, Schwinghammer [59] proved the coherence of
coercion translation from Moggi’s computational lambda calculus [40] with subtyping.
Central to the first approach is to find a normal form for a representation of the derivationand show that normal forms are unique for a given typing judgement. However, this approachcannot be directly applied to Curry-style calculi, i.e, where the lambda abstractions are nottype annotated. Also this line of reasoning cannot be used when the calculus has generalrecursion. Biernacki and Polesiuk [8] considered the coherence problem of coercion semantics.
Their criterion for coherence of the translation is contextual equivalence in the target calculus.
They presented a construction of logical relations for establishing so constructed coherence
for coercion semantics, applicable in a variety of calculi, including delimited continuations
and control-effect subtyping.
As far as we know, our work is the first to use logical relations to show the coherence
for intersection types and the merge operator. The BCD subtyping in our setting poses a
non-trivial complication over Biernacki and Polesiuk’s simple structural subtyping. Indeed,because any two coercions between given types are behaviorally equivalent in the target
language, their coherence reasoning can all take place in the target language. This is nottrue in our setting, where coercions can be distinguished by arbitrary target programs, but
not those that are elaborations of source programs. Hence, we have to restrict our reasoning
to the latter class, which is reflected in a more complicated notion of contextual equivalenceand our logical relation’s non-trivial treatment of pairs.

ECOOP 2018

22:24The Essence of Nested Composition

Intersection Types and the Merge Operator. Forsythe [54] has intersection types anda merge-like operator. However to ensure coherence, various restrictions were added tolimit the use of merges. For example, in Forsythe merges cannot contain more than one
function. Castagna et al. [15] proposed a coherent calculus with a special merge operator
that works on functions only. More recently, Dunfield [23] shows significant expressivenessof type systems with intersection types and a merge operator. However his calculus lacks
coherence. The limitation was addressed by Oliveira et al. [46], who introduced disjointness
to ensure coherence. The combination of intersection types, a merge operator and parametricpolymorphism, while achieving coherence was first studied in the Fi calculus [2]. Compared
to prior work, NeColus simplifies type systems with disjoint intersection types by removing
several restrictions. Furthermore, NeColus adopts a more powerful subtyping relation basedon BCD subtyping, which in turn requires the use of a more powerful logical relations based
method for proving coherence.
BCD Type System and Decidability. The BCD type system was first introduced by
Barendregt et al. [4]. It is derived from a filter lambda model in order to characterize exactly
the strongly normalizing terms. The BCD type system features a powerful subtyping relation,
which serves as a base for our subtyping relation. Bessai el at. [5] showed how to type classes
and mixins in a BCD-style record calculus with Bracha-Cook’s merge operator [9]. Theirmerge can only operate on records, and they only study a type assignment system. The
decidability of BCD subtyping has been shown in several works [47, 35, 52, 62]. Laurent [36]has formalized the relation in Coq in order to eliminate transitivity cuts from it, but his
formalization does not deliver an algorithm. Based on Statman’s work [62], Bessai et al. [6]show a formally verified subtyping algorithm in Coq. Our Coq formalization follows adifferent idea based on Pierce’s decision procedure [47], which is shown to be easily extensible
to coercions and records. In the course of our mechanization we identified several mistakesin Pierce’s proofs, as well as some important missing lemmas.
Family Polymorphism. There has been much work on family polymorphism since Ernst’s
original proposal [25]. Family polymorphism provides an elegant solution to the Expression
Problem. Although a simple Scala solution does exist without requiring family polymorphism(e.g., see Wang and Oliveira [65]), Scala does not support nested composition: programmers
need to manually compose all the classes from multiple extensions. Generally speaking,systems that support family polymorphism usually require quite sophisticated mechanisms
such as dependent types.
There are two approaches to family polymorphism: the original object family approachof Beta (e.g., virtual classes [38]) treats nested classes as attributes of objects of the familyclasses. Path-dependent types are used to ensure type safety for virtual types and virtual
classes in the calculus vc [27]. As for conflicts, vc follows the mixin-style by allowing therightmost class to take precedence. This is in contrast to NeColus where conflicts are detected
statically and resolved explicitly. In the class family approach of Concord [34], Jx andJ& [42, 43], nested classes and types are attributes of the family classes directly. Jx supports
nested inheritance, a class family mechanism that allows nesting of arbitrary depth. J&
is a language that supports nested intersection, building on top of Jx. Similar to NeColus,
intersection types play an important role in J&, which are used to compose packages/classes.
Unlike NeColus, J& does not have a merge-like operator. When conflicts arise, prefix types
can be exploited to resolve the ambiguity. J&s [50] is an extension of the Java languagethat adds class sharing to J&. Saito et al. [57] identified a minimal, lightweight set of

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:25

language features to enable family polymorphism, Corradi et al. [19] present a language
design that integrates modular composition and nesting of Java-like classes. It features aset of composition operators that allow to manipulate nested classes at any depth level.
More recently, a Java-like language called Familia [66] were proposed to combine subtyping
polymorphism, parametric polymorphism and family polymorphism. The object and classfamily approaches have even been combined by the work on Tribe [16].
Compared with those systems, which usually focus on getting a relatively complex Javalike language with family polymorphism, NeColus focuses on a minimal calculus that supports
nested composition. NeColus shows that a calculus with the merge operator and a variant of
BCD captures the essence of nested composition. Moreover NeColus enables new insights on
the subtyping relations of families. NeColus’s goal is not to support full family polymorphism
which, besides nested composition, also requires dealing with other features such as self
types [12, 56] and mutable state. Supporting these features is not the focus of this paper,
but we expect to investigate those features in the future.

7

Conclusions and Future Work

We have proposed NeColus, a type-safe and coherent calculus with disjoint intersection types,
and support for nested composition/subtyping. It improves upon earlier work with a more
flexible notion of disjoint intersection types, which leads to a clean and elegant formulationof the type system. Due to the added flexibility we have had to employ a more powerfulproof method based on logical relations to rigorously prove coherence. We also show how
NeColus supports essential features of family polymorphism, such as nested composition. We
believe NeColus provides insights into family polymorphism, and has potential for practicalapplications for extensible software designs.
A natural direction for future work is to enrich NeColus with parametric polymorphism.
There is abundant literature on logical relations for parametric polymorphism [53]. The
main challenge in the definition of the logical relation is the clause that relates type variables
with arbitrary types. Careful measures are to be taken to avoid potential circularity due toimpredicativity.7 With the combination of parametric polymorphism and nested composition,
an interesting application that we intend to investigate is native support for a highly modular
form of Object Algebras [45, 7] and Visitors (or the finally tagless approach [14]).
Another direction for future work is to add mutable references, which would affect two
aspects of our metatheory: type safety and coherence. For type safety, we expect that lessons
learned from previous work on family polymorphism and mutability on OO apply to ourwork. For example, it is well-known that subtyping in the presence of mutable state often
needs restrictions. Given such suitable restrictions we expect that type-safety in the presenceof mutability still holds. For coherence, it would be a major technical challenge to adjust ourcoherence proof and its Coq mechanization: logical relations that account for mutable state(e.g., see Ahmed’s thesis [1]) introduce significant complexity.
References
1

7

Amal Jamil Ahmed. Semantics of types for mutable state. PhD thesis, Princeton University,
2004.

Our prototype implementation already supports polymorphism, but we are still in the process ofextending our Coq development with polymorphism.

ECOOP 2018

22:26The Essence of Nested Composition

2
3
4

5

6
7
8
9
10
11
12
13
14

15
16
17
18
19
20
21
22

23

João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In
European Symposium on Programming, 2017.
Nada Amin, Adriaan Moors, and Martin Odersky. Dependent object types. In Workshop
on Foundations of Object-Oriented Languages, 2012.
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda
model and the completeness of type assignment. The journal of symbolic logic, 48(04):931–
940, 1983.
Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de’Liguoro. Typing classes and mixins with intersection types. In Workshop on Intersection Types andRelated Systems (ITRS), 2014.
Jan Bessai, Andrej Dudenhefner, Boris Düdder, and Jakob Rehof. Extracting a formallyverified subtyping algorithm for intersection types from ideals and filters. In TYPES, 2016.
Xuan Bi and Bruno C. d. S. Oliveira. Typed first-class traits. In European Conference on
Object-Oriented Programming, 2018.
Dariusz Biernacki and Piotr Polesiuk. Logical relations for coherence of effect subtyping.
In LIPIcs, 2015.
Gilad Bracha and William R. Cook. Mixin-based inheritance. In International Conference
on Object-Oriented Programming, Systems, Languages, and Applications, 1990.
Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as
implicit coercion. Information and Computation, 93(1):172–221, 1991.
Kim Bruce, Luca Cardelli, Giuseppe Castagna, Gary T Leavens, Benjamin Pierce, et al.
On binary methods. In Theory and Practice of Object Systems, 1996.
Kim B. Bruce, Angela Schuett, and Robert van Gent. Polytoil: A type-safe polymorphic
object-oriented language. In European Conference on Object-Oriented Programming, 1995.
Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471–523, 1985.
Jacques Carette, Oleg Kiselyov, and Chung-Chieh Shan. Finally tagless, partially evaluated:
Tagless staged interpreters for simpler typed languages. Journal of Functional Programming,
19(05):509, 2009.
Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions with subtyping. In LFP, 1992.
David Clarke, Sophia Drossopoulou, James Noble, and Tobias Wrigstad. Tribe: More
Types for Virtual Classes. In AOSD, 2007.
Adriana B Compagnoni and Benjamin C Pierce. Higher-order intersection types and multiple inheritance. MSCS, 6(5):469–501, 1996.
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters ofsolvable terms. Mathematical Logic Quarterly, 1981.
Andrea Corradi, Marco Servetto, and Elena Zucca. DeepFJig — modular composition ofnested classes. The Journal of Object Technology, 11(2):1:1, 2012.
Pierre-Louis Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing andtype-checking in f ≤. MSCS, 2(01):55, 1992.
Rowan Davies and Frank Pfenning. Intersection types and computational effects. In International Conference on Functional Programming, 2000.
Stéphane Ducasse, Oscar Nierstrasz, Nathanael Schärli, Roel Wuyts, and Andrew P Black.
Traits: A mechanism for fine-grained reuse. ACM Transactions on Programming Languages
and Systems (TOPLAS), 28(2):331–388, 2006.
Joshua Dunfield. Elaborating intersection and union types. Journal of Functional Programming, 24:133–165, 2014.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

24

25
26
27
28
29
30
31
32
33
34

35
36
37
38

39
40
41
42

43

44

45
46

22:27

Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions incall-by-value languages. In Foundations of Software Science and Computation Structure(FoSSaCS), 2003.
Erik Ernst. Family polymorphism. In European Conference on Object-Oriented Programming, 2001.
Erik Ernst. Higher-order hierarchies. In European Conference on Object-Oriented Programming, 2003.
Erik Ernst, Klaus Ostermann, and William R. Cook. A virtual class calculus. In Symposiumon Principles of Programming Languages, 2006.
Facebook. Flow. https://flow.org/, 2014.
Kathleen Fisher and John Reppy. A typed calculus of traits. In Workshop on Foundationsof Object-Oriented Languages, 2004.
Tim Freeman and Frank Pfenning. Refinement types for ML. In Conference on Programming Language Design and Implementation, 1991.
Robert Harper. Practical Foundations for Programming Languages. Cambridge University
Press, 2016.
Fritz Henglein. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197–230, jun 1994.
David Herman, Aaron Tomb, and Cormac Flanagan. Space-efficient gradual typing. HigherOrder and Symbolic Computation, 23(2):167, 2010.
Paul Jolly, Sophia Drossopoulou, Christopher Anderson, and Klaus Ostermann. Simple dependent types: Concord. In European Conference on Object-Oriented Programming Workshop on Formal Techniques for Java Programs (FTfJP), 2004.
Toshihiko Kurata and Masako Takahashi. Decidable properties of intersection type systems.
Typed Lambda Calculi and Applications, pages 297–311, 1995.
Olivier Laurent. Intersection types with subtyping by means of cut elimination. Fundamenta Informaticae, 121(1-4):203–226, 2012.
Olivier Laurent. A syntactic introduction to intersection types. Unpublished note, 2012.
O. L. Madsen and B. Moller-Pedersen. Virtual classes: a powerful mechanism in objectoriented programming. In International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 1989.
Microsoft. Typescript. https://www.typescriptlang.org/, 2012.
Eugenio Moggi. Notions of computation and monads. Information and Computation,
93(1):55–92, 1991.
James Hiram Morris Jr. Lambda-calculus models of programming languages. PhD thesis,
Massachusetts Institute of Technology, 1969.
Nathaniel Nystrom, Stephen Chong, and Andrew C. Myers. Scalable extensibility via
nested inheritance. In International Conference on Object-Oriented Programming, Systems,
Languages, and Applications, 2004.
Nathaniel Nystrom, Xin Qi, and Andrew C. Myers. J&: Nested Intersection for Scalable Software Composition. In International Conference on Object-Oriented Programming,
Systems, Languages, and Applications, 2006.
Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth,
Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger.
An overview of the scala programming language. Technical report, EPFL, 2004.
Bruno C. d. S. Oliveira and William R. Cook. Extensibility for the masses. In European
Conference on Object-Oriented Programming, 2012.
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In
International Conference on Functional Programming, 2016.

ECOOP 2018

22:28The Essence of Nested Composition

47
48
49
50
51
52
53
54
55
56
57
58

59
60
61
62
63
64
65
66

Benjamin C Pierce. A decision procedure for the subtype relation on intersection types
with bounded variables. Technical report, Carnegie Mellon University, 1989.
Gordon Plotkin. Lambda-definability and logical relations. Edinburgh University, 1973.
Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry:
essays on combinatory logic, lambda calculus and formalism, 1980.
Xin Qi and Andrew C. Myers. Sharing classes between families. In Conference on Programming Language Design and Implementation, 2009.
Redhat. Ceylon. https://ceylon-lang.org/, 2011.
Jakob Rehof and Paweł Urzyczyn. Finite combinatory logic with intersection types. In
International Conference on Typed Lambda Calculi and Applications, 2011.
John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP, 1983.
John C Reynolds. Preliminary design of the programming language forsythe. Technicalreport, Carnegie Mellon University, 1988.
John C. Reynolds. The coherence of languages with intersection types. In Lecture Notes
in Computer Science (LNCS), pages 675–700. Springer Berlin Heidelberg, 1991.
Chieri Saito and Atsushi Igarashi. Matching ThisType to subtyping. In Symposium on
Applied Computing (SAC), 2009.
Chieri Saito, Atsushi Igarashi, and Mirko Viroli. Lightweight family polymorphism. Journalof Functional Programming, 18(03), 2007.
Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P Black. Traits:
Composable units of behaviour. In European Conference on Object-Oriented Programming,
2003.
Jan Schwinghammer. Coherence of subsumption for monadic types. Journal of Functional
Programming, 19(02):157, 2008.
Jeremy Siek, Peter Thiemann, and Philip Wadler. Blame and coercion: together again for
the first time. In Conference on Programming Language Design and Implementation, 2015.
Richard Statman. Logical relations and the typed λ-calculus. Information and Control,65(2-3):85–97, 1985.
Rick Statman. A finite model property for intersection types. Electronic Proceedings in
Theoretical Computer Science, 177:1–9, 2015.
W. W. Tait. Intensional interpretations of functionals of finite type i. The Journal ofsymbolic logic, 32(2):198–212, 1967.
Philip Wadler. The expression problem. Java-genericity mailing list, 1998.
Yanlin Wang and Bruno C d S Oliveira. The expression problem, trivially! In Proceedingsof the 15th International Conference on Modularity, 2016.
Yizhou Zhang and Andrew C. Myers. Familia: unifying interfaces, type classes, and family
polymorphism. In International Conference on Object-Oriented Programming, Systems,
Languages, and Applications, 2017.

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

A

22:29

Some Definitions

I Definition 32 (Type translation).
|Nat| = Nat|>| = hi
|A → B| = |A| → |B||A & B| = |A| × |B||{l : A}| = {l : |A|}
I Example 33 (Derivation of other direction of distribution).
A1 <: A1A1 <: A1A2 & A3 <: A2

A1 → A2 & A3 <: A1 → A2

S-arr

A2 & A3 <: A3
S-arr

A1 → A2 & A3 → A1 → A3

S-and

A1 → A2 & A3 <: (A1 → A2 ) & (A1 → A3 )I Example 34 (Derivation of contravariant distribution).
A1 & A3 <: A1
S-andl(A1 → A2 ) & (A3 → A2 ) <: A1 → A2

A2 <: A2

A1 → A2 <: A1 & A3 → A2

S-arr
S-trans(A1 → A2 ) & (A3 → A2 ) <: A1 & A3 → A2

B

Full Type System of NeColus

A <: Bc(Declarative subtyping)
S-trans

S-reflA <: AA2 <: A3
id

A1 <: A2

c1

c1 ◦ c2

A1 <: A3

S-rcd

S-top

c2

A <: >

top

S-arr

A <: B{l : A} <: {l : B}
S-andlB1 <: A1c{l : c}π1A2 <: B2

A1 → A2 <: B1 → B2

c2

c1 → c2

S-and

S-andr

A1 & A2 <: A1

c1

A1 <: A2

A1 & A2 <: A2

π2

c1

A1 <: A2 & A3

A1 <: A3c2

hc1 , c2 i

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

dist→

S-topArr{l : A} & {l : B} <: {l : A & B}

> <: > → >dist{l}top→

S-topRcd> <: {l : >}top{l}ECOOP 2018

22:30The Essence of Nested Composition

Γ`E⇒A

e

(Inference)

T-top

T-lit

T-var

x:A ∈ ΓΓ`>⇒>hi

Γ ` i ⇒ Nat

Γ`x⇒A

i

T-app

x

T-mergeΓ ` E1 ⇒ A1 → A2
e1
Γ ` E2 ⇐ A1
e2

T-annoΓ ` E1 E2 ⇒ A2

Γ`E:A⇒A

Γ`E⇐A

e1 e2

Γ ` E1 ⇒ A1
Γ ` E2 ⇒ A2e2e

Γ ` E1 , , E2 ⇒ A1 & A2

e

T-rcd

Γ ` E ⇒ {l : A}eΓ ` {l = E} ⇒ {l : A}{l = e}Γ ` E.l ⇒ A

e
e.l

e

(Checking)
T-sub

T-abs

Γ, x : A ` E ⇐ B

Γ`E⇒B

e

Γ ` λx. E ⇐ A → B

B <: A

e

Γ`E⇐A

λx. e

c

ce

A∗B

(Disjointness)

D-topL

D-topR

>∗A

A∗>

D-arr

A1 ∗ BA1 → A2 ∗ B1 → B2
D-rcdNeq

A2 ∗ B

A1 & A2 ∗ B

A∗B

l1 6= l2

D-axNatArr{l : A} ∗ {l : B}

{l1 : A} ∗ {l2 : B}Nat ∗ A1 → A2

A ∗ B2A ∗ B1 & B2

D-andLA2 ∗ B2

D-rcdEq

D-andRA ∗ B1

he1 , e2 iT-proj

Γ`E⇒A

Γ`E⇐A

e1
A1 ∗ A2

D-axArrNat

D-axNatRcd

D-axRcdNat

D-axArrRcd

A1 → A2 ∗ Nat

Nat ∗ {l : A}{l : A} ∗ Nat

A1 → A2 ∗ {l : A}

D-axRcdArr{l : A} ∗ A1 → A2
C : (Γ ⇒ A) 7→ (Γ0 ⇒ B)

D

(Context typing I)
CTyp-appL1

C : (Γ ⇒ A) 7→ (Γ0 ⇒ A1 → A2 )
Γ0 ` E2 ⇐ A1e

CTyp-empty1[·] : (Γ ⇒ A) 7→ (Γ ⇒ A)[·]

CTyp-appR1

Γ0 ` E1 ⇒ A1 → A2e0
C : (Γ ⇒ A) 7→ (Γ ⇐ A1 )D

E1 C : (Γ ⇒ A) 7→ (Γ0 ⇒ A2 )eD

C E2 : (Γ ⇒ A) 7→ (Γ0 ⇒ A2 )D
DeCTyp-mergeL1

C : (Γ ⇒ A) 7→ (Γ0 ⇒ A1 )D
0Γ ` E2 ⇒ A2e
A1 ∗ A2

C , , E2 : (Γ ⇒ A) 7→ (Γ0 ⇒ A1 & A2 )hD, ei

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:31

CTyp-mergeR1

Γ0 ` E1 ⇒ A1e
0
C : (Γ ⇒ A) 7→ (Γ ⇒ A2 )A1 ∗ A2

D

E1 , , C : (Γ ⇒ A) 7→ (Γ0 ⇒ A1 & A2 )he, Di

CTyp-rcd1

C : (Γ ⇒ A) 7→ (Γ0 ⇒ B)D0

{l = C} : (Γ ⇒ A) 7→ (Γ ⇒ {l : B})
CTyp-proj1

C : (Γ ⇒ A) 7→ (Γ0 ⇒ {l : B})
0C.l : (Γ ⇒ A) 7→ (Γ ⇒ B)

C : (Γ ⇐ A) 7→ (Γ0 ⇐ B)

{l = D}

CTyp-anno1

C : (Γ ⇒ B) 7→ (Γ0 ⇐ A)

D

D

0

D.l

C : A : (Γ ⇒ B) 7→ (Γ ⇒ A)

D

D(Context typing II)
CTyp-abs2

C : (Γ ⇐ A) 7→ (Γ0 , x : A1 ⇐ A2 )x∈
/ Γ0

CTyp-empty2[·] : (Γ ⇐ A) 7→ (Γ ⇐ A)

C : (Γ ⇐ A) 7→ (Γ0 ⇒ B)

λx. C : (Γ ⇐ A) 7→ (Γ0 ⇐ A1 → A2 )

[·]

D

λx. D

(Context typing III)

CTyp-appL2

CTyp-appR2

C : (Γ ⇐ A) 7→ (Γ0 ⇒ A1 → A2 )
Γ0 ` E2 ⇐ A1
e
C E2 : (Γ ⇐ A) 7→ (Γ0 ⇒ A2 )D

Γ0 ` E1 ⇒ A1 → A2e
C : (Γ ⇐ A) 7→ (Γ0 ⇐ A1 )D

D

E1 C : (Γ ⇐ A) 7→ (Γ0 ⇒ A2 )DeeDCTyp-mergeL2

C : (Γ ⇐ A) 7→ (Γ0 ⇒ A1 )D
Γ0 ` E2 ⇒ A2e
A1 ∗ A2

C , , E2 : (Γ ⇐ A) 7→ (Γ0 ⇒ A1 & A2 )hD, ei

CTyp-mergeR2

Γ0 ` E1 ⇒ A1e
C : (Γ ⇐ A) 7→ (Γ0 ⇒ A2 )A1 ∗ A2

D

E1 , , C : (Γ ⇐ A) 7→ (Γ0 ⇒ A1 & A2 )he, Di

CTyp-rcd2

C : (Γ ⇐ A) 7→ (Γ0 ⇒ B)
0

{l = C} : (Γ ⇐ A) 7→ (Γ ⇒ {l : B})
CTyp-proj2

C : (Γ ⇐ A) 7→ (Γ0 ⇒ {l : B})
0C.l : (Γ ⇐ A) 7→ (Γ ⇒ B)D
{l = D}

CTyp-anno2

D
D.l

C : (Γ ⇐ B) 7→ (Γ0 ⇐ A)
0

C : A : (Γ ⇐ B) 7→ (Γ ⇒ A)

D
D

ECOOP 2018

22:32The Essence of Nested Composition

C : (Γ ⇒ A) 7→ (Γ0 ⇐ B)

D

(Context typing IV)

CTyp-abs1

C : (Γ ⇒ A) 7→ (Γ0 , x : A1 ⇐ A2 )
x∈
/ Γ0

D

λx. C : (Γ ⇒ A) 7→ (Γ0 ⇐ A1 → A2 )L ` A ≺: Bc

(Algorithmic subtyping)

A-and

A-arr

L ` A ≺: B1

L ` A ≺: B2

c1

L ` A ≺: B1 & B2

L, B1 ` A ≺: B2

c2

JLK& ◦ hc1 , c2 i

A-rcd

c

L ` A ≺: B1 → B2

L, {l} ` A ≺: B

c

A-top

L ` A ≺: {l : B}c

L ` A ≺: >A-arrNatc

JLK> ◦ top

A-rcdNat[] ` A ≺: A1

L ` A2 ≺: Nat

c1

A, L ` A1 → A2 ≺: Nat

L ` A ≺: Natc2

c1 → c2

L ` A2 ≺: Natc

L ` A1 & A2 ≺: Nat

id{l : c}A-andN2

L ` A1 ≺: Nat[] ` Nat ≺: Natc{l}, L ` {l : A} ≺: Nat

A-andN1

A-nat

C

λx. D

c ◦ π1

L ` A1 & A2 ≺: Natcc ◦ π2

Full Type System of λc∆`e:τ(Target typing)

typ-unit

typ-littyp-vartyp-absx:τ ∈ ∆
∆ ` hi : hi

∆ ` i : Nat∆, x : τ1 ` e : τ2∆`x:τ

typ-app∆ ` λx. e : τ1 → τ2

typ-pair∆ ` e1 : τ1 → τ2

∆ ` e1 : τ1

∆ ` e2 : τ1

∆ ` e1 e2 : τ2
typ-capp∆ ` he1 , e2 i : τ1 × τ2
typ-rcdc ` τ . τ0∆`e:τ∆ ` ce : τ∆ ` e2 : τ20

typ-proj∆`e:τ

∆ ` e : {l : τ }∆ ` {l = e} : {l : τ }∆ ` e.l : τc ` τ1 . τ2
cotyp-refl(Coercion typing)
cotyp-transc1 ` τ2 . τ3

id ` τ . τ
cotyp-topRcd

top{l} ` hi . {l : hi}c2 ` τ1 . τ2

c1 ◦ c2 ` τ1 . τ3
cotyp-arr

c1 ` τ10 . τ1

cotyp-top

cotyp-topArr

top ` τ . hi

top→ ` hi . hi → hi

c2 ` τ2 . τ20

c1 → c2 ` τ1 → τ2 . τ10 → τ20

cotyp-pairc1 ` τ1 . τ2c2 ` τ1 . τ3

hc1 , c2 i ` τ1 . τ2 × τ3

X. Bi, B. C. d. S. Oliveira and T. Schrijvers

22:33

cotyp-rcd

cotyp-projl

cotyp-projr

π1 ` τ1 × τ2 . τ1

π2 ` τ1 × τ2 . τ2c ` τ1 . τ2
{l : c} ` {l : τ1 } . {l : τ2 }cotyp-distRcd

dist{l} ` {l : τ1 } × {l : τ2 } . {l : τ1 × τ2 }cotyp-distArr

dist→ ` (τ1 → τ2 ) × (τ1 → τ3 ) . τ1 → τ2 × τ3e −→ e 0(Small-step reduction)

step-idstep-transstep-top

id v −→ v(c1 ◦ c2 ) v −→ c1 (c2 v)

top v −→ hi

step-topArr(top→ hi) hi −→ hi

step-arrstep-topRcd

top{l} hi −→ {l = hi}((c1 → c2 ) v1 ) v2 −→ c2 (v1 (c1 v2 ))step-pairstep-distArr

hc1 , c2 i v −→ hc1 v, c2 vi(dist→ hv1 , v2 i) v3 −→ hv1 v3 , v2 v3 istep-distRcd

step-projl

step-projr

dist{l} h{l = v1 }, {l = v2 }i −→ {l = hv1 , v2 i}

π1 hv1 , v2 i −→ v1

π2 hv1 , v2 i −→ v2

step-crcd

step-beta

step-projRcd{l : c} {l = v} −→ {l = c v}

(λx. e) v −→ e[x 7→ v]{l = v}.l −→ v

step-app1

step-app2

step-pair1

step-pair2

e1 e2 −→ e10 e2

v1 e2 −→ v1 e20

he1 , e2 i −→ he10 , e2 i

hv1 , e2 i −→ hv1 , e20 i

e1 −→ e10e2 −→ e20

e1 −→ e10e2 −→ e20

step-cappstep-rcd1

step-rcd2

c e −→ c e 0{l = e} −→ {l = e 0 }e.l −→ e 0 .l

e −→ e 0

e −→ e 0

e −→ e 0

ECOOP 2018