To appear in JFP, 2021. © Cambridge University Press 2021

1

Taming the Merge Operator
XUEJING HUANGJINXU ZHAOBRUNO C. D. S. OLIVEIRAThe University of Hong Kong(e-mail: {xjhuang, jxzhao, bruno}@cs.hku.hk)

Abstract
Calculi with disjoint intersection types support a symmetric merge operator with subtyping. The
merge operator generalizes record concatenation to any type, enabling expressive forms of object
composition, and simple solutions to hard modularity problems. Unfortunately, recent calculi withdisjoint intersection types and the merge operator lack a (direct) operational semantics with expected
properties such as determinism and subject reduction, and only account for terminating programs.
This paper proposes a type-directed operational semantics (TDOS) for calculi with intersection
types and a merge operator. We study two variants of calculi in the literature. The first calculus,
called λi , is a variant of a calculus presented by Oliveira et al. (2016) and closely related to anothercalculus by Dunfield (2014). Although Dunfield proposes a direct small-step semantics for her calculus, her semantics lacks both determinism and subject reduction. Using our TDOS we obtain a directsemantics for λi that has both properties. The second calculus, called λ+i , employs the well-known
subtyping relation of Barendregt, Coppo and Dezani-Ciancaglini (BCD). Therefore, λ+i extends themore basic subtyping relation of λi , and also adds support for record types and nested composition(which enables recursive composition of merged components). To fully obtain determinism, both λiand λ+
i employ a disjointness restriction proposed in the original λi calculus. As an added benefit the
TDOS approach deals with recursion in a straightforward way, unlike previous calculi with disjoint
intersection types where recursion is problematic. We relate the static and dynamic semantics of λito the original version of the calculus and the calculus by Dunfield. Furthermore, for λ+i , we show
a novel formulation of BCD subtyping, which is algorithmic, has a very simple proof of transitivity and allows for the modular addition of distributivity rules (i.e. without affecting other rules ofsubtyping). All results have been fully formalized in the Coq theorem prover.

1 Introduction
The merge operator for intersection types was firstly introduced in the Forsythe language
over 30 years ago (Reynolds, 1988). It has since been studied, refined and used in somelanguage designs by multiple researchers (Pierce, 1991; Castagna et al., 1995; Dunfield,
2014; Oliveira et al., 2016; Alpuim et al., 2017; Bi et al., 2018). At its essence, the merge
operator allows the creation of values that can have multiple types, which are encoded
as intersection types (Pottinger, 1980; Coppo et al., 1981). For example, with the merge
operator, the following program is valid:
let x : Int & Bool = 1 ,, True in (x + 1, not x)
Here the variable x has two types, expressed by the intersection type Int & Bool. The corresponding value for x is built using the merge operator (,,). Later uses of x, such as the2Taming the Merge Operator

expression (x + 1, not x) can use x both as an integer or as a boolean. For this particular
example, the result of executing the expression is the pair (2, False).
The merge operator adds expressive power to calculi with intersection types. Much
work on intersection types has focused on refinement intersections (Freeman and Pfenning,
1991; Davies and Pfenning, 2000; Dunfield and Pfenning, 2003), which only increase theexpressive power of types. In systems with refinement intersections, types can simply beerased during the compilation. However, in those systems, the intersection type Int & Boolis invalid since Int and Bool are not refinements of each other. In other systems, including many OO languages with intersection types – such as Scala (Odersky et al., 2004),
TypeScript (Microsoft, 2012), Flow (Facebook, 2014) or Ceylon (RedHat, 2011) – thetype Int & Bool has no inhabitants and the simple program above is inexpressible. The
merge operator adds expressiveness to terms and allows constructing values that inhabit
the disjoint intersection type Int & Bool, enabling writing programs like the above.
There are various practical applications for the merge operator. As Dunfield (2014)
argues, the merge operator provides “general mechanisms that subsume many different
features”. This is important because a new type system feature often involves extending
the metatheory and implementation, which can be non-trivial. If instead we provide general mechanisms that can encode such features, adding new features will become a loteasier. Dunfield has illustrated this point by showing that multi-field records, overloading
and forms of dynamic typing can all be easily encoded in the presence of the merge operator. Furthermore, when we restrict our attention to the concatenation of records, which themerge operator generalizes, the combination of record concatenation and subtyping paves
the ground for encoding expressive forms of multiple inheritance (Wand, 1989; Rémy,
1995; Palsberg and Zhao, 2004; Zwanenburg, 1997).
More recently, the merge operator has been used in calculi with disjoint intersection
types (Oliveira et al., 2016; Alpuim et al., 2017; Bi et al., 2018). The disjointness restrictionmeans that the two values being merged cannot have conflicts. In such settings, the merge
operator is symmetric, associative and commutative (Bi et al., 2018). Such a variant of themerge operator has been used to encode several non-trivial object-oriented features, whichenable highly dynamic forms of object composition not available in current mainstream
languages such as Scala or Java. These include first-class traits (Bi and Oliveira, 2018),
dynamic mixins (Alpuim et al., 2017), and forms of family polymorphism (Bi et al., 2018).
These features enable widely used and expressive techniques for object composition used
by JavaScript programmers (and programmers in other dynamically typed languages), but
in a completely statically type-safe manner (Bi and Oliveira, 2018; Alpuim et al., 2017).
For example, in the SEDEL language (Bi and Oliveira, 2018), which is based on disjoint
intersection types, we can define and use first-class traits such as:// addId takes a trait as an argument, and returns another trait
addId(base : Trait[Person], idNumber : Int) : Trait[Student] =trait inherits base ⇒ { // dynamically inheriting from an unknown person
def id : Int = idNumber}

Similarly to classes in JavaScript, first-class traits can be passed as arguments, returned
as results, and can be constructed dynamically (at run-time). In the program above
inheritance is encoded as a merge in the core language used by SEDEL.

Journal of Functional Programming

3

Despite over 30 years of research, the semantics of the merge operator has proved tobe quite elusive. In retrospect, this is perhaps not too surprising. It is well-known that,in the closely related area of record calculi, the combination of record concatenation andsubtyping is highly non-trivial (Cardelli and Mitchell, 1991). Since the merge operator
for intersection types generalizes record concatenation and calculi with intersection types
naturally give rise to subtyping, the semantics of the merge operator will clearly not be any
simpler than the semantics of record concatenation with subtyping!
Because of its foundational importance, we would expect a simple and clear directsemantics for calculi with a merge operator. After all, this is what we get for other foundational calculi such as the simply-typed lambda calculus, System F, System Fω , the calculusof constructions, System F<: , Featherweight Java and others. All these calculi have a simple and elegant direct operational semantics, often presented in a small-step style (Wrightand Felleisen, 1994). While for the merge operator there have been efforts in the past to
define direct operational semantics, these efforts have placed severe limitations that disallow many of the previously discussed applications or they lacked important properties.
Reynolds (1991) was the first to look at this problem, but in his calculus the merge operator is severely limited. Castagna et al. (1995) studied another calculus, where only mergesof functions are possible. Pierce (1991) was the first to briefly consider a calculus with anunrestricted merge operator (called glue in his work). He discussed an extension to F∧ witha merge operator but he did not study the dynamic semantics with the extension. Finally,
Dunfield (2014) goes further and presents a direct operational semantics for a calculus
with an unrestricted merge operator. However, the problem is that subject reduction anddeterminism are lost.
Dunfield also presents an alternative way to give the semantics for a calculus with themerge operator indirectly by elaboration to another calculus. This elaboration semantics
is type-safe and offers, for instance, a reasonable implementation strategy, and it is also
employed in more recent work on the merge operator with disjoint intersection types.
However, the elaboration semantics has two major drawbacks. Firstly, reasoning about
the elaboration semantics is more involved: to understand the semantics of programs withthe merge operator we have to understand the translation and semantics of the target calculus. This complicates informal and formal reasoning. Secondly, in calculi defined byelaboration, we want to have coherence (Reynolds, 1991), which is a property that ensuresthat the meaning of a program is not ambiguous. Dunfield’s elaboration semantics is notcoherent. To fix this, calculi with disjoint intersection types have to impose some restrictions. However, even with such restrictions, coherence comes at a high price: the calculi
and proof techniques employed to prove coherence are complex, and can only deal withterminating programs. The latter is a severe limitation in practice!
This paper proposes a type-directed operational semantics (TDOS) for calculi with intersection types and a merge operator. We study two calculi, which are variants of existing
calculi with disjoint intersection types in the literature. The first calculus, called λi , is avariant of a calculus introduced by Oliveira et al. (2016) and it is also closely related toa calculus by Dunfield (2014). The second calculus, called λ+i , employs the well-known
subtyping relation of Barendregt, Coppo and Dezani-Ciancaglini (BCD). BCD subtyping

4Taming the Merge Operator

introduces distributivity of intersections over arrows in the subtyping relation:
OS- DISTA RR(A → B) & (A → C) 6 A → B & C
From the point of view of coercive subtyping, this rule denotes that a merge of two functions can be converted to one function, if their input type is the same. Therefore, λ+i extends
the more basic subtyping relation of λi , and also adds support for record types and nested
composition, subsuming the original λ+i calculus by Bi et al. (2018).
Both calculi address two key difficulties in the dynamic semantics of calculi with amerge operator. The first difficulty is the type-dependent nature of the merge operator.
Using type annotations in the TDOS to guide reduction (and influence operational behavior) addresses this difficulty, and paves the way to prove subject reduction. The second
difficulty is that a fully unrestricted merge operator is inherently ambiguous. For instancethe merge 1, , 2 can evaluate to both 1 and 2. Therefore some restriction is still necessary fora deterministic semantics. To fully obtain determinism, both calculi employ a disjointness
restriction that is used in calculi using disjoint intersection types, and two important new
notions: typed reduction and consistency. Typed reduction is a reduction relation that canfurther reduce values under a certain type. Consistency is an equivalence relation on values, that is key for the determinism result. Determinism in TDOS offers the same guaranteethat coherence offers in an elaboration semantics (both properties ensure that the semantics
is unambiguous), but it is much simpler to prove. Additionally, the TDOS approach deals
with recursion in a straightforward way, unlike λi and subsequent calculi (Bi et al., 2018,2019) where recursion is very problematic for proving coherence.
To further relate λi to the calculi by Dunfield and the original λi by Oliveira et al., weshow two results. Firstly, we show that the type system of λi is complete with respect tothe original calculus. Secondly, the semantics of λi is sound with respect to an extensionof Dunfield’s semantics. The extension is needed because λi uses a slightly more powerfulsubtyping relation, which enables λi to account for merges of functions in a natural way
compared to the original λi . Furthermore, for λ+i , we show a novel formulation of BCD
subtyping, which is algorithmic, has a very simple proof of transitivity and allows for themodular addition of distributivity rules (i.e. without affecting other rules of subtyping). We
also deal with several additional complications in the operational semantics that arise fromthe nested composition. The two calculi and their metatheory have been fully formalized
in the Coq theorem prover.
In summary, the contributions of this paper are:
• The λi and λ+i calculi and their TDOS: We present a TDOS for two calculi
with intersection types and a merge operator. The semantics of both calculi isdeterministic and it has subject reduction.
• Support for non-terminating programs: Our new proof methods can deal withrecursion, unlike the proof methods used in previous calculi with disjoint intersection
types, due to limitations of the current proof approaches for coherence.
• Typed reduction and consistency: We propose the novel notions of typed reduction
and consistency, which are useful to prove determinism and subject reduction.

Journal of Functional Programming

5• Relation with other calculus with intersection types: We relate λi with the calculi
proposed by Dunfield and Oliveira et al.. In short, all programs that are accepted by
the original λi calculus can type-check with our type system, and the semantics of
λi is sound with respect to Dunfield’s semantics.
• Novel algorithmic formulation of BCD subtyping: In our new formulation, thechallenging distributivity rules are added in a modular way, and the transitivity proof
is straightforward.
• Coq formalization: All the results presented in this paper have been formalized in
the Coq theorem prover and they are available from https://github.com/XSnow/
TamingMerge.
This paper is an extended version from a conference paper (Huang and Oliveira, 2020).
The λ+
i calculus and the algorithmic formulation of BCD subtyping are new. Furthermore
λi differs from the calculus in the conference paper (where it is called λi: ) in that itallows the top value to act like a function and employs bidirectional typechecking (Pierce
and Turner, 1998). This change enables typing formulations (for both λi and λ+i ) to bealgorithmic. Moreover, we added an extra section giving more background and motivation.
Roadmap. Section 2 presents the background, motivation and applications for the calculi.
Section 3 gives an overview of the challenges and the design of the TDOS, and introduces the specification of disjointness and consistency. Section 4 and Section 5 present
the type system and operational semantics, respectively. The relation with the original
λi ’s type system, and with Dunfield’s semantics is discussed at the end of each section.
Section 6 introduces a novel algorithmic formulation of BCD subtyping using splittabletypes. Section 7 presents the λ+i calculus and its TDOS, which extends λi with BCD subtyping and records. The design of rules is significantly affected by the new distributive
subtyping rules. Finally, Section 9 discusses the related work and Section 10 concludes.

2 Motivation and Applications of the Merge Operator
A key advantage of the merge operator is its generality and the ability to model various
programming language features. However, there are challenging problems that arise fromthe merge operator. In particular, the combination of the merge operator and subtyping
is problematic. In this section, we revisit those challenges, as well as two applications of
the merge operator: typed first-class traits (Bi and Oliveira, 2018) and nested composition (Bi et al., 2018). For the simple examples illustrating the merge operator in Section
2.1 we assume some convenience features not in our calculi (but supported, for instance,
in SEDEL), including a let construct and some inference of type annotations.
2.1 The Merge Operator, Ambiguity and Subtyping
Ambiguity. As we have discussed in Section 1, a key problem with the merge operator is
ambiguity. The problem stems from the implicit (type-directed) extraction of values frommerges. For instance, for the expression:(1 ,, 2) + 3

6

Taming the Merge Operator

the result is ambiguous (it could be 4 or 5) since we could extract either 1 or 2 from themerge to add to 3. One way to avoid ambiguity is to restrict the types of merged values
to have disjoint types (Oliveira et al., 2016). For instance, Int is disjoint to Bool, so themerge 1 ,, True is accepted. In contrast, 1 ,, 2 is rejected. Disjointness leads to a symmetric,
associative and commutative merge operator (Bi et al., 2018). Other alternatives include
having a biased merge operator, which allows conflicting values. In such a case, when
extracting a value of a certain type from a merge, the merge is searched in a particular order(for instance left-to-right) and the first value of the searched type is returned (Dunfield,2014).
The complications of subtyping. Intersection types naturally induce a subtyping relationship between types. However, subtyping and the subsumption rule enable a program to“forget” about some static information about the types of values. Since the extraction ofvalues from merges is type-directed, such loss of type information can affect the search forthe value. Consider the following program:let x : Bool = True ,, 1 in (2 ,, x) + 3
Note that here we view True ,, 1 as a value. The merge has type Bool & Int, but becauseof subtyping it also has type Bool, the type for x. In a naive operational semantics, for the
program above, we would eventually reach a point where we would need to extract a value
from the merge 2 ,, True ,, 1. This merge has two conflicting integers values.
In a language employing a disjointness restriction the merge 2 ,, True ,, 1 ought to be
rejected, but such a merge only appears at run-time. In the program itself all merges are
disjoint: True ,, 1 is disjoint; and 2 ,, x is also disjoint since x has type Bool. Thus the
program should type-check! One possibility would be to abort the program at run-timewith a disjointness error. However, this would defeat the main purpose of the disjointness
restriction, which is to provide a way to statically prevent ambiguity.
A language offering an asymmetric merge operator would have other issues. Assumingthat the merge operator would be right-biased (giving preference to the values on the rightside), then a programmer may expect that because x has type Bool, (2 ,, x) + 3 should evaluate to 5. However such static reasoning is not synchronized with the run-time behavior,
since x contains the integer 1 and therefore the result of the evaluation would be 4.
From another perspective, we could expect that a valid optimization of the program
above is to replace the expression (2 ,, x) + 3 by 2 + 3, since the static type of x has no integer type. This optimization would be valid (for both symmetric and asymmetric merges) if
the origin of runtime values can be determined statically by looking at the types. However
this is not the case if we simply employ a naive semantics: we statically know that themerge contains an integer 2, but at runtime 1 is extracted instead. The issue is somewhat
similar to the (naive) dynamic scoping semantics for the lambda calculus, where the originof the values for free variables cannot be determined statically when a function is created.
Static (or lexical) scoping solves the problem by using a more sophisticated semantics.
Thus a possible solution for the problem of determining the origin of values in merges
statically in the presence of subtyping is to have a more sophisticated semantics as well.
Record concatenation and subtyping. The problems with the merge operator and subtyping are closely related to the problem of typing record concatenation in the presence ofJournal of Functional Programming

7

subtyping. The latter is well-acknowledged to be a difficult problem in the design of record
calculi (Cardelli and Mitchell, 1991). Foundational work on programming languages in theend of the 80s and early 90s looked at this problem because the combination record concatenation with subtyping was perceived as a way to extend lambda calculi with support
for OOP. In essence, since objects in OOP can be viewed as records, it is natural to look fora language that supports records. Furthermore, record concatenation would provide support for encoding multiple inheritance, which entails composing several objects/records
together. Finally, subtyping is perceived as a key feature of OOP and should be supported
as well. Unfortunately, the problem was found to be quite challenging, for very similar reasons to those that make the interaction of the merge operator with subtyping difficult. Thisshould not come as a surprise, since the merge operator can generalize record concatenation. To see the relationship between the two problems, consider the following variant of
the previous program with records:
let x : {n : Bool} = {m = 1} ,, {n = True} in ({m = 2} ,, x).m + 3
In this variant, x is a record with the static type {n : Bool}, but having an extra field m thatis hidden by subtyping. The record x is then merged with the record {m = 2}. Staticallythis merge seems safe, since the static types of both records do not share record labels incommon. However, when doing the field lookup for m at runtime there would be two fields
m with different values (once again assuming a naive semantics). In essence, we would
have the same problems as with the earlier variant of the program without records.
As we have been hinting, a way to solve this problem is to change the operational semantics to account for types at run-time. We will discuss in depth the technical challenges andaspects of such an approach from Section 3 onwards. But before doing this, we first show
why this is a problem worth solving in the first place, by illustrating interesting applications that can be defined in languages that support a merge operator in the presence ofsubtyping.
2.2 Typed First-Class Traits
To illustrate the interesting applications that a merge operator enables we briefly introduce
typed first-class traits (Bi and Oliveira, 2018) in the SEDEL language. This application is
not new to this paper, but it is useful to revisit it to illustrate the kinds of applications thatare enabled by the merge operator. Typed first-class traits are very much in line with theapplications that OOP researchers had in mind while seeking for calculi integrating record
concatenation and subtyping. In particular, the merge operator naturally enables a form ofmultiple inheritance, as well as a powerful form of dynamic inheritance (where inheritedimplementations can be parameterized).
Traits (Schärli et al., 2003) in Object-Oriented Programming provide a model of multiple
inheritance. Both traits and mixins (Bracha and Cook, 1990; Flatt et al., 1998) encapsulate acollection of related methods to be added to a class. The main difference between traits andmixins has to do with how conflicts are dealt with. Mixins use the order of composition
to determine which implementation to pick in the case of conflicts. Traits require programmers to explicitly resolve the conflicts instead, and reject compositions with conflicts.

8

Taming the Merge Operator

In essence, this difference is closely related to the choice of a symmetric or asymmetric model for the merge operator. Symmetric merges with disjoint intersection types areclosely related to traits because merges with conflicts are rejected, and the composition isassociative and commutative (just like the composition for traits). Asymmetric merges arecloser to mixins, giving preference to one of the implementations in the case of conflicts.
We point the reader to Scharli’s et al. paper for an extensive discussion of the qualities of
the trait model and a comparison with the mixin model.
The SEDEL language (Bi and Oliveira, 2018) has a variant of traits. It essentially adopts
the original trait model, but traits in SEDEL are statically typed and support dynamic
inheritance (unlike Scharli et al. traits). The semantics of SEDEL’s traits is defined via anelaboration to a calculus with disjoint intersection types, where the merge operator is key
to model trait composition. Our examples next are adapted from Bi and Oliveira.
A simple example of a trait in SEDEL is:
type Editor = {on_key : String → String, do_cut : String, show_help :String};type Version = {version : String};
trait editor [self : Editor & Version] ⇒ {on_key(key : String) = "Pressing " ++ key;
do_cut = self.on_key "C-x" ++ " for cutting text";
show_help = "Version: " ++ self.version ++ " Basic usage..."};A trait can be viewed as a function taking a self argument and producing a record. In thisexample, the record, which contains three fields, is encoded as a merge of three single
field records. Because all the fields have distinct field names, the merge is disjoint and thedefinition is accepted. Methods in SEDEL can be dynamically dispatched, as usual in OOP
languages. For instance, in the trait editor, the do_cut method calls the on_key method via
the self reference and it is dynamically dispatched. Moreover, traits in SEDEL have a self
type annotation similar to Scala (Odersky et al., 2004). In this example, the type of the self
reference is the intersection of two record types Editor and Version. Note that show_help
is defined in terms of an undefined version method. Usually, in a statically typed language
like Java, an abstract method is required, making editor an abstract class. Instead, SEDEL
encodes abstract methods via self-types. The requirements stated by the type annotation ofself must be satisfied when later composing editor with other traits, i.e. an implementationof the method version should be provided.
First-class traits and dynamic inheritance. The interesting features in SEDEL are that
traits are first-class and inheritance can be dynamic. The next example shows such features:type Spelling = {check : String};
spell (base : Trait[Editor & Version, Editor]) =trait [self : Editor & Version] inherits base ⇒ {override on_key(key : String) = "Process " ++ key ++ " on spell editor";check = super.on_key "C-c" ++ " for spelling check"};Journal of Functional Programming

9

The spell function takes a trait as an argument and returns a trait as a result. Thus,
since traits can be passed as arguments and returned as results they are first-class (justlike lambda functions in functional programming). The new trait adds a check method
and overrides the on_key method of the base trait. The argument base is a trait of type
Trait[Editor & Version, Editor], where the two types denote trait requirements andfunctionality respectively. As we can see from its definition, trait editor matches that type.
Note that unlike mainstream OOP languages like Java, the inherited trait (which would
correspond to a superclass in Java) is parameterized, thus enabling dynamic inheritance.
In SEDEL the choice of the inherited trait (i.e. the superclass) can happen at run-time,
unlike in languages with static inheritance (such as Java or Scala).
Multiple inheritance. Besides first-class traits and dynamic inheritance, multiple inheritance is also supported. The following trait illustrates multiple inheritance in SEDEL:
trait version ⇒ {version = "0.2"};
trait spell_editor [self : Editor & Version & Spelling ]
inherits spell editor & version ⇒ {};editor1 = new[Editor & Version & Spelling] spell_editor;

The trait spell_editor inherits from both spell editor and version. The latter defines animplementation for the field version. Finally an object editor1 can be created from thetrait spell_editor.
2.3 Nested Composition
The NeColus calculus (Bi et al., 2018) and the SEDEL language support nested composition. With nested composition, it is not only possible to compose top-level traits, but also
to compose any elements inside the top-level trait recursively. Nested composition enables
simple solutions to hard modularity problems like the Expression Problem (Wadler, 1998),
and it is enabled by a powerful form of subtyping where intersections can distribute overother constructs.
The Expression Problem. Here we present the SEDEL style solution of the Expression
Problem, originally described by Bi et al. (2018). The expression problem is a classic challenge about the extensibility of a programming language. In the expression problem, a data
type of expressions is defined, with several cases (literals and additions in the followingcode) associated with some operations (e.g. evaluation). There are two directions to extend
the data type: adding a new case and adding a new operation. In a solution both extensions
should be independently defined, and it should be possible to combine them to close thediamond. In a typical OOP language, class inheritance makes it easy to add a new caseto the data type, while extending in the other direction in a modular and type-safe way
remains hard. To illustrate the SEDEL solution, we start from a simple language with twocases and one operation.
type IEval = { eval : Double };type Lang = { lit : Double → IEval, add : IEval → IEval → IEval };10Taming the Merge Operator

trait implLang ⇒ {lit (x : Double)= { eval = x };add (x : IEval) (y : IEval) = { eval = x.eval + y.eval }} : Lang;

In the above example, two fields lit and add in Lang model the constructors for expressions. Trait implLang defines a concrete evaluation operation over expressions by providing
implementations for lit and add. As observed by Bi et al., traits such as implLang, can beviewed as a family of related implementations in the sense of family polymorphism (Ernst,
2001). In family polymorphism the central idea is that classes can be nested inside otherclasses, to form a family of related classes. In implLang, we can view the trait itself as afamily, and the implementations of the constructors as the implementations of the nested“classes”. The type Lang can be understood as the type of the family.
Adding a new operation print is straightforward via a new trait implPrint, which isdefined in a similar way to implLang.
type IPrint = { print : String };type LangPrint = { lit : Double → IPrint, add : IPrint → IPrint → IPrint };trait implPrint ⇒ {lit (x : Double)= { print = x.toString };add (x : IPrint) (y : IPrint) = {print = "(" ++ x.print ++ " + " ++ y.print ++ ")"}} : LangPrint;

Similarly, a new case for negation can be added independently. The type of the new trait is
the intersection of Lang and a record type for negation. Correspondingly, its implementation
also reuses implLang via trait inheritance.
type LangNeg = Lang & { neg : IEval → IEval };trait implNeg inherits implLang ⇒ {neg (x : IEval) = { eval = 0 - x.eval }} : LangNeg;

It is necessary to extend implPrint for the newly defined case neg before composing them.
trait implExt inherits implNeg & implPrint ⇒ {neg (x : IPrint) = { print= "-" ++ x.print }};The trait combines the missing method with the extension of two dimensions: implNeg and
implPrint. The following code shows how we can use the extended arithmetic language.
type ExtLang = { lit : Double → IEval&IPrint, add : IEval&IPrint →IEval&IPrint → IEval&IPrint, neg : IEval&IPrint → IEval&IPrint };fac = new[ExtLang] implExt;
e = fac.add (fac.neg (fac.lit 2)) (fac.lit 3);
main = e.print ++ " = " ++ e.eval.toString -- "(-2.0 + 3.0) = 1.0";

Journal of Functional Programming

11

BCD subtyping and nested composition. Notably the expression e has type IEval &IPrint allowing both the print and eval methods to be called. This is possible because
nested composition is triggered by the annotation ExtLang for new when creating theobject fac. While the expression implExt has type Trait[LangNeg & LangPrint & { neg: IPrint → IPrint }], the annotation in new forces the resulting object to have type
ExtLang. This is allowed because with BCD-style subtyping (Barendregt et al., 1983) the
following subtyping statement holds:
LangNeg & LangPrint & { neg : IPrint → IPrint } <: ExtLang

In short, in BCD-style subtyping, intersections distribute over other type constructors, likefunctions or records, thus allowing the previous subtyping statement to hold. For instance,
for records the distributivity rule for subtyping is:OS- DIST R CD

{l : A} & {l : B} 6 {l : A & B}
Nested composition gives an operational meaning to such an upcast at runtime by suitably adapting the values of the subtype to the right form to fit the supertype. For a simple
example, consider the merge of two records, each containing a field x of (disjoint) types
Int and String, respectively. Because of the distributivity of intersections over records,
such a merge can be typed as a single record, with a field x of type Int&String:{x = 3},, {x = "Hello"} : {x : Int & String}At runtime, the value {x = 3},, {x = "Hello"} will be converted into {x = 3 ,,"Hello"}, in order for the shape of the value to match up with the shape of the type. Since
traits in SEDEL are in essence records of functions, distributivity can trigger a series ofsuch transformations that reshape the values to match up with the shape of types. Suchtransformations are what we call nested composition, which is essentially reflecting thechanges triggered by distributivity (and other subtyping) rules at runtime. Thus the components that are nested inside the traits being composed are themselves recursively composed,
enabling the creation of objects like e containing implementations for both print and eval.
Encoding source language features. The SEDEL language, used to illustrate the examples in this section, is built on top of the Fi calculus (Alpuim et al., 2017). The Fi calculus
is itself a polymorphic extension of the original version of λi (Oliveira et al., 2016).
In essence, source language constructs, such as traits and extensible records, are elaborated into the more primitive constructs available in Fi . In particular, traits are encodedusing merges of single field records. To model self-references and inheritance, the elaboration into Fi employs ideas from Cook’s denotational semantics of inheritance (Cook andPalsberg, 1989). The details of the elaboration of SEDEL’s source language constructs into
Fi are outside of the scope of this paper, and are given in work by Bi and Oliveira (2018).
A more recent version of SEDEL, employing the same encoding, but targeting the Fi+ calculus instead and enabling distributive subtyping and nested composition, was used by Bi
et al. (2019). We have used such a version to present the examples in Section 2.2.
Although SEDEL itself cannot be fully elaborated to λi and λ+i , because of the absenceof polymorphism, a large subset of it can indeed be directly encoded into λi and λ+i . Inparticular, all the examples that we present in Section 2.2 fit within this (monomorphic)

12

Taming the Merge Operator

subset of SEDEL. In fact, although SEDEL implementations support polymorphic traits,
the encoding of traits presented by Bi and Oliveira (2018) only supports monomorphic
traits for simplicity. Therefore, such an encoding of traits can essentially be directly applied
to encode the examples in Section 2.2 into λ+i . One small point is that the encoding assumes
a letrec construct, which needs to be encoded with fixpoints in λi and λ+i .
In addition to encoding source-level constructs, the type system of SEDEL also performs simple forms of type-inference, allowing source programs to be written with fewer
annotations than those needed in λi and λ+i . During elaboration the type information isused to insert extra type annotations, which are used by the core language.
3 An Overview of the Type-Directed Operational Semantics
While the merge operator has many applications, designing a direct operational semantics for a calculus with the merge operator is not straightforward. This section gives an
overview of the type-directed operational semantics for λi and λ+i . We first introduce
Dunfield (2014)’s untyped semantics to show the behavior of the merge operator. As
Dunfield herself noted, such a semantics has two important problems: non-determinism;and the lack of subject reduction. In this section we illustrate how the TDOS uses type
annotations to guide reduction, solving the problems in Dunfield’s semantics.
3.1 Background: Dunfield’s Non-Deterministic Semantics
Dunfield studied a calculus with unrestricted intersections and unions. The interesting
aspect of her calculus is the merge operator: it takes two terms E1 and E2 of some types
A and B, to create a new term that can behave both as a term of type A and as a term oftype B. She proposed an operational semantics and an indirect elaboration semantics forthe calculus. As Dunfield noted, the operational semantics is nondeterministic and does notpreserve types. Nonetheless, such a semantics plays an important role in Dunfield’s workby giving an over-approximation of the intended behavior of programs using the merge
operator. It is used to justify the elaboration semantics, where programs are compiled intoa language with products and sums, and without intersections and unions. Indeed, intersection types and the merge operator in Dunfield’s calculus are similar to product types andpairs. For example, a program written with pairs that behaves identically to the program
shown in Section 1 is:
let x : (Bool, Int) = (True, 1) in (snd x + 1, not (fst x))
However while for pairs both the introductions and eliminations are explicit, with themerge operator the eliminations (i.e. projections) are implicit and driven by the types of
the terms. Dunfield exploits this similarity in her elaboration semantics. By extending typing judgments, the elaboration transforms merges into pairs, intersections into products
and inserts the missing projections.
Syntax. The top of Figure 1 shows the syntax of Dunfield’s calculus. Types include a top
type Top, function types (A → B) and intersection types (written as A & B). Following theconvention introduced by previous works (Oliveira et al., 2016), → has lower precedence
than &, which means A → B & C is equal to A → (B & C). Most expressions are standard,
except for the merge E1 ,, E2 . The calculus also includes a canonical top value >, and13

Journal of Functional Programming(Syntax of Dunfield’s Calculus)
Types
Expressions
Values

E

A, B
E
V

Top | A → B | A & B
x | > | λ x. E | E1 E2 | fix x. E | E1 ,, E2
x | > | λ x. E | V1 ,, V2

::=
::=
::=

E0

(Operational Semantics of Dunfield’s Calculus)
DS TEP - APPRDS TEP - APPLDS TEP - BETA

E1

E10

E2

E20

E1 E2

E10 E2

V1 E2

V1 E20(λ x. E) V

DS TEP - MERGELDS TEP - FIX

fix x. EE[x 7→ fix x. E]
DS TEP - UNMERGEL

E1 ,, E2

E1

DS TEP - MERGER

E10

E1

E20

E2

E10 ,, E2

E1 ,, E2

E[x 7→ V ]V1 ,, E2

DS TEP - UNMERGERDS TEP - SPLIT

E1 ,, E2

E

E2

V1 ,, E20

E ,, E

Fig. 1. Syntax and non-deterministic small-step semantics of Dunfield’s calculus.
considers variables as values. Note that the original calculus by Dunfield uses a different notation for intersection types (A ∧ B), and supports union types (A ∨ B). For a better
comparison, we adjust the syntax and omit union types in Dunfield’s system. Union types
are not supported by λi , since it is based on the calculus by Oliveira et al. (2016) withdisjoint intersection types, which focus on the merge operator and does not have unions
types. Integrating union types with disjointness is still an open problem, which has notbeen addressed in previous work on disjoint intersection types. Since such a problem isorthogonal to the work in this paper, the calculi presented in this paper do not support
union types either.
Operational semantics. The bottom part of Figure 1 presents the reduction rules. All rules
not involving the merge operator are standard call-by-value reduction rules. The reduction of a merge construct in Dunfield’s calculus is quite flexible: V1 ,, V2 is a value, but
E1 ,, E2 (including values) can step, to its left subexpression (by rule DS TEP - UNMERGEL)
or the right one (by rule DS TEP - UNMERGER). Other values can step further as well, by
rule DS TEP - SPLIT, which allows any expression to split into two.
Problem 1: no subject reduction. The operational semantics does not preserve types.
Since the reduction is oblivious of types, a term can reduce to two terms with potentiallydifferent (and unrelated) types. For instance:
1 ,, True

1

1 ,, True

True

Here the merge of an integer and a boolean is reduced to either the integer (rule DS TEP UNMERGEL ) or the boolean (rule DS TEP - UNMERGER ). In Dunfield’s calculus the term
1 ,, True can have multiple types, including Int or Bool or Int & Bool. Not all types thatcan be assigned to a term lead to type-preserving reductions. For instance, if the term

14Taming the Merge Operator

is given the type Int, then the second reduction above does not preserve the type. Whatis worse, a well-typed expression can reduce to an ill-typed expression by dropping thewrong part:(1 ,, λ x. x + 1) 2

12

Problem 2: non-determinism. Even in type-preserving reductions there can be anotherproblem. Because of the pair of UNMERGE rules (rule DS TEP - UNMERGEL andrule DS TEP - UNMERGER), the choice between a merge always has two options. This meansthat a reduced term can lead to two other terms of the same type, but with different
meanings. For example:
1 ,, 2

1

1 ,, 2

2

There is even a third option to reduce a merge with the split rule (rule DS TEP - SPLIT):
1 ,, 2(1 ,, 2) ,, (1 ,, 2)In other words, the semantics is non-deterministic. Non-determinism is also the root of the
problem with the examples discussed in Section 2.1.
Dunfield’s elaboration semantics, although is type-safe, also suffers from this issue. The
merge 1 ,, 2 can elaborate to 1 or 2 when checked against Int by the typing rules. Her
implementation prioritizes the left part, resulting in a biased merge operator.
3.2 A Type-Driven Semantics for Type Preservation
An essential problem is that the semantics cannot ignore the types if the reduction ismeant to be type-preserving. Dunfield (2014) notes that “For type preservation to hold,the operational semantics would need access to the typing derivation”. To avoid run-time
type-checking, we design a type-driven semantics and use type annotations to guide reduction. Therefore our λi calculus is explicitly typed, unlike Dunfield’s calculus. Nevertheless,
it is easy to design source languages that infer some of the type annotations and insert them
automatically to create valid λi terms as we will see in Section 4.4. We discuss the main
challenges and key ideas of the design of λi next.
Annotations and type-driven reduction. Our operational semantics follows a standard call-by-value small-step reduction and it is closely related to Dunfield’s semantics.
However, type annotations are used to guide reduction. For example, in λi we can write
explicitly annotated expressions for which the following reductions are valid:(1 ,, True) : Int ,→ 1

(1 ,, True) : Bool ,→ True

In contrast, the following reductions are not possible:(1 ,, True) : Bool 6,→ 1(1 ,, True) : Int 6,→ True

Note also that 1 ,, True without any type annotation is a value and does not reduce.
Typed reduction in action. The crucial component in the operational semantics, whichenables the use of type information during reduction, is an auxiliary typed reduction relation v ,→A v0 . This relation is used when we want some value to match a type. Typed
reduction is where type information from annotations in λi “filters” reductions that are

Journal of Functional Programming

15

invalid due to a type mismatch. It takes a value and a type as inputs, and produces a valueof that type as output. Similarly to Dunfield’s operational semantics, this process may
result in further reduction of values, unlike many other languages where values can neverbe further reduced. Typed reduction is used in two places during reduction:
S TEP - ANNOVS TEP - BETA

v ,→A v0

v ,→A v0v : A ,→ v0(λ x. e : A → B) v ,→ (e[x 7→ v0 ]) : B

The first place is in rule S TEP - ANNOV. When reduction meets a value v with a type
annotation A, it uses typed reduction to further reduce v against the type A. To see typed
reduction in action, consider a simple merge of primitive values 1 ,, True ,, ‘c’ with anannotation Int & Char. Using rule S TEP - ANNOV, typed reduction is invoked, resulting in:
1 ,, True ,, ‘c’ ,→Int & Char 1 ,, ‘c’
We can also type-reduce the same value under a similar type but where the two types in
the intersection are interchanged:
1 ,, True ,, ‘c’ ,→Char & Int ‘c’ ,, 1
The two valid reductions illustrate the ability of typed reduction to create a value thatmatches exactly with the shape of the type.
The second place where typed reduction is used is in rule S TEP - BETA. In a function
application, the argument can contain more components than what the function expects.
That is because subtyping is allowed for function inputs. For intersection types, we know
A & B <: A. Thus a function can take an input of type A & B while it expects an A. One concrete example is (λ x. x + 1 : Int → Int) (1 ,, True). The merge term (1 ,, True) provides
an integer 1, while the other component True is useless. Such redundant components are
sometimes even harmful. In the following example, we directly substitute the argument todemonstrate why we need to do typed reduction first.
(λ x. (x ,, False) : Int → Int & Bool) (1 ,, True) ,→ (1 ,, True ,, False) : Int & BoolThe function expects an integer but is applied to (1 ,, True). Direct substitution (as done
usually by beta-reduction) would lead to a merge containing two different booleans: 1 ,,True ,, False. Such an ambiguous term is not well-typed, as we shall see in Section 3.4.
Thus such reduction would not be type-preserving.
To avoid the issue with direct substitution, we choose to drop the boolean before beta
reduction by type-reducing the argument. The input type annotation of the applied function
is used to guide the typed reduction and therefore cannot be omitted in lambda expressions.
With only one boolean, the final result is well-typed.
(λ x. (x ,, False) : Int → Int & Bool) (1 ,, True) ,→ (1 ,, False) : Int & Bool
Note that, even an identity function could change its input value.
(λ x. x : Int → Int) (1 ,, ‘c’) ,→ 1 : Int
That may look strange from the view of the subtyping models used in conventional OOP
languages, where upcasting has no runtime impact. However, in coercive subtyping (Luo,1999), subtyping triggers coercions, and such coercions can have an operational effect and16Taming the Merge Operator

change the underlying value. Previous work on intersection types with the merge operator (Dunfield, 2014; Oliveira et al., 2016; Alpuim et al., 2017; Bi et al., 2018, 2019)
employ an elaboration semantics with coercive subtyping: the elaboration introduces coercions that transform values. For example, a merge is translated into a pair, and the coercion
from Int & Char to Int is a projection on the pair which takes the first component. In our
semantics, typed reduction plays a similar role to coercions, and our model of subtyping isquite close to coercive subtyping. Annotations trigger typed reduction, which plays a rolesimilar to coercions in an elaboration approach.
The examples in this (sub)section have shown some non-trivial aspects of typed reduction, which must decompose values, and possibly drop (or rather hide via subtyping) someof the components and permute other components. The details of the typed reduction
relation will be discussed in Section 5. As we shall see next functions introduce further
complications.
3.3 The Challenges of Functions
Some of the hardest challenges in designing the semantics of λi involve functions. We
discuss them next.
Return types matter. Unlike primitive values, we cannot tell the type of a function by
its form. Although the input type annotation of lambdas helps beta reduction, it is notenough to distinguish among multiple functions in a merge (e.g. (λ x. x + 1) ,, (λ x. True))
without run-time type checking. To be able to select the right function from a merge, in λi ,all functions are annotated with both the input and output types. With such annotations we
can deal with programs like:((λ f . f 1 : (Int → Int) → Int)) ((λ x. x + 1 : Int → Int) ,, (λ x. True : Int → Bool))In this program we have a lambda that takes a function f as an argument and applies it to
1. The lambda is applied to the merge of two functions of types Int → Int and Int → Bool.
We select the wanted function by comparing their type annotations to the target type in
typed reduction. Otherwise runtime type-checking would be necessary to recover the full
type of functions.
Annotation refinement. Typed reduction reduces any value v to another value v0 thathas a supertype of the type of v. Subtyping of intersection types leads to selecting
and dropping components from merges. On the other hand, the subtyping of arrow
types requests for type refinements on lambda expressions. Consider a single function
λ x. x ,, False : Int → Int & Bool to be reduced under type Int & Bool → Int. To let thefunction return an integer when applied to a merge of type Int & Bool, we must change
either the lambda body or the embedded annotation. Since reducing under a lambda body
is not allowed in call-by-value, λi adopts the latter option, and treats the input and output
annotations differently. The input annotation should not be changed as it represents the
expectation of the function and helps to adjust the input value before substitution. The next
example demonstrates that refining the input type annotation could result in ambiguity(having both True and False in one merge), which we prevent using rule S TEP - BETA.

Journal of Functional Programming

,→
,→

17

(λ x. x ,, False : Int → Int & Bool : Int & Bool → Int) (1 ,, True){ wrong step here: not keeping the input annotation in typed reduction }(λ x. x ,, False : Int & Bool → Int) (1 ,, True){ by rule S TEP - BETA }(1 ,, True ,, False) : Int(Does not type-check!)

The output annotation, in contrast, must be replaced by Int, representing a future
reduction to be done after substitution. The output of the application then can be thoughtof as an integer and can be safely merged with another boolean. The next example
illustrates how λi correctly deals with annotation refinements:

,→
,→
,→

((λ x. x ,, False : Int → Int & Bool : Int & Bool → Int) (1 ,, True)) ,, True
{ keep the input annotation and change the output one }((λ x. x ,, False : Int → Int) (1 ,, True)) ,, True
{ by rule S TEP - BETA }(1 ,, False) : Int ,, True
{ by rule S TEP - ANNOV }1 ,, True

This example is similar to the previous one but, additionaly, we merge the expression with
True to demonstrate that the ouput type after beta-reduction, will filter the resulting merge.
Some calculi avoid the problem of function annotation refinement by treating annotatedlambdas as values. For example, the target language of NeColus does not reduce a value
wrapped by a coercion in a function form. In the blame calculus (Wadler and Findler,2009), a value with a cast from an arrow type to another arrow type is still a value.
3.4 Disjoint Intersection Types and Consistency for Determinism
Even if the semantics is type-directed and it rules out reductions that do not preserve types,
it can still be non-deterministic. To solve this problem, we employ the disjointness restriction that is used in calculi with disjoint intersection types (Oliveira et al., 2016) and thenovel notion of consistency. Both disjointness and consistency play a fundamental role in
the proof of determinism.
Disjointness. Two types are disjoint (written as A ∗ B), if any common supertypes that they
have are top-like types (i.e. supertypes of any type; written as eCd).
Definition 3.1 (Disjoint Types). A ∗ B ≡ ∀C if A <: C and B <: C then eCd
If two types are disjoint (e.g. (Int & Char) ∗ Bool), their corresponding values do not overlap (e.g. 1 ,, ‘c’ and True). The only exceptions are top-like types, as they are disjoint withany type (Alpuim et al., 2017). Since every value of a top-like type has the same effect,
typed reduction unifies them to a fixed result. Thus the disjointness check in the following
typing rule guarantees that e1 and e2 can be merged safely, without any ambiguities. For
example, this typing rule does not accept 1 ,, 2 or True ,, 1 ,, False, as two subterms of the

18

Taming the Merge Operator

merge have overlapped types (in this case, the same type Int and Bool, respectively).
T YP - MERGEΓ ` e1 ⇒ A

Γ ` e2 ⇒ B

A∗BΓ ` e1 ,, e2 ⇒ A & B
Note that in this rule, ⇒ denotes the synthesis mode in bidirectional typing. In typing
judgements with such a mode, types are synthesized from the term, rather than checked.
Consistency. Recall the rule DS TEP - SPLIT in Dunfield’s semantics: E E ,, E. It duplicates terms in a merge. Similar things can happen in our typed reduction if the type hasoverlapping parts, which is allowed, for example, in an expression 1 : Int & Int. Note thatin this expression the term 1 can be given type annotation Int & Int since Int <: Int & Int.
During reduction, typed reduction is eventually used to create a value that matches theshape of type Int & Int by duplicating the integer:
1 ,→Int & Int 1 ,, 1Note that the disjointness restriction does not allow sub-expressions in a merge to havethe same type: 1 ,, 1 cannot type-check with rule T YP - MERGE. To retain type preservation,
there is a special typing rule for merges of values, where a novel consistency check is used(written as v1 ≈spec v2 ):T YP - MERGEV· ` v1 ⇒ A· ` v2 ⇒ B

v1 ≈spec v2

Γ ` v1 ,, v2 ⇒ A & B
This rule is not designed to accept more programs written by users. Instead, it takes careof expressions like 1 ,, 1 that may appear at runtime. Mainly, consistency allows values
to have overlapped parts as far as they are syntactically equal. For example, 1 ,, True and
1 ,, ‘c’ are consistent, since the overlapped part Int in both of merges has the same value.
True and ‘c’ are consistent because they are not overlapped at all. But 1 ,, True and 2 are
not consistent, as they have different values for the same type Int. When two values havedisjoint types, they must be consistent. For merges of such values, both rule T YP - MERGEVand rule T YP - MERGE can be applied, and the types always coincide. In λi , consistency isdefined in terms of typed reduction:
Definition 3.2 (Consistency). Two values v1 and v2 are said to be consistent (written
v1 ≈spec v2 ) if, for any type A, the result of typed reduction for the two values is the same.
v1 ≈spec v2 ≡ ∀A if v1 ,→A v01 and v2 ,→A v02 then v01 = v02
Although the specification of consistency is decidable and an equivalent algorithmic definition exists (later defined in Figure 14), an algorithmic definition is not required. In practice,in a programming language implementation, the rule T YP - MERGEV may be omitted, since,
as stated, its main purpose is to ensure that run-time values are type-preserving. On theother hand, after preservation is proved in metatheory, run-time values are guaranteed to
be well-typed and therefore there is no need to employ run-time type checking.
Note that the original λi (Oliveira et al., 2016) is stricter than our variant of λi and forbids any intersection types which are not disjoint. That is to say, the term 1 : Int & Int is
not well-typed because the intersection Int & Int is not disjoint. In the original λi (Oliveira

Journal of Functional Programming

19

et al., 2016) calculus disjointness checking is done by defining type well-formedness andforbidding all intersections of two non-disjoint types. However this approach is moreconservative and less expressive.
The idea of allowing unrestricted intersections, while only having the disjointness
restriction for merges, was first employed in the NeColus calculus (Bi et al., 2018). λi follows such an idea and 1 : Int & Int is well-typed in λi . Allowing unrestricted intersections
adds extra expressive power. For instance, in calculi with polymorphism, unrestrictedintersections can be used to encode bounded quantification (Cardelli and Wegner, 1985),
whereas with disjoint intersections only such an encoding does not work (Bi et al.,2019; Xie et al., 2020). Various authors, including Pierce and Castagna have (informally)observed that some form of bounded quantification can be encoded via (unrestricted)
intersection types (Pierce, 1991; Castagna and Xu, 2011). Xie et al. formalize this encoding precisely (Xie et al., 2020). For further details on this encoding, as well as to why
unrestricted intersections are needed, we refer to the work of Xie et al.
Revisiting the examples with merges and subtyping. Recall the first example presented
in Section 2, rewritten here to use a lambda instead of a let expression:(λ x. (2 ,, x) + 3 : Bool → Int) (True ,, 1)As argued in Section 2, in a naive untyped semantics, examples like the above areproblematic since they can lead to non-disjoint merges appearing at runtime. So, how does
the TDOS approach deal with such an example? Here are the full reduction steps:

,→
,→
,→

(λ x. (2 ,, x) + 3 : Bool → Int) (True ,, 1)((2 ,, True) + 3) : Int
5 : Int
5

by rule S TEP - BETA
reduction for +by rule S TEP - ANNOFirstly, the input value is filtered via the typed reduction against the input type Bool.
Importantly, only the selected part True is substituted in the body of the lambda duringbeta-reduction. Then, the expression (2 ,, True) + 3 evaluates to 5. In the process, + acts
like a lambda with annotation Int → Int → Int. Finally, the return type Int filters the result,which does not change it in this case.
The second example with records, is slightly more involved, but can be dealt with similarly. In the example with records, besides the use of the let expressions, which are notpresent in λi or λ+i , we assume some type-inference that avoids some explicit type annotations. Therefore, to encode such an example in λ+i , we must first introduce an explicit type
annotation. The SEDEL language, in its elaboration process to the Fi core language (which
is similar to λi or λ+i , except for the addition of polymorphism), inserts such annotations
automatically (see also Section 8.3).
We show the full reduction steps, starting from the original example encoded as a
λ+i expression using a lambda instead of a let expression, and with an extra annotation({m : Int}) in Figure 2. In this example, a function that expects a record of Bool takes amerge of two records. Only the one with the expected label and field is selected via typed
reduction. Later, the annotation {m : Int} helps to drop the record with unmatched labels
before projection. Afterwards the reduction is straightforward.

20

Taming the Merge Operator

,→
,→
,→
,→
,→

(λ x. (({m = 2} ,, x) : {m : Int}).m + 3 : {n : Bool} → Int) ({m = 1} ,, {n = True}){ by rule S TEP - BETA and typed reduction}((({m = 2} ,, {n = True}) : {m : Int}).m + 3) : Int{ by rule S TEP - ANNO }({m = 2}.m + 3) : Int{ reduction for record projection }(2 + 3) : Int{ reduction for + }5 : Int{ by rule S TEP - ANNO }5
Fig. 2. Reduction for the record example.

3.5 The Challenges of Distributivity
The λi calculus captures the basic functionality of the merge operator with a simple subtyping relation with intersection types. However, such a simple subtyping relation lacks
distributivity rules that enable, for instance, subtyping statements such as:(A → B) & (C → D) <: A & C → B & D
where the intersections distribute over the function types. Distributivity in a calculus witha merge operator is interesting because it enables nested composition, which essentiallyreflects the distributivity seen at the type level into the term level. Therefore, a merge of
two functions can be treated as a single function where the inputs and outputs of the two
original functions have intersection types.
The λ+
i calculus extends λi with distributivity rules for subtyping and nested composition. The subtyping relation for λ+i is based on the well-known subtyping relation of
Barendregt, Coppo and Dezani-Ciancaglini (BCD) (Barendregt et al., 1983). Adding BCD
style subtyping into the type system of λi enables interesting applications, but it also brings
more challenges.
Splittable arrow types. Without distributivity, if an arrow type is a supertype of an intersection of multiple types, then it must be a supertype of one of those types. Conversely,
when doing typed reduction of a merge under an arrow type, we will obtain a single function (one of the components of the merge) as a result. However, in λ+i , we are now facedwith the following kind of typed reduction due to the change in subtyping:(λ x. x : Int → Int) ,, (λ x. True : Int → Bool) ,, (λ x. ‘c’ : Int → Char),→Int → Int & Char (λ x. x : Int → Int) ,, (λ x. ‘c’ : Int → Char)
Even though we are doing typed reduction under an arrow type, we do not obtain a function
as a result. Instead what we have is a merge of two functions. This is because, with the
distributivity of arrow types, multiple components present in a merge can contribute to thefinal result. For instance, in the reduction above both the first and the last lambdas must bepresent to ensure that the resulting value “behaves” as a function of type Int → Int & Char.

Journal of Functional Programming

21

Parallel application. One consequence of allowing merges to have arrow types is thata beta reduction for applications is not enough, since merges of functions can also be
applied to values. We use a relation called the parallel application to deal with applicationsof merges to another value. Parallel application distributes the input to every lambda in amerge, and beta reduces them in parallel. From the point of view of the small-step semantics, the parallel application process, like typed reduction, is finished in a single step, likethe following example.
(λ x. x + 1 : Int → Int ,, (λ x. True : Int → Bool ,, λ x. ‘c’ : Int → Char)) 2,→ (2 + 1) : Int ,, (True : Bool ,, ‘c’ : Char)
Generalized consistency. In λ+i , a merge of function values, once applied to an argument,
can step to a merge of expressions. In the previous example, for instance, one of the components in the resulting merge is (2 + 1) : Int, which is an expression but not a value.
This raises a challenge to the consistency definition employed in λi , which can only relate
values (but not arbitrary expressions). Therefore we have to extend the definition of consistency in λ+i to include such expressions. Intuitively, two expressions can be safely merged
if their reduction result is the same, like (2 + 1) : Int or 3 ,, (2 + 1). However, there aresome difficulties regarding how to reason about expressions like the latter one. Consider
two non-terminating programs, comparing them may never end. Instead we model consistency with a syntactic definition, which is less powerful in the sense that it does notallow 3 ,, (2 + 1). But such a definition is enough to accept the terms generated by parallel
application, which keeps the syntactic equivalence among the components of merges.
Records. Together with BCD subtyping, single-field records and record types are added
into λ+i . There is a distributivity rule in subtyping for records as well: {l : A} & {l : B} 6
{l : A & B}. A merge of several records can be used as a single record, as long as the records
have the same field name. This is similar to function application where functions in one
merge share one input. In reduction, we treat record projection like function application.
That is to say, the parallel application relation not only applies functions in a merge inparallel but also projects records in a merge at the same time.
({l = True} ,, {l = 2}).l ,→ True ,, 2

4 The λi Calculus: Syntax, Subtyping and Typing
This section presents the type system of λi : a calculus with intersection types and a merge
operator. This calculus is a variant of the original λi calculus (Oliveira et al., 2016) (whichis inspired by Dunfield (2014)’s calculus) with fixpoints and explicitly annotated lambdas
instead of unannotated ones. Explicit annotations are necessary for the type-directed operational semantics of λi to preserve determinism. The TDOS can handle non-terminating
programs, while some calculi using elaboration and coherence proofs (Bi et al., 2018,2019) do not support non-terminating programs. Dunfield (2014)’s calculus supports
recursion, but it is incoherent.

22

Taming the Merge Operator
4.1 Syntax

The syntax of λi is:
Types
Expressions
ValuesContexts
Typing modes

A, B
e
v
Γ
⇔

::=
::=
::=
::=
::=

Int | Top | A → B | A & B
x | i | > | e : A | e1 e2 | λ x. e : A → B | e1 ,, e2 | fix x. e : A
i | > | λ x. e : A → B | v1 ,, v2· | Γ, x : A⇒|⇐

Types. Meta-variables A and B range over types. Two basic types are included: the integer
type Int and the top type Top. Function types A → B and intersection types A & B can beused to construct compound types.
Expressions. Meta-variable e ranges over expressions. Expressions include some standard
constructs: variables (x); integers (i); a canonical top value >; annotated expressions (e : A);and application of a term e1 to term e2 (denoted by e1 e2 ). Lambda abstractions (λ x.e :A → B) must have a type annotation A → B, meaning that the input type is A and the output
type is B. The expression e1 ,, e2 is the merge of expressions e1 and e2 . Finally, fixpoints
fix x. e : A (which also require a type annotation) model recursion.
Values, contexts, and typing modes. Meta-variable v ranges over values. Values include
integers, the top value >, lambda abstractions, and merges of values. Typing context Γ
tracks bound variables (x) with their type A. ⇔ stands for the mode of a bidirectional typing
judgment: ⇒ is the synthesis mode; ⇐ is the checking mode. They differ on whether
the type is an output (inferred) or an input (to be checked). The details of bidirectional
typechecking will be discussed in Section 4.3.
4.2 Subtyping and Disjointness
Subtyping. The subtyping rules are shown at the top of Figure 3. Here we follow theformalization by Davies and Pfenning (2000), except that we generalize rule S- TOP toallow any top-like types to be supertypes of any type. The original subtyping relation is
known to be reflexive and transitive (Davies and Pfenning, 2000). We proved the reflexivity
and transitivity of the extended subtyping relation as well.
Top-like types and arrow types. As suggested by its name, a top-like type is both a supertype and a subtype of Top. Besides Top, top-like types contain intersection types likeTop & Top. In the middle of Figure 3 is its formal definition. Notably, rule TL- ARR allows
arrow types to be top-like when their return types are top-like. This enlargement of top-liketypes is inspired by the following rule in BCD-style subtyping (Barendregt et al., 1983):

Top <: Top → Top

BCD- TOPARR

We will come back to our motivation for allowing such top-like types in Section 4.3.
Disjointness. Section 3.4 presented the specification of disjointness. Such a specification
is a liberal version of the original definition in λi . In our definition A and B can be toplike types, which was forbidden in λi . An equivalent algorithmic definition of disjointness

23

Journal of Functional Programming
A <: B(Subtyping)
S- TOP

S- Z

Int <: Int

S- ANDL 1

S- ANDL 2

eBd

A1 <: A3A2 <: A3

A <: B

A1 & A2 <: A3

A1 & A2 <: A3

S- ANDR

S- ARR

B1 <: A1A2 <: B2

A1 <: A2

A1 → A2 <: B1 → B2

A1 <: A3A1 <: A2 & A3

eAd

(Top-Like Types)
TL- AND

TL- ARR
TL- TOP

eBd

eTopd

eA → Bd

eAd

eBd

eA & Bd

A ∗a B(Algorithmic Disjointness)
D- AND L

D- TOP L

D- TOP R

Top ∗a AA ∗a TopA1 ∗a BD- AND R

A2 ∗a BA ∗a B1

A1 & A2 ∗a B

A ∗a B2

A ∗a B1 & B2
D- ARR A RR

D- INTA RR

D- ARR I NT

Int ∗a A1 → A2

A1 → A2 ∗a Int

A2 ∗a B2
A1 → A2 ∗a B1 → B2

Fig. 3. Subtyping, top-like types, and disjointness of λi .

(A ∗a B) is presented on the bottom of Figure 3, which is the same as the definition in the
NeColus calculus (Bi et al., 2018).
Lemma 4.1 (Disjointness properties). Disjointness satisfies:
1. A ∗ B if and only if A ∗a B.
2. if A ∗ (B1 → C) then A ∗ (B2 → C).
3. if A ∗ B & C then A ∗ B and A ∗ C.
4.3 Bidirectional Typing
We use a bidirectional type system for λi to avoid a general subsumption rule, which causes
ambiguity in the presence of a merge operator. A bidirectional type system has two kindsof typing judgements, each associated with one mode. The checking judgement Γ ` e ⇐ Asays that in the typing environment Γ the expression e can be checked against type A, while
the synthesis judgment Γ ` e ⇒ A infers the type A from Γ and e. Unlike the original typesystem of λi (Figure 5), types have no well-formedness restriction; and expressions like1 : Int & Int are allowed. This generalization is inspired by the NeColus calculus (Bi et al.,24

Taming the Merge Operator

AB(Applicative Distributivity)
AD- ARR

AD- TOPA RR

A→BA→B

Top  Top → TopΓ`e ⇔ A

(Bidirectional Typing)

T YP - TOPΓ ` > ⇒ Top

T YP - ABS

T YP - VAR

T YP - LITΓ ` i ⇒ Int

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

T YP - APPΓ ` e1 ⇒ C
CA→BΓ ` e2 ⇐ A

T YP - MERGEΓ ` e1 ⇒ A

Γ ` e1 e2 ⇒ B

Γ ` e2 ⇒ B

A∗BΓ ` e1 ,, e2 ⇒ A & B

T YP - ANNOT YP - FIXΓ`e ⇐ AΓ, x : A ` e ⇐ A

Γ ` (e : A) ⇒ A

Γ ` fix x. e : A ⇒ A

T YP - MERGEVT YP - SUB· ` v1 ⇒ A· ` v2 ⇒ B

v1 ≈spec v2

Γ ` v1 ,, v2 ⇒ A & BΓ`e ⇒ A

A <: BΓ`e ⇐ B

Fig. 4. Typing of λi .
2018), which is the first to introduce unrestricted intersections to a calculus which supports
disjoint intersection types.
In Figure 4, most typing rules directly follow the bidirectional type system of the original λi , including the merge rule T YP - MERGE, where disjointness is used. When two
expressions have disjoint types, any parts from each of them do not overlap in the types.
Therefore, their merge does not introduce ambiguity. With this restriction, rule T YP MERGE does not accept expressions like 1 ,, 2 or even 1 ,, 1. On the other hand, the novel
rule T YP - MERGEV allows consistent values to be merged regardless of their types. It
accepts 1 ,, 1 while still rejecting 1 ,, 2. The consistency specification used in rule T YP MERGEV is given in Definition 3.1. It is for values only, and values are closed. Therefore
the premises should have an empty context (denoted by ·). As discussed in Section 3.4,
together the two rules support the determinism and type preservation of the TDOS, andrule T YP - MERGEV does not need to be included in an implementation. The type systemwith the remaining rules is algorithmic. The rule T YP - FIX is new and allows fixpoints.
In addition, two rules are revised: rule T YP - ABS and rule T YP - APP. Since lambdas are
now fully annotated in the current system, rule T YP - ABS is changed from checking to synthesis mode. Next, we will discuss how rule T YP - APP is generalized with the applicative
distributivity relation.
Applicative distributivity and rule T YP - APP. The top of Figure 4 shows the applicative
distributivity relation, which relates a type with one of its arrow supertypes. Applicative

Journal of Functional Programming

25

distributivity is used in rule T YP - APP, where a term is expected to play the role of a function. Therefore a term of type Top can be used as if it has type Top → Top, and be applied
to any terms. For example, > 1 is allowed and it evaluates to >.
Top-like types and merges of functions. We can finally come back to the motivation
to allow arrow types in top-like types and depart from Dunfield’s calculus. If no arrow
types are top-like, two arrow types A → B and C → D are never disjoint in terms of
Definition 3.1, as they have a common supertype A & C → Top. Consequently, we cannever create merges with more than one function, which is quite restrictive. For Dunfield
this is not a problem, because she does not have the disjointness restriction. So her calculus
supports merges of any functions (but it is incoherent). In the original λi an ad-hoc solution is proposed, by forcing the matter and employing the syntactic definition of top-liketypes in Figure 3 in disjointness, while keeping the standard rule A <: Top in subtyping.
However this means that top-like function types are not supertypes of Top, which contradicts the intended meaning of a top-like type. In contrast, the approach we take in λi is
to change the rule S- TOP in subtyping. Now Top <: (A & C → Top) is derivable and thus
A & C → Top is genuinely a top-like type. In turn, this makes merges of multiple functions
typeable without losing the intuition behind top-like types.
Checked subsumption. Unlike many calculi where there is a general subsumption rulethat can apply anywhere, λi employs bidirectional typechecking, where subsumption iscontrolled. The subsumption (rule T YP - SUB) is in checking mode only. The checking
mode is explicitly triggered by a type annotation, either via the rule T YP - ANNO, rule T YP ABS or rule T YP - FIX . The annotation rule T YP - ANNO acts as explicit subsumption andassigns supertypes to expressions, provided a suitable type annotation. There is a strong
motivation not to include a general (implicit) subsumption rule in calculi with disjoint
intersection types. With an implicit subsumption rule, disjointness is insufficient to prevent
some ambiguous terms, as shown in the following example.

S UB
M ERGES UB· ` 1 ⇒ Int

Int <: Top· ` 1 ⇒ Top· ` 2 ⇒ Int

Top ∗ Int· ` 1 ,, 2 ⇒ Top & Int

Top & Int <: Int & Int· ` 1 ,, 2 ⇒ Int & Int

Via the typical implicit subsumption, type Top is assigned to integer 1. Then 1 can bemerged with 2 of type Int since their types are disjoint. At that time, the merged term
1 ,, 2 has type Top & Int, which is a subtype of Int & Int. By applying the subsumption
rule again, the ambiguous term 1 ,, 2 finally bypasses the disjointness restriction, having
type Int & Int. However, note that with rule T YP - ANNO we can still type-check the term
(1 : Top) ,, 2, and reducing that term under the type Int can only unambiguously result in
2. The type annotation is key to prevent using the value 1 as an integer.
Typing properties. The bidirectional type-checking system has some properties that areimportant for the type soundness proof presented in Section 5. Firstly, each term has only
one synthesized type. Secondly, any well-typed term has a synthesized type, which is theprincipal type. Thirdly, the type in a checking judgement can be replaced by a supertype.

26

Taming the Merge Operator

Lemma 4.2 (Synthesis uniqueness). If Γ ` e ⇒ A and Γ ` e ⇒ B , then A = B.
Lemma 4.3 (Synthesis principality). If Γ ` e ⇐ A then there exists type B, s.t. Γ ` e ⇒ B
and B <: A.
Lemma 4.4 (Checking subsumption). If Γ ` e ⇐ A and A <: B, then Γ ` e ⇐ B.
4.4 Completeness with Respect to the Original Type System
In this section, we discuss the relationship between the original λi (Oliveira et al., 2016)
and the new variant. To disambiguate between the two calculi we use λi '16 to denotethe original calculus and λi for our variant. We prove that the type system of the newvariant is at least as expressive as the λi '16 calculus1 . The syntax of λi '16 (minus pairs
and product types) is almost the same as λi , except that there are no fixpoints and thelambdas do not have any type annotations. Thus lambdas can only be typed in checked
mode. Figure 5 presents an excerpt of the type system. The type system has a type wellformedness definition and a slightly different disjointness relation compared to our variantof λi . Also note that the rule for the merge of values (rule T YP - MERGEV) is absent because
the disjointness restriction in well-formedness prevents duplicated values.
Some details need to be explained before presenting the completeness theorem. Firstly,
subtyping in our variant of λi is stronger due to top-like types. Secondly, top-like types are
disjoint to any type in our variant, while the disjointness in the original λi '16 is restricted
to types that are not top-like. We extended the bidirectional type system of the original λi'16 with recursion and designed an elaboration from the extended system to λi . We proveda theorem which shows the type system of λi can type check any well-typed terms in λi'16, with type annotations inserted based on the typing derivation:
Theorem 4.1 (Completeness of typing with respect to the extended original λi ). If Γ |=E ⇔ A ,→ e , then Γ ` e ⇔ A.
The result means that the type system of λi '16 (or any type system equivalent to it) canbe used as a surface language where many of the explicit annotations of λi are inferred
automatically. That is to say, the λi '16 calculus can be translated into λi without loss ofexpressivity or flexibility. Moreover, the extension of fixpoints further shows that some
type inference with recursion is feasible.
5 A Type-Directed Operational Semantics for λiThis section introduces the type-directed operational semantics for λi . The operationalsemantics uses type information arising from type annotations to guide the reduction process. In particular, a new relation called typed reduction is used to further reduce values
based on the contextual type information, forcing the value to match the type structure. We
show two important properties for λi : determinism of reduction and type soundness. That
is to say, there is only one way to reduce an expression according to the small-step relation,and the process preserves types and never gets stuck.
1

Note that the original λi includes pairs and product types. In the Coq formalization we have a variant withpairs and product types as well. It has all the previous properties proved in this section. For simplicity andconsistency of presentation, we use the variant without pairs and product types in the paper.

27

Journal of Functional Programming
Γ |= A(Type Well-formedness)
W F - ARRW F - TOPW F - INT

Γ |= TopΓ |= IntW F - AND

Γ |= A

Γ |= B

Γ |= A

Γ |= A → B

Γ |= BA∗B

Γ |= A & B

Γ |= E ⇔ A ,→ e

(Bidirectional Typing)

IBT YP - TOP

IBT YP - LIT

IBT YP - VAR

x:A ∈ ΓΓ |= > ⇒ Top ,→ >

Γ |= i ⇒ Int ,→ i

Γ |= x ⇒ A ,→ x

IBT YP - MERGEIBT YP - APP

Γ |= E1 ⇒ A → B ,→ e1
Γ |= E2 ⇐ A ,→ e2

Γ |= E1 ⇒ A ,→ e1
A∗BΓ |= E2 ⇒ B ,→ e2

Γ |= E1 E2 ⇒ B ,→ e1 e2

Γ |= E1 ,, E2 ⇒ A & B ,→ e1 ,, e2

IBT YP - ANNOIBT YP - FIX

Γ |= A

Γ |= E ⇐ A ,→ e
Γ |= E : A ⇒ A ,→ e : A

Γ |= fix x. E ⇐ A ,→ fix x. e : A

IBT YP - LAM

Γ |= AΓ, x : A |= E ⇐ A ,→ e

IBT YP - SUB

Γ, x : A |= E ⇐ B ,→ e

Γ |= E ⇒ A ,→ e

Γ |= λ x. E ⇐ A → B ,→ (λ x. e : A → B)

A <: B

Γ |= E ⇐ B ,→ eFig. 5. The type system of the original λi (extended with fixpoints). Three rules that relatewith product types are ignored.
v ,→A v0

(Typed Reduction)
TR- ARROW

TR- TOP
TR- LITTR- MERGEVL

A1 <: B1

TR- MERGEVR

A Ordinary

v1 ,, v2 ,→A v01

B2 <: A2

λ x. e : B1 → B2 ,→(A1 →A2 ) λ x. e : B1 → A2

v ,→A >

i ,→Int i
v1 ,→A v01¬eA2 deAd

A Ordinary

v2 ,→A v02

TR- AND

A Ordinary

v1 ,, v2 ,→A v02

v ,→A v1

v ,→B v2

v ,→A & B v1 ,, v2

Fig. 6. Typed reduction of λi .
5.1 Typed Reduction of Values
To account for the type information during reduction, λi uses an auxiliary reduction relation
called typed reduction for reducing values under a certain type. Typed reduction v ,→A v0
reduces the value v under type A, producing a value v0 that has type A. It arises when
given a value v of some type, where A is a supertype of the type of v, and v needs to28Taming the Merge Operator

be converted to a value compatible with the supertype A. Typed reduction ensures thatvalues and types have a strong correspondence. If a value is well-typed, its principal typecan be told directly by looking at its syntactic form. Typed reduction can be viewed as arelation that gives a runtime interpretation to subtyping, and the rules of typed reduction arealigned in a one-by-one correspondence with subtyping. While subtyping states what kindof conversions are valid at the type level, typed reduction gives an operational meaning forsuch conversions on values.
Figure 6 shows the typed reduction relation. Rule TR- TOP expresses the fact that a toplike type is the supertype of any type, which means that any value can be reduced under
it. The top-like type is restricted to be ordinary (Davies and Pfenning, 2000), to avoid
overlapping with the rule TR- AND. Ordinary types are all types that are not intersections:

A Ordinary(Ordinary types)

O- TOPO- INT

O- ARROWTop Ordinary

Int Ordinary

A → B Ordinary

The rule TR- TOP indicates that under such a type, any value reduces to the top value>. Recall that the top-like definition in Figure 3 includes arrow types whose return type
is top-like, thus the rule TR- TOP covers values with such top-like arrow types as well.
Rule TR- LIT expresses that an integer value reduced under the supertype Int is just the
integer value itself. Rule TR- ARROW states that a lambda value λ x. e : A → B, under anon-top-like type C → D, evaluates to λ x. e : A → D if C <: A and B <: D. The restrictionthat C → D is not top-like avoids overlapping with rule TR- TOP. Importantly rule TRARROW changes the return type of lambda abstractions, and keeps the input type, since it
is needed at run-time (by rule S TEP - BETA which is discussed in Section 5.3).
Intersections and merges. In the remaining rules, we first decompose intersections. Then
we only need to consider ordinary types. We take care of the value by going through every
merge, until both the value and type are in a basic form. Rule TR- MERGEVL and rule TRMERGEVR are a pair of rules for reducing merges under an ordinary type. Since the type
is not an intersection, the result contains no merge. Usually, we need to select between theleft part and right part of a merge according to the type. The values of disjoint types do not
overlap on non-top-like types. For example, 1 ,, (λ x. x : Int → Int) ,→Int 1 selects the leftpart. For top-like types, no matter which rule is applied, the reduction result is determinedby the type only, as the rule TR- TOP suggests.
Rule TR- AND is the rule that deals with intersection types. It says that if a value v can be
reduced to v1 under type A, and can be reduced to v2 under type B, then its reduction result
under type A & B is the merge of two results v1 ,, v2 . Note that this rule may duplicate
values. For example 1 ,→Int & Int 1 ,, 1. Such duplication requires special care, since themerge violates disjointness. The specially designed typing rule (rule T YP - MERGEV) uses
the notion of consistency (Definition 3.2) instead of disjointness to type-check a mergeof two values. Note also that such duplication implies that sometimes it is possible touse either rule TR- MERGEVL or rule TR- MERGEVR to reduce a value. For example, 1 ,,

Journal of Functional Programming29

1 ,→Int 1. The consistency restriction in rule T YP - MERGEV ensures that no matter which
rule is applied in such a case, the result is the same.
Example. A larger example to demonstrate how typed reduction works is:(λ x. (x ,, ‘c’) : Int → Int & Char) ,, (λ x. x : Bool → Bool) ,, 1,→Int & (Int→Int) 1 ,, (λ x. (x ,, ‘c’) : Int → Int)
The initial value is the merge of two lambda abstractions and an integer. The target type is
Int & (Int → Int). Because the target type is an intersection, typed reduction first employs
rule TR- AND to decompose the intersection into Int and Int → Int. Under type Int the value
reduces to 1, and under type Int → Int it will reduce to λ x. x ,, ‘c’ : Int → Int. Therefore,
we obtain the merge 1 ,, (λ x. x ,, ‘c’ : Int → Int) with type Int & (Int → Int).
Basic properties of typed reduction. Some properties of typed reduction can be proved
directly by induction on the typed reduction derivation. First, when typed reduction is undera top-like type, the result only depends on the type. Second, typed reduction produces thesame result whenever it is done directly or indirectly. Third, if a well-typed value can be
type-reduced by some type, its synthesized type must be a subtype of that type. The threeproperties are formally stated next:
Lemma 5.1 (Top-like typed reduction). If eAd, v1 ,→A v01 , and v2 ,→A v02 then v01 = v02 .
Lemma 5.2 (Typed reduction transitivity). If v ,→A v1 , and v1 ,→B v2 , then v ,→B v2 .
Lemma 5.3 (Subtyping preservation). If v ,→A v0 and · ` v ⇒ B, then B <: A.
Note that Lemma 5.3 relates typed reduction and subtyping.
5.2 Consistency, Determinism and Type Soundness of Typed Reduction
Consistent values, as specified in Definition 3.2, introduce no ambiguity in typed reduction.
If two consistent values both can reduce under a type, they should produce the same result.
The consistency restriction ensures that duplicated values in a merge type-check, but it
still rejects merges with different values of the same type. A value of a top-like type isconsistent with any other value. It only type-reduces under top-like types, which leads to a
fixed result decided by the type.
Relating disjointness and consistency. Assuming that the synthesized types of two values
are disjoint, from Lemma 5.3, we can conclude that when the two values both reduce undera type, that type must be a common supertype of their principal types, which is known to
be top-like. Furthermore, Lemma 5.1 implies that their reduction results are always thesame under such top-like types, so they are consistent. The above discussion concludes
that values with disjoint types evaluate to the same result under the same type, i.e. they are
consistent. This is captured by the following lemma:
Lemma 5.4 (Consistency of disjoint values). If A ∗ B, · ` v1 ⇒ A, and · ` v2 ⇒ B thenv1 ≈spec v2 .
Determinism of typed reduction. The merge construct makes it hard to design a deterministic operational semantics. Disjointness and consistency restrictions prevent merges

30Taming the Merge Operator

AB(Runtime Subtyping)
RS UB - ARR

RS UB - AND

RS UB - Z

B1 <: A1AA

A1 → A2  B1 → B2

A2  B2

A1  B1RS UB - TOP

A2  B2

A1 & A2  B1 & B2

eAd
Top  A

Fig. 7. Runtime subtyping of λi .

like 1 ,, 2, and bring the possibility to deal with merges based on types. Typed reduction takes a well-typed value, which, if it is a merge, must be consistent (according toLemma 5.4). When the two typed reduction rules for merges (rule TR- MERGEVL andrule TR- MERGEVR) overlap, no matter which one is chosen, either value reduces to thesame result due to consistency. Indeed our typed reduction relation always produces aunique result for any legal combination of the input value and type. This serves as afoundation for the determinism of the operational semantics.
Lemma 5.5 (Determinism of typed reduction). For every well-typed v (that is there issome type B such that · ` v ⇒ B), if v ,→A v1 and v ,→A v2 then v1 = v2 .
Runtime subtyping. While most typed reduction rules produce values of the reduction
type (in synthesis mode), two rules are more relaxed. Rule TR- TOP offers > for any toplike types. Rule TR- ARROW keeps the original input annotation in the reduced lambda:(λ x. x ,, 2 : Char → Char & Int) ,→(Char & Int→Char) λ x. x ,, 2 : Char → Char
Precisely speaking, the synthesized type of the result in typed reduction is a runtime subtype of the reduction type. Defined in Figure 7, runtime subtyping is a restricted form ofsubtyping. Roughly, runtime subtyping only allows subtyping in contravariant positions
except for top-like types.
Runtime subtyping is introduced because we need to find a middle point between
equality and subtyping to describe how typed reduction preserves the reduction type(Lemma 5.7). If A is the reduction type and B is the type of the output value in the typed
reduction relation, we cannot simply say that B = A. But knowing only that B <: A is notenough. It does not even prevent directly using the input value as the result. Runtime subtyping ensures that the reduction result behaves like a term of the reduction type, and it
keeps transitivity as well. Thus after multiple steps of reduction, the ultimate result still
has a runtime subtype in terms of the type of the initial expression. Therefore the preservation property of λi is safely relaxed, to allow the expression type to become more andmore specific during reduction.
Type soundness of typed reduction. Via the transitivity lemma (Lemma 5.2) and thedeterminism lemma (Lemma 5.5), we obtain the following property: any reduction resultsof the given value are consistent.
Lemma 5.6 (Consistency after Typed Reduction). If v is well-typed , and v ,→A v1 , andv ,→B v2 then v1 ≈spec v2 .

Journal of Functional Programming

31

The lemma shows that the reduction result of rule TR- AND is always made of consistentvalues, which is needed in type preservation via the typing rule T YP - MERGEV. Then a(generalized) type preservation lemma on typed reduction can be proved.
Lemma 5.7 (Preservation of typed reduction). If · ` v ⇐ A and v ,→A v0 , then ∃B, · `v0 ⇒ B and B  A.
In general, this lemma shows that typed reduction produces well-typed values: it showsthat if a value is checked by type A and it can be type-reduced by A then the reduced value
is always well-typed, and its synthesized type B is a runtime subtype of A. What is more,
typed reduction is guaranteed to progress for a given value and a type it can be checkedagainst. That is to say, from a well-typed value, we can derive the existence of a typed
reduction judgement and the well-typedness of the reduction result.
Lemma 5.8 (Progress of typed reduction). If · ` v ⇐ A, then ∃v0 , v ,→A v0 .
Fewer checks on typed reduction. In rule TR- ARROW (in Figure 6), the premise A1 <: B1
is redundant for reduction. Since we only care about well-typed terms being reduced, sucha check has already been guaranteed by typing. Therefore an actual implementation could
omit that check. The reason why we keep the premise is that typed reduction plays anotherrole in our metatheory: it allows us to define consistency. Consistency is defined for any(untyped) values, and the extra check there tightens up the definition of consistency. With
the premise, typed reduction directly implies a subtyping relation between the type of the
reduced value and the reduction type. (See Lemma 5.3: If v ,→A v0 , and · ` v ⇒ B, thenB <: A).
One could wonder if this property is unnecessary because it may be derived by typepreservation of reduction. Note that whenever typed reduction is called in a reduction rule,the subtyping relation can be obtained from the typing derivation of the reduced term. For
example, reducing v : A will type-reduce v under A. If v : A is well-typed, then we could in
principle prove that the type of v is a subtype of A. Unfortunately, the above proof is hard
to attain in practice. Because type preservation depends on consistency, and consistency isdefined by typed reduction. Once the subtyping property relies on type preservation, there
is a cyclic dependency between the properties.
5.3 Reduction
The reduction rules are presented in Figure 8. Recall that rule T YP - APP is generalized using
applicative distributivity. Correspondingly, the top value consumes every input it meets
using rule S TEP - TOP. Pierce and Steffen (1997) employ a similar rule in a calculus withhigher-order subtyping. Rule S TEP - BETA and rule S TEP - ANNOV are the two rules relying
on typed reduction judgments. Rule S TEP - BETA says that a lambda value λ x. e : A → B
applied to value v reduces by replacing the bound variable x in e by v0 . Importantly v0
is obtained by type-reducing v under type A. In other words, in rule S TEP - BETA further(typed) reduction may be necessary on the argument depending on its type. This is unlike
many other calculi where values are in a final form and no further reduction is needed
before substitution. The rule S TEP - ANNOV says that an annotated v : A can be reduced tov0 if v type-reduces to v0 under type A.

32

Taming the Merge Operator

e ,→ e0S TEP - TOP> v ,→ >S TEP - APPR

(Reduction)
S TEP - BETAS TEP - ANNOVS TEP - APPL

v ,→A v0

v ,→A v0

e1 ,→ e01

(λ x. e : A → B) v ,→ (e[x 7→ v0 ]) : B

v : A ,→ v0

e1 e2 ,→ e01 e2

S TEP - MERGELS TEP - MERGERS TEP - ANNO

e2 ,→ e02

e1 ,→ e01

e2 ,→ e02

e ,→ e0v1 e2 ,→ v1 e02

e1 ,, e2 ,→ e01 ,, e2

v1 ,, e2 ,→ v1 ,, e02

e : A ,→ e0 : A

S TEP - FIX(fix x. e : A) ,→ (e[x 7→ (fix x. e : A)]) : A

Fig. 8. Call-by-value reduction of λi .
Metatheory of reduction. When designing the operational semantics of λi , we want it tohave two properties: determinism of reduction and type soundness. That is to say, there is
only one way to reduce an expression according to the small-step relation, and the process
preserves types and never gets stuck. Similar lemmas on typed reduction were alreadypresented, which are necessary for proving the following theorems, mainly in cases related
to rule S TEP - ANNOV and rule S TEP - BETA.
Theorem 5.1 (Determinism of ,→). If · ` e ⇐ A, e ,→ e1 , e ,→ e2 , then e1 = e2 .
The preservation theorem states that during reduction, the program is always well-typed,
and the reduced expression can be checked against the original type.
Theorem 5.2 (Type preservation of ,→). If · ` e ⇔ A, and e ,→ e0 then · ` e0 ⇐ A.
This theorem is a corollary of the following lemma:
Lemma 5.9 (Generalized type preservation of ,→). If · ` e ⇔ A, and e ,→ e0 then ∃B,· ` e0 ⇔ B and B  A.
The lemma has a similar structure to Lemma 5.7: the type of the reduced result is a runtime
subtype (Figure 7) of the target type. Note that ⇔ in this and the following lemmas is ameta-variable for typing mode. It means both checking and synthesis mode work for it,
as long as the conclusion and the premise have the same mode. To prove Lemma 5.9, thesubstitution lemma has to be adapted. The substituted term is allowed to have a runtime
subtype of the expected type. The type of the result, accordingly, is a subtype of the initial
type. For example, a lambda of type Int → Int can be used when a term of Int & Char → Int
is expected. It can be viewed as a combination of type narrowing via runtime subtyping
and the conventional substitution lemma.
Lemma 5.10 (Substitution preserves types). For any expression e, if Γ1 , x : B, Γ2 ` e1 ⇔A and Γ2 ` e2 ⇒ B0 , B0  B, then Γ1 , Γ2 ` e1 [x 7→ e2 ] ⇔ A0 and A0  A.
Finally, the progress theorem promises that reduction never gets stuck. Its proof relies on
the progress lemma of typed reduction.

Journal of Functional Programming|i||>|| λ x. e : A → B || fix x. e : A ||e:A|| e1 e2 || e1 ,, e2 |

=
=
=
=
=
=
=

33

i
>
λ x. | e |fix x. | e ||e|| e1 | | e2 || e1 | ,, | e2 |Fig. 9. Type erasure of λi .
Theorem 5.3 (Progress of ,→). If · ` e ⇐ A, then e is a value or ∃e0 , e ,→ e0 .
5.4 Soundness with respect to Dunfield’s Operational Semantics
Dunfield’s non-deterministic operational semantics motivates our TDOS. Here, we show
the soundness of the operational semantics of λi with respect to a slightly extended versionof Dunfield’s semantics. The need for extending Dunfield’s original semantics is mostly
due to the generalization of the rule S- TOP in subtyping. In the conference version of thispaper (Huang and Oliveira, 2020) we also discuss a variant of λi (which uses the original
subtyping) and show that such a variant requires no changes to Dunfield’s semantics.
Dunfield’s original reduction rules are presented in Fig 1. We extend her operationalsemantics with the following two rules.
E

E0(The extension of Dunfield’s calculus)
DS TEP - TOPV>DS TEP - TOPARR>V>

Rule DS TEP - TOPARR states that the value > can be used as a lambda which returns >,suggested by the newly added top-like types for arrow types returning Top. Rule DS TEP TOP states that any value can be reduced to >, corresponding to A <: Top. Dunfield avoids
having a rule DS TEP - TOP by performing a simplifying elaboration step in advance:Γ ` V : Top ,→ >D UNFIELD -T YPING -T

With such a rule, values of type Top are directly translated into >, and do not need any
further reduction in the target language. We do not have such an elaboration step. Instead
we extend the original semantics with the two rules above.
Type erasure. Differently from Dunfield’s calculus, λi uses type annotations in its syntax
to obtain a direct operational semantics. | e | erases annotations in term e. By erasing all
annotations, terms in λi can be converted to terms in Dunfield’s calculus (and also theoriginal λi ). The annotation erasure function is defined in Figure 9. Note that for every
value v in λi , | v | is a value as well.
Soundness. Given Dunfield’s extended semantics, we can show a theorem that each stepin the TDOS of λi corresponds to zero, one, or multiple steps in Dunfield’s semantics.

34

Taming the Merge Operator

Theorem 5.4 (Soundness of ,→ with respect to Dunfield’s semantics). If e ,→ e0 , then| e | ∗ | e0 |.
A necessary auxiliary lemma for this theorem is the soundness of typed reduction.
Lemma 5.11 (Soundness of typed reduction with respect to Dunfield’s semantics). If
v ,→A v0 , then | v | ∗ | v0 |.
This lemma shows that although the type information guides the reduction of values, itdoes not add additional behavior to values. For example, a merge can step to its leftpart (or the right part) with rule TR- MERGEVL (or rule TR- MERGEVR), corresponding
to rule DS TEP - UNMERGEL (or rule DS TEP - UNMERGER). Rule TR- AND can be understood as a combination of splitting (rule DS TEP - SPLIT V V ,, V ) and further reduction
on each component separately.
6 A Modular and Algorithmic Formulation of BCD Subtyping
The formalization of λ+i in Section 7 is an extension of λi . At the type level, the main+
addition of λi over λi is a more powerful subtyping relation based on BCD subtyping (Barendregt et al., 1983). In this section, we first revisit BCD subtyping and propose a
new modular and algorithmic formulation of BCD subtyping. This new algorithmic formulation of BCD subtyping is important for the design of the typed reduction relation for λ+i .
The most interesting feature in BCD subtyping is its distributivity rule between intersection
and function types. However, such a rule introduces complications, and designing soundand complete algorithms is tricky. In particular, in previous work (Bi et al., 2018; Pierce,
1989; Bessai et al., 2016, 2019; Siek, 2019), the distributivity rule leads to non-modular
algorithmic formulations where many standard subtyping rules have to be changed due to
distributivity. Furthermore, the metatheory of BCD subtyping is challenging.
We propose a novel modular and algorithmic BCD formulation. The key idea is to use
the novel notion of splittable types, which are types that can be split into an intersection of
two simpler types. We show basic properties of our formulation, including transitivity andinversion lemmas, and conclude that it is sound and complete with respect to the declarative
BCD subtyping. Of particular interest is our transitivity proof. This proof is remarkably
simple in comparison with other proofs in the literature due to a semantic characterizationof types using splittable and ordinary types (Davies and Pfenning, 2000), which is used as
the inductive argument for transitivity.
6.1 BCD Subtyping
The BCD subtyping relation supports intersection types and allows some forms of distributivity. The original BCD formulation is shown in Figure 10. Most notably BCD subtyping
supports distributivity of intersections over function types using the rule OS- DISTA RR.
This rule says that an intersection of two function types A → B and A → C is a subtype ofa function type A → B & C.
The rule OS- TOPA RR is also interesting: in combination with the transitivity rule, it
essentially allows Top to be a subtype of any function type returning Top (recall also thediscussion in Section 4.2). In fact, the relation Top <: Top → Top is equivalent to Top <:A → Top, since Top → Top is the lower bound of A → Top for any type A. With BCD

35

Journal of Functional Programming
A6B(Original BCD Declarative Subtyping)OS- TRANS

OS- REFL

A6B

A6A

A6C

OS- ARR

B6A

B6C

OS- TOP

OS- TOPA RR

A 6 Top

Top 6 Top → Top

OS- AND

C6D

A→C6B→D

A6B

A6C

A6B&C

OS- ANDL

OS- ANDR

A&B6A

A&B6B

OS- DISTA RR(A → B) & (A → C) 6 A → B & C
Fig. 10. Declarative BCD subtyping.
subtyping, we can further justify the property Top <: A → Top by the distributivity rule
(extended to multiple components):(A → B1 ) & (A → B2 ) & ... & (A → Bn ) 6 A → B1 & B2 & ... & Bn
The Top type is commonly treated as an intersection of zero types. Therefore, when n = 0,
the above subtyping judgment becomes Top <: A → Top. On the other hand, from thecoercive subtyping point of view, a simple coercion that validates the relation can be aconstant function that returns λ x. > : A → Top.
The reflexivity and transitivity rules are common elements for declarative systems. In
this particular system, the transitivity rule is hard to eliminate, mainly due to the existenceof rule OS- DISTA RR.
6.2 A Simple and Modular Formulation of BCD with Splittable Types
In order to obtain an algorithm for the BCD subtyping, the transitivity rule must be eliminated. As a step towards transitivity elimination, we treat any type A that is equivalent toan intersection type directly as an equivalent intersection type B & C. If such treatment ispossible, we call A splittable; otherwise A is ordinary.
Ordinary types. Ordinary types (Davies and Pfenning, 2000) have been used in the past
to define algorithmic formulations of subtyping with intersection types (but without distributivity). At the top of Figure 11 we present the definition of ordinary types for ourformulation. Traditionally an ordinary type is any type that is not an intersection of twoother types. However, in this part of the paper, this distinction is more fine-grained, sincesome function types may not be ordinary. For a function type to be ordinary its output typemust be ordinary as well.
Splittable types. The splittable relation, also shown in Figure 11, can be viewed as taking
an input type A, and returning two types B and C, such that A is equivalent to B & C,
i.e. A <: B & C ∧ B & C <: A. Rule S P - AND splits an intersection type directly. Rule S P ARROW splits a function type when its return type is splittable. The reasoning for rule S P ARROW is that both A → B & C <: (A → B) & (A → C) and (A → B) & (A → C) <: A →36

Taming the Merge Operator

A Ordinary+(Ordinary Types)
O- BCD - ARROWO- BCD - TOP

O- BCD - INT

Top Ordinary+

Int Ordinary+

BAC

B Ordinary+
A → B Ordinary+(Splittable Types)
S P - ARROWS P - ANDCBD

AA&BB

A→CA→BA→D

A <: B(Modular BCD Subtyping)S- BCD - TOP

S- BCD - INT

S- BCD - ARR

B Ordinary+

Int <: Int

D Ordinary+eBd

B <: A

C <: D

A → C <: B → D

A <: BS- BCD - ANDR

S- BCD - ANDL

C Ordinary+

C Ordinary+

A <: CA & B <: C

B <: CA & B <: C

S- BCD - AND

BDC

A <: BA <: CA <: D

Fig. 11. Algorithmic and modular subtyping.
B & C are derivable in declarative BCD subtyping. The following lemma provides somejustification for type splitting. It is proven by a routine induction on the splittable premise.
Lemma 6.1 (Splittable Subtypes). If B1  B  B2 and A 6 B1 and A 6 B2 , then A 6 B.
Three important properties related to ordinary and splittable types are:Lemma 6.2 (Ordinary types do not split). For any ordinary type A, A is not splittable.
Lemma 6.3 (Types are ordinary or splittable). For any type A, either A is ordinary or A is
splittable, and it is decidable.
Lemma 6.4 (Splittable determinism). For any splittable type A, if B1  A  C1 and B2 A  C2 , then B1 = B2 and C1 = C2 .

Algorithmic BCD subtyping. By splitting a type into (nested) intersections of ordinary
types, the distributivity rule in BCD subtyping is no longer problematic. In essence, wenormalize the function type produced by distributivity to an equivalent intersection type.
Our new formulation of the subtyping relation A <: B is shown at the bottom of
Figure 11. The main idea with this formulation is that we always split B if possible. In
such a case, rule S- BCD - AND is applied, which works in a similar way to rule S- ANDRJournal of Functional Programming

37

when D is already an intersection type, such as D1 & D2 . The most interesting case iswhen D is a splittable function type. For example, D := D1 → (D21 & D22 ), and D can be
split into D1 → D21 and D1 → D22 . Therefore, the premises of A <: D are A <: D1 → D21
and A <: D1 → D22 , or equivalently, A <: (D1 → D21 ) & (D1 → D22 ), which can conclude
A <: D with a combination of rule OS- TRANS and rule OS- DISTA RR in the declarative
BCD subtyping. In fact, the split of two types already takes rule OS- DISTA RR into consideration implicitly, while rule S- BCD - AND combines rule OS- TRANS and rule OS- AND.
All the other rules are straightforward, because we already rule out the possibility that B
is splittable. They look almost identical to standard subtyping rules found in the literature,modulo the additional ordinary-type conditions marked in gray.
Top-like types. Top-like types are the same as defined in Figure 3. Rule S- BCD - TOP saysthat a top-like type is a supertype of any type, which is equivalent to the declarative
rule OS- TOP and rule OS- TOPA RR. Although the supertype in rule OS- TOPA RR looks
different than that of rule TL- ARR, the equivalence is supported by the transitivity rule.
For example, Int → Top and Int → (Top → Top) are supertypes (and also subtypes) ofTop. The following property generalizes rule OS- TOP in the declarative BCD subtyping,and it shows the soundness of the definition of top-like types.
Lemma 6.5 (S- BCD - TOP in declarative BCD). If eBd, then A 6 B.
Modularity. A more declarative (and modular) formulation of subtyping is to omit eachordinary-type condition in a gray background in Figure 11. Note that here we employ theterm “modularity” to mean that existing subtyping rules do not need to be changed becauseof a new feature (in this case distributivity).
Our first observation is that omitting the ordinary-type conditions does not change
expressiveness.
Lemma 6.6 (Modular S- BCD - TOP). If eBd, then A <: B.
Lemma 6.7 (Modular S- BCD - ARR). If B <: A, C <: D, then A → C <: B → D.
Lemma 6.8 (Modular S- BCD - ANDL). If A <: C, then A & B <: C.
Lemma 6.9 (Modular S- BCD - ANDR). If B <: C, then A & B <: C.
With these lemmas, the two formulations (with and without ordinary-type conditions)are proved to be sound and complete with respect to each other. Thus, compared to thesubtyping relation in Figure 3 (which is not BCD), the modular BCD subtyping relation
only replaces rule S- ANDR by rule S- BCD - AND to enable BCD distributivity. The new
subtyping rules generalize the previous ones.
It is possible to have an equivalent alternative approach for adding BCD distributivity(rule S- BCD - AND) without modifying the existing rules. One just needs to keep the oldrule S- ANDR and add rule S- BCD - AND - ALT:
S- BCD - AND - ALT
S- ANDR

A1 <: A2A1 <: A3A1 <: A2 & A3

BECA <: D → B
A <: D → C
A <: D → E

38Taming the Merge Operator

Additionally, top-like types are handled by rule S- BCD - TOP using the top-like relation(eAd). An alternative to that rule is to use the following two rules:
S- BCD - TOP - ALT- ARR
S- BCD - TOP - ALT

Top <: C

A <: TopA <: B → C

The first rule is just the standard rule for top types, while the second rule is a special rule
which deals with top-like function types.
Both alternative approaches replace one rule in our modular subtyping relation by two,
while keeping the expressiveness of subtyping unchanged. Rule S- BCD - AND and rule SBCD - TOP in our modular BCD subtyping are generalizations of the designs that would use
2 rules instead, which is why we choose them to be in our system.
It is also worth mentioning that our algorithmic relation keeps the simple judgment
form A <: B, thus the system is easier to extend with orthogonal features, which havebeen presented with a subtyping relation of that form. Some BCD subtyping formulations
require a different form to the subtyping relation (Bi et al., 2018; Pierce, 1989; Bessai
et al., 2016, 2019).
6.3 Metatheory of Modular BCD
A benefit of our new formulation of BCD subtyping is that the metatheory is remarkably simple. The metatheory of BCD subtyping has been a notoriously difficult topic ofresearch.
Inversion lemmas. Given that our algorithmic relations are not entirely syntax-directed,
several inversion lemmas indicate that the algorithm and the declarative system behave
similarly.
Lemma 6.10 (Inversion on left split). Given B Ordinary+ , if A <: B and A1  A  A2 thenA1 <: B or A2 <: B.
Lemma 6.11 (Inversion on right split). If A <: B and B1  B  B2 then A <: B1 and A <:B2 .
Both lemmas are easily proven by induction on the subtyping premises.
Transitivity. Since the transitivity rule is eliminated in algorithmic systems, we need toshow that the transitivity lemma holds. This property is critical but difficult for any BCD
formulation without the transitivity axiom built-in.
Lemma 6.12 (Transitivity of modular BCD). If A <: B and B <: C then A <: C.
To prove the transitivity lemma, one might try at first to proceed by induction on B.
However, that does not succeed, since our algorithm is not entirely syntax-directed. In
particular, the behavior of the subtyping algorithm is determined by whether the type on
the right is ordinary or splittable (but not simply the syntax form of the type). For example,
in the case where A <: B is derived by rule S- BCD - AND, B can be split into two parts
B1  B  B2 , yet B1 and B2 cannot be applied to the induction hypothesis, simply because
they may not be components of type B. On the other hand, assuming one does induction

39

Journal of Functional Programming`& A(Proper Types)
RTY- ORD F UN
RTY- INT

RTY- TOP`& Int`& TopB Ordinary+

`& A

`& B

`& A → B

RTY- SPLIT

BAC

`& B

`& C

`& A

Fig. 12. Proper types.
on the two subtyping derivations, it is a tricky case when A <: B is derived by rule S- BCD AND and B <: C is derived by rule S- BCD - ARR . The former splits type B while the latterdecomposes it as a function type, and they do not match.
To overcome this problem we would like to treat any splittable type similarly to anintersection type. Therefore, we need a proper characterization of the type structure, sothat the induction hypothesis on splittable types is always as desired. The relation definedin Figure 12 defines the so-called proper types. Proper types act as an alternative inductive
definition for types, distinguishing types based on whether they are ordinary or splittable.
The following lemma shows that the definition is general: any type is a proper type.
Lemma 6.13 (Types are proper types). For any type A, `& A.
With the new definition for types, we are ready to prove the transitivity lemma. Induction
is performed on the relation `& B which is obtained easily on type B through Lemma 6.13.
The induction then breaks into several cases:• Int and Top are easy base cases.
• When B is a function type constructed by rule RTY- ORD F UN, a nested induction on
the premise B <: C gives three sub-cases.
– Sub-cases rule S- BCD - TOP and rule S- BCD - AND are easy to prove by induction
hypothesis.
– Sub-case rule S- BCD - ARR is then able to finish by another nested induction on
the other premise A <: B.
• The last case is when B is a splittable type (B1  B  B2 ), where we know that A <:B1 and A <: B2 by Lemma 6.11. Let us do induction on `& C.
– If C is an ordinary type, by Lemma 6.10, either B1 <: C or B2 <: C holds. In bothcases, applying the induction hypothesis of B finishes the proof.
– Otherwise, assuming C1  C  C2 , we apply Lemma 6.11 to B <: C and get B <:C1 and B <: C2 . Via the induction hypothesis of C we can obtain A <: C1 andA <: C2 and reach the goal by rule S- BCD - AND.
Equivalence to declarative BCD. Thanks to the simple judgment form used in ouralgorithm, the soundness and completeness theorems are stated directly as follows.

40

Taming the Merge Operator

Theorem 6.1 (Soundness of modular BCD). If A <: B then A 6 B.
The soundness theorem only relies on Lemma 6.1 and Lemma 6.5.
The completeness theorem is also easy to show with the help of transitivity(Lemma 6.12), by induction on the premise.
Theorem 6.2 (Completeness of modular BCD). If A 6 B then A <: B.
To sum up, our novel formulation of BCD subtyping adds the function distributivity
feature in a modular way, and the metatheory is straightforward to establish with the notionof proper types.
7 The Nested Composition Calculus: Syntax, Subtyping and Typing
In this section, we will introduce the λ+i calculus, which is essentially a TDOS variantof the calculus with the same name introduced by Bi et al. (2018). In the original λ+i
hasrecordtypes
andsupports
recordcalculus the semantics is defined by elaboration. λ+iconcatenation via the merge operator. While λ+i is quite similar to the λi calculus, BCD
subtyping empowers λ+i so that a merge of functions (or records) can act as a function (ora record). We will see how this behavior leads to changes in the typing and reduction rules.
7.1 Syntax and Typing
The syntax of λ+
i is:
Type
Expr
Value
Pre-value
Context
Values and labels

A, B
e

::=
::=

v
u
Γ
vl

::=
::=
::=
::=

Int | Top | A → B | A & B | {l : A}x | i | > | e : A | e1 e2 | λ x.e : A → B | e1 ,, e2 | fix x. e : A| {l = e} | e.li | > | λ x.e : A → B | v1 ,, v2 | {l = v}
v | e : A | u1 ,, u2 | {l = u}
· | Γ, x : A
v | {l}Records and record types. The addition of records affects definitions at both the term
and type level. {l = e} stands for a single-field record whose label is l and its field is e.
Projection (e.l) selects the field(s) from e with label l. In a record type {l : A}, A is the typeof the field. As discussed in Section 2, records can be concatenated by the merge operator.
A merge of single-field records can be thought of as a multi-field record, and therefore canbe used, for example, to model objects. Finally, a new syntactic category vl is defined tounify values and labels for reduction.
Splittable types and subtyping. Figure 13 shows the extension of ordinary types, splittable types, top-like types, and the modular BCD subtyping to record types. The original
definitions can be found in Figure 11, discussed in Section 6. For each relation, a rule forrecord types is added in a modular way. Distributivity of intersection over record types is
supported via rule S- BCD - AND. The definition of splittable types is extended with a newrule S P - RCD, which states that a record type is splittable if the type of its field is splittable.
Disjointness. The disjointness definition, presented on the top of Figure 14, extends λi ’s
definition in Figure 3. It might be a bit surprising that, except for the new record related
rules, the remaining rules are the same as λi ’s disjointness definition. The two systems

41

Journal of Functional Programming
A Ordinary(Ordinary Types)

O- BCD - RCD

BAC

B Ordinary+{l : B} OrdinaryeAd

S P - RCD

CBD

+

(Top-like Types)(Splittable Types){l : C}  {l : B}  {l : D}
A <: BTL- RCDeBde{l : B}d(Modular BCD Subtyping)S- BCD - RCD

D Ordinary+
C <: D{l : C} <: {l : D}

Fig. 13. Rules extending subtyping in Figure 11 with records.

both respect the specification of disjointness (Definition 3.1), from which we know that if
type A is not disjoint with type B, then it is not disjoint to any subtypes of B. Therefore,
since types in λ+i can have more supertypes, its disjointness definition is expected to bestricter than λi . However, in λi , for arrow types, disjointness only cares about output types.
In other words, the set of all output types in an intersection of arrow types decides theset of its disjoint types. For (A → B) & (A → C), if a type is disjoint to it, the type cannot
contain B or C in the return type of any its components. The same criterion applies to types
disjoint from (A → B & C). Therefore, for (A → B) & (A → C), the additional supertype
A → B & C introduced by the distributivity rule in BCD subtyping, brings no extra nondisjoint type to it. Thus the disjointness definition does not change. What is more, theextended definition also has the following properties:
Lemma 7.1 (Disjointness properties). Disjointness satisfies:
1. A ∗ B if and only if A ∗a B.
2. if A ∗ (B1 → C) then A ∗ (B2 → C).
3. if A ∗ B & C then A ∗ B and A ∗ C.
Pre-values and consistency. As shown in Section 3.5, merges like e : A ,, e : A, could be
produced during reduction, since merged functions both take the input. To type check suchmerges, in λ+i , we use pre-values to denote a sort of terms including values, annotatedterms, and merges composed by them, and generalize consistency to pre-values. A prevalue’s type, if it is not a merge, can be told directly from its form without analyzing its
structure. The principal type of a term is the most specific one among all of its types,
i.e. it is the subtype of every other type of the term. The middle of Figure 14 shows thesyntax-directed definition of principal types for pre-values. It is proved that for a well-typed
pre-value with type A, its principal type is A.
Lemma 7.2 (Principal types). For any pre-value u,
1. if u : A and · ` u ⇒ B, then A = B.
2. if · ` u ⇒ A then u : A.

42

Taming the Merge Operator

A ∗a B(Algorithmic Disjointness (Extended with Records))

D- RCD E Q

D- RCD N EQ

A ∗a Bl1 6= l2

{l : A} ∗a {l : B}

{l1 : A} ∗a {l2 : B}

D- INT R CD

D- RCD I NT

Int ∗a {l : A}{l : A} ∗a Int

D- ARR R CD

D- RCDA RR

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

u:A

(Principal Type of Pre-Values)
PT- RCD

PT- TOP

PT- INT

PT- LAM> : Topi : Int(λ x. e : A → B) : (A → B)

u:A
{l = u} : {l : A}

PT- MERGE

u1 : A

PT- ANNO

u2 : B(u1 ,, u2 ) : (A & B)

(e : A) : A

u1 ≈ u2(Consistency)
C- RCD

C- LIT

C- ABS

C- ANNOi≈iλ x. e : A → B1 ≈ λ x. e : A → B2

e:A≈e:B

C- DISJOINT

u1 : A

C- MERGEL

u2 : Bu1 ≈ u2A ∗a Bu1 ≈ uu1 ≈ u2{l = u1 } ≈ {l = u2 }C- MERGER

u2 ≈ uu1 ,, u2 ≈ u

u ≈ u1u ≈ u2u ≈ u1 ,, u2Fig. 14. Extension of disjointness in Figure 3, principal types and consistency in λ+i .
Recall that the intuition of consistency is to allow two terms in a merge if they have disjoint
types or their overlapped parts are equal. In λi , only values can be consistent, and the specification of consistency relies on typed reduction, which is hard to extend to expressions. To
extend consistency to pre-values, we now use an inductive relation to define consistency,
where principal types are used to simplify the definition. Consistency is showed on thebottom of Figure 14. Notably, for values, the definition is sound and complete with respect
to the specification (Definition 3.2).
Lemma 7.3 (Soundness and completeness of consistency definition). For all well-typed
value v1 and v2 , v1 ≈ v2 if and only if v1 ≈spec v2 .
Typing and applicative distributivity. Figure 15 presents the extension of typing andapplicative distributivity. The initial definitions can be found in Figure 4. Applicative
distributivity is extended in two dimensions. One is to treat record types as one of theapplicative forms. Rule AD- RCD is the base case for record types, given that the shape
can already accept label projections. Top can behave like different types depending on the43

Journal of Functional Programming(Applicative Distributivity (λ+i Extension))AB

AD- AND R CD

AD- RCD

AD- TOP R CD

{l : A}  {l : A}Top  {l : Top}A  {l : A2 }A & B  {l : A2 & B2 }AD- ANDA RR

A  A1 → A2

B  {l : B2 }B  B1 → B2

A & B  A1 & B1 → A2 & B2

(Bidirectional Typing (λ+i Extension))Γ`e ⇔ AT YP - BCD - MERGEVT YP - BCD - RCDΓ`e ⇒ AΓ ` {l = e} ⇒ {l : A}T YP - BCD - PROJΓ`e ⇒ AA  {l : C}

Γ ` e.l ⇒ C· ` u1 ⇒ A· ` u2 ⇒ B
u1 ≈ u2Γ ` u1 ,, u2 ⇒ A & B

Fig. 15. Typing and applicative distributivity of λ+i (extends Figure 4).

context: 1) {l : Top} when a record type is required, or 2) Top → Top when a function typeis required. The other dimension is about distributivity over intersections, where rule ADANDA RR now supports intersection of function (-like) types, thanks to the distributivity
rule of BCD subtyping. Rule AD- AND R CD combines both dimensions and enables theintersection of record (-like) types.
Typing relies on applicative distributivity. Due to the distributivity and top-like types,
in rule T YP - APP and rule T YP - BCD - PROJ, where a term is expected to play the role of afunction or record, its inferred type is allowed to be Top, or (in λ+i ) an intersection type.
Assuming that a term e1 of type (Int → Int) & (Bool → Bool) is applied to term e2 , via thisrelation, we can derive that e2 should be checked against type Int & Bool. Besides this, two
new rules are added for records and record projection: rule T YP - BCD - RCD and rule T YP BCD - PROJ . Moreover, rule T YP - BCD - MERGEV is generalized from values to pre-values.
Thus, merges like e : A ,, e : A are well-typed in λ+i .
7.2 Operational Semantics
Typed reduction. Compared with λi , the new typed reduction has one more rule forrecords, and two rules that change, as shown in Figure 16. An additional condition is added
in rule TR- BCD - ARROW to make sure that it only applies to ordinary arrow types. The condition is unnecessary in λi because every arrow type there is ordinary. Rule TR- BCD - RCD
mimics the arrow rule. Rule TR- BCD - AND works on splittable types, so now it needs totake care of more types than just intersections. Although we choose to merge the two
results of the split types, there are some other alternative options. One possible design isto construct a lambda from the results. Therefore, we could prevent merges from being the
inhabitants of arrow types. However, manipulating the lambda body breaks the transitivity
of typed reduction, which plays an important role in our metatheory.

44

Taming the Merge Operator

v ,→A v0

(Typed Reduction (λ+i Extension))TR- BCD - ARROW

TR- BCD - RCD

A Ordinary

+

¬eAd

v ,→A v0{l = v} ,→{l:A} {l = v }

0

¬eDd

D Ordinary+
C <: AB <: D

λ x. e : A → B ,→(C→D) λ x. e : A → D

TR- BCD - AND

BACv ,→B v1

v ,→C v2

v ,→A v1 ,, v2

Fig. 16. Typed reduction of λ+i (extends Figure 6).
Reduction. In the reduction rules of λ+i , presented in Figure 17, rule S TEP - BCD - PAPP
replaces the original beta-reduction rule and rule S TEP - TOP. Rule S TEP - BCD - RCD,
rule S TEP - BCD - PROJ, and rule S TEP - BCD - PPROJ are added for records and record
projection. The rules for merges are changed to reduce components in parallel.
Parallel application. The distributivity rule in BCD subtyping indicates that a merge offunctions can be applied. While the current typing rule can check such applications withsuitable annotations, designing new reduction rules is necessary. An intuitive solution is tohave a rule that distributes the input value, like
(v1 ,, v2 ) v ,→ v1 v ,, v2 v
Assuming that v1 and v2 are consistent but not disjoint, to obtain preservation, v1 v andv2 v have to be consistent. To avoid the complexity of extending consistency to expressions including applications, we design parallel application (Figure 17) to distribute andsubstitute the input value in a big-step style, where a function application is divided into
two parts v and vl, and steps to an expression e. Consider a merge of three functions being
applied to a value. Compared to adding the previous single rule to the small-step reduction, parallel reduction helps us to “jump” from (f1 ,, f2 ,, f3 ) v to a merge of annotatedterms when reasoning about reduction. Every lambda gets the input directly without intermediate reduction steps such as ((f1 ,, f2 ) v) ,, f3 v. Record projection is handled in a similarstyle. In this case, v is a record value, and vl stands for a label instead.
{l = 1} ,, ({l = True} ,, {l = 1}) • {l} ,→ 1 ,, (True ,, 1)
The above example shows how merged records are projected in parallel, and the wholeterm is kept consistent. Rule PAPP - TOP shows that the top value can be used as a functionthat returns >, or a record which contains > in its field. With it, rule S TEP - BCD - PAPP
subsumes the rule S TEP - TOP in Figure 8.
Parallel reduction of merges. To maintain consistency of subterms in a merge (which
may contain non-values), as required by the typing rule T YP - MERGEV, we reduce every
component in a merge simultaneously through rule S TEP - BCD - MERGE. This rule is helpful to preserve consistency of pre-values during reduction, and therefore enables the typepreservation theorem. As a counter-example, if parallel reduction is not employed, we45Journal of Functional Programmingv • vl ,→ e(Parallel Application)

PAPP - ABS

v ,→A v0
λ x. e : A → B • v ,→ (e[x 7→ v0 ]) : B

PAPP - PROJ

PAPP - TOP{l = v} • {l} ,→ v

> • vl ,→ >PAPP - MERGE

v1 • vl ,→ e1v2 • vl ,→ e2(v1 ,, v2 ) • vl ,→ e1 ,, e2
e ,→ e0(Reduction (λ+i Extension))

S TEP - BCD - PAPPS TEP - BCD - RCDS TEP - BCD - PROJS TEP - BCD - PPROJ

v1 • v2 ,→ ee ,→ e0

e ,→ e0v • {l} ,→ v0

v1 v2 ,→ e{l = e} ,→ {l = e0 }

e.l ,→ e0 .l

v.l ,→ v0

S TEP - BCD - MERGE

e1 ,→ e01

S TEP - BCD - MERGEL

e2 ,→ e02

e1 ,, e2 ,→ e01 ,, e02

S TEP - BCD - MERGER

e1 ,→ e01

e2 ,→ e02

e1 ,, v2 ,→ e01 ,, v2

v1 ,, e2 ,→ v1 ,, e02

Fig. 17. Parallel application and reduction of λ+i (extends Figure 8).

might encounter the following reduction step:(1 + 1) : Int ,, (1 + 1) : Int ,→ 2 : Int ,, (1 + 1) : Int
where the r.h.s term is ill-typed, since the subterms are not consistent any more. In contrast, rule S TEP - BCD - MERGE will keep the reduction of terms synchronized. When one of
the subterms is already a value, rule S TEP - BCD - MERGE no longer applies. In that case,rule S TEP - BCD - MERGEL or rule S TEP - BCD - MERGER reduces the other subterm.
Overloading on return types. The λi and λ+i calculi support a form of overloading on
return types. With parallel application, we can even merge multiple functions and apply
them together to one input. Eventually, the return value would be a combination of theoutputs of all functions, and can play the role of any single output. The following example
shows how this mechanism works.

,→
,→
,→
,→

not ((λ x. x + 1 : Int → Int ,, λ x. True : Int → Bool) 1){ by S TEP - BCD - PAPP and parallel application }not (2 : Int ,, True : Bool){ by S TEP - APPR, S TEP - BCD - MERGE, S TEP - ANNOV and typed reduction }not (2 ,, True){ assuming not has type Bool → Bool }False : Bool{ by S TEP - ANNOV and typed reduction }
False

46

Taming the Merge Operator(BCD Runtime Subtyping (λ+i Extension))AB

RS UB - BCD - TOP

RS UB - BCD - RCD

A Ordinary+AB{l : A}  {l : B}

eAd

Top  ARS UB - BCD - SPLIT

B1  B  B2

A1  A  A2
A1  B1

A2  B2AB

Fig. 18. Runtime subtyping of λ+i extends the definition in Figure 7.
7.3 Metatheory
Completeness of the type system with respect to the original λ+i (or NeColus) calculus. Besides the extra rule for consistent merges (rule T YP - BCD - MERGEV), λ+i has twodifferent rules for record projection and function application when compared with the typesystem of NeColus (Bi et al., 2018).
Γ `n e ⇔ A(NeColus Typing (Selected))
N EC -T- PROJ

N EC -T- APPΓ `n e1 ⇒ A1 → A2

Γ `n e2 ⇐ A1

Γ `n e1 e2 ⇒ A2

Γ `n e ⇒ {l : A}
Γ `n e.l ⇒ A

To show that every well-typed term in NeColus can be type-checked in λ+i , we prove thefollowing lemmas:
Lemma 7.4 (λ+i application subsumes NeColus’s application). For any expressions e1 ande2 , if Γ ` e1 ⇒ A → B and Γ ` e2 ⇐ A, then Γ ` e1 e2 ⇒ B.
Lemma 7.5 (λ+i projection subsumes NeColus’s projection). For any expressions e andany label l, if Γ ` e ⇒ {l : A}, then Γ ` e.l ⇒ C.
Then it is straightforward that NeColus can be translated into λ+i . In our Coq formalization
we designed an elaboration from NeColus to λ+andprovedthecompleteness of λ+ii ’s typesystem with respect to NeColus.
Properties of the TDOS. The TDOS of λ+i preserves determinism, progress, and subjectreduction. Most of the proof follows λi ’s structure. Runtime subtyping is extended, and the
newly added parallel application requires some extra lemmas.
Runtime subtyping and preservation. Compared with Figure 7, λ+i ’s runtime subtyping
has one more rule for record types, and two rules changed for distributivity (Figure 18).
Rule RS UB - BCD - RCD allows a record type to be a runtime subtype of another record
type if their label is the same and the former’s field type is a runtime subtype of the latter’s.
Type A is constrained to be ordinary in rule RS UB - BCD - TOP. Therefore, Top  Top & Top
and A → Top  A → Top & Top are no longer derivable. The change is to maintain theJournal of Functional Programming

47

transitivity of subtyping. As a consequence of the generalization of rule RS UB - AND torule RS UB - BCD - SPLIT, an intersection type can be a runtime supertype of an arrow type.
However, A → Top, as an ordinary type, is not a runtime subtype of (A → Top) & (A →Top), and that would break transitivity. Since we need rule RS UB - BCD - SPLIT to help somemerges of functions to act as a function, we choose to drop the unneeded A → Top  A →Top & Top.
Parallel application. Some extra lemmas about parallel application are proved:
Lemma 7.6 (Type preservation of parallel application on functions). If · ` v1 v2 ⇒ A, andv1 • v2 ,→ e then · ` e ⇒ A.
Lemma 7.7 (Type preservation of parallel application on records). If · ` v1 .l ⇒ A, andv1 • {l} ,→ e then · ` e ⇒ A.
For both function application and record projection, parallel reduction preserves theoriginal type. Furthermore we can prove the following determinism lemmas:
Lemma 7.8 (Determinism of parallel application on functions). If · ` v1 v2 ⇒ A, v1 •v2 ,→ e1 , v1 • v2 ,→ e2 then e1 = e2 .
Lemma 7.9 (Determinism of parallel application on records). If · ` v1 .l ⇒ A, v1 • l ,→e1 , v1 • l ,→ e2 then e1 = e2 .
We can also prove the following progress lemmas for parallel application:
Lemma 7.10 (Progress of parallel application on functions). If · ` v1 v2 ⇒ A, then ∃e,v1 • v2 ,→ e.
Lemma 7.11 (Progress of parallel application on records). If · ` v1 .l ⇒ A, then ∃e, v1 •l ,→ e.
Finally, based on all the lemmas above, the key properties of reduction can be derived,
including type preservation with runtime subtyping:
Lemma 7.12 (Type preservation of ,→ with respect to runtime subtyping). If · ` e ⇒ A,
and e ,→ e0 then exists B, · ` e0 ⇒ B and B  A.
And its corollary:
Theorem 7.1 (Type preservation of ,→). If · ` e ⇒ A, and e ,→ e0 then · ` e0 ⇐ A.
Determinism and progress theorems are proved as well.
Theorem 7.2 (Determinism of ,→). If · ` e ⇒ A, e ,→ e1 , e ,→ e2 , then e1 = e2 .
Theorem 7.3 (Progress of ,→). If · ` e ⇒ A, then e is a value or ∃e0 , e ,→ e0 .

48Taming the Merge Operator
8 Discussion

This section provides some discussion on design choices, a comparison with elaboration
semantics as well as implementation considerations and possible extensions for futurework.
8.1 TDOS versus an Elaboration Semantics
This paper proposes the use of type-directed operational semantics for modelling languages
with a merge operator. Since a general form of the merge operator has a type-directedsemantics, previous work has favored an elaboration semantics. Traditionally, for languages with type-directed semantics, elaboration has been a common choice. That is thecase, for instance, for many previous calculi with the merge operator (Dunfield, 2014;
Oliveira et al., 2016; Alpuim et al., 2017; Bi et al., 2018, 2019), gradual typing (Siekand Taha, 2006), or type classes (Wadler and Blott, 1989; Kaes, 1988). In the elaboration approach, the idea is that the source language can be translated via a type-directedtranslation into a conventional target calculus, whose semantics is not type-directed. In thecase of languages with the merge operator, the target calculus is typically a conventional
calculus (such as the STLC) extended with pairs. The implicit upcasts that extract components from merges are modelled by explicit projections with pairs. One very appealing
benefit of the elaboration semantics is that it gives a simple way to obtain an implementation. Since elaboration targets conventional languages/calculi, that means that it can simply
reuse existing and efficient implementations of languages. For example, in the case of themerge operator, a key motivation of Dunfield (2014) was that the elaboration could just target ML-like languages, which have several efficient implementations available. From theimplementation point-of-view, the TDOS would be more useful for guiding the design ofa dedicated virtual machine, compiling directly to bytecode/assembly, or having an interpreter. However, obtaining an efficient implementation for the latter options would requiresignificantly more effort than with an elaboration approach.
Nevertheless, the reason for designing a semantics for a language or calculus is not
merely implementation. In fact, the implementation aspects are not our primary motivation
for TDOS. Although, as we will discuss in Section 8.2, TDOS can provide some insights
for obtaining efficient implementations as well. Furthermore we do not view TDOS as
being mutually exclusive with elaboration: both approaches have interesting aspects andthey can serve different purposes. Our main motivation for the TDOS is reasoning. A
semantics is supposed to describe the meaning of the language constructs in the language.
Having a clear and high-level presentation of the semantics is then useful for language
implementers to understand the behaviour of the language. Furthermore, it is also useful toprovide programmers with a mental model of how programs are executed, and to study theproperties of the language. Next, we give more details on the advantages of a direct semantics over the elaboration semantics in terms of reasoning and proof methods employed inprevious work on disjoint intersection types.
Shorter, more direct reasoning. Programmers want to understand the meaning of theirprograms. A formal semantics can help with this. With our TDOS we can essentiallyemploy a style similar to equational reasoning in functional programming to directly

49

Journal of Functional Programming
T- MERGE...
T- ANN...

· ` (2 ,, ‘c’) ⇒ Int & Char (2 , ‘c’)····S UB - ANDL
λ x. x + 1····
Int & Char <: Int·
T- SUB· ` (2 ,, ‘c’) ⇐ Int fst (2 , ‘c’)· ` (λ x. x + 1 : Int → Int) ⇒ Int → Int······
T- APP· ` (λ x. x + 1 : Int → Int) (2 ,, ‘c’) ⇒ Intfst(λ x. x + 1) (fst (2 , ‘c’))Fig. 19. Elaboration of (λ x. x + 1 : Int → Int) (2 ,, ‘c’) to a calculus with products.
reason about programs written in λi . For example, it takes a few reasoning steps to workout the result of (λ x. x + 1 : Int → Int) (2 ,, ‘c’):

,→
,→
,→

(λ x. x + 1 : Int → Int) (2 ,, ‘c’)
(2 + 1) : Int
3 : Int
3

by S TEP - BETA and typed reduction
by S TEP - ANNO and arithmetic
by S TEP - ANNOV and typed reduction

Here reasoning is easily justifiable from the small-step reduction rules and type-directed
reduction. Building tools (such as debuggers), that automate such kind of reasoning shouldbe easy using the TDOS rules.
However, with an elaboration semantics, the (precise) reasoning steps to determine thefinal result are more complex. Firstly the expression has to be translated into the target
language before reducing to a similar target term. Figure 19 shows this elaboration processin λi , where an expression in the source language is translated into an expression in a target language with products. The source term (λ x. x + 1 : Int → Int) (2 ,, ‘c’) is elaborated
into the target term (λ x. x + 1) (fst (2 , ‘c’)). As we can see the actual derivation is rather
long, so we skip the full steps. Also, for simplicity’s sake, here we assume the subtyping judgement produces the most straightforward coercion fst. This elaboration step andthe introduction of coercions into the program make it harder for programmers to precisely
understand the semantics of a program. Moreover while the coercions inserted in this small
expression may not look too bad, in larger programs the addition of coercions can be a lot
more severe, hampering the understanding of the program.
After elaboration we can then use the target language semantics, to determine a target
language value.

,→
,→
,→

(λ x. x + 1) (fst (2 , ‘c’))(λ x. x + 1) 2
2 +1
3

reduction for application and pairs
by the beta reduction ruleby arithmetic

A final issue is that sometimes it is not even possible to translate back the value of thetarget language into an equivalent “value” on the source. For instance in the NeColus calculus (Bi et al., 2018) 1 : Int & Int results in (1, 1), which is a pair in the target language.
But the corresponding source value 1 ,, 1 is not typable in NeColus. In essence, with an

50

Taming the Merge Operator

elaboration, programmers must understand not only the source language, but also the elaboration process as well as the semantics of the target language, if they want to precisely
understand the semantics of a program. Since the main point of semantics is to give clear
and simple rules to understand the meaning of programs, a direct semantics is a better
option for providing such understanding.
Simpler proofs of unambiguity. For calculi with an elaboration semantics, unrestrictedintersections make it harder to prove coherence. Our λi calculus, on the other hand, has adeterministic semantics, which implies unambiguity directly. For instance, (1 : Int & Int) :Int only steps to 1 in λi . But it can be elaborated into two target expressions in the
NeColus calculus corresponding to two typing derivations:(1 : Int & Int) : Int

fst (1, 1)(1 : Int & Int) : Int

snd (1, 1)

Thus the coherence proof needs deeper knowledge about the semantics: the two different
terms are known to both reduce to 1 eventually. Therefore they are related by the logicalrelation employed in NeColus for coherence. Things get more complicated for functions.
The following example shows two possible elaborations of the same function. Relatingthem requires reasoning inside the binders and a notion of contextual equivalence.
λ x. x + 1 : Int & Int → Int

λ x. fst x + 1

λ x. x + 1 : Int & Int → Int

λ x. snd x + 1

Furthermore, the two target expressions above are clearly not equivalent in the generalcase. For instance, if we apply them to (1, 2) we get different results. However, the target
expressions will always behave equivalently when applied to arguments elaborated fromthe NeColus source calculus. NeColus, forbids terms like (1 ,, 2) and thus cannot produce atarget value (1, 2). Because of elaboration and also this deeper form of reasoning required
to show the equivalence of semantics, calculi defined by elaboration require a lot more
infrastructure for the source and target calculi and the elaboration between them, while
in a direct semantics only one calculus is involved and the reasoning required to prove
determinism is quite simple.
Not limited to terminating programs. The (basic) forms of logical relations employed by
NeColus and Fi+ has cannot deal with non-terminating programs. In principle, recursion
could be supported by using a step-indexed logical relation (Ahmed, 2006), but this isleft for future work. λi smoothly handles unrestricted intersections and recursion, using
TDOS to reach determinism with a significantly simpler proof method. It also makes otherfeatures that lead to non-terminating programs, such as recursive types, feasible.
8.2 Implementation considerations
The TDOS for λi and λ+i is implementable directly, since the relations developed in thispaper are all essentially algorithmic. However, a direct implementation will not be very
efficient, for multiple reasons. Next we discuss some considerations for the design ofefficient implementations of languages with the merge operator.

Journal of Functional Programming

51

Merge lookups. From the efficiency point of view, one particularly bad aspect of the
TDOS is that run-time lookup on merges (triggered by typed reduction) does not exploit
statically known information. For instance, if we have a program such as:
let x : ... & Int & ... = ... ,, 2 ,, ... in x + 1
extracting the number 2 from the merge currently requires blindly going through theelements in the merge at runtime until the integer value is found. The approach in theelaboration semantics is much better here, since during type-checking we know staticallywhere the integer value can be found. Therefore, when generating code in the target language we can simply look up the value directly at that position, thus avoiding having tosearch for the value in the merge at runtime. It should be possible to create optimizations
for the TDOS by employing similar ideas to the elaboration. That is, using the type system
to statically determine where to find values. For this to work with the TDOS, we would
need to extend the TDOS with explicit projections, so that code with implicit projections
could be replaced with explicit projections. For instance, if the integer 2 is at position 5 ina merge, the code x + 1 could be replaced by x[5] + 1, where x[5] denotes the projection of
the 5th element in the merge. We should remark that, for such optimizations to be correct,
it is essential that the origin of values can be statically determined. As we have discussed
in Section 2.1, with some alternative semantics for the merge operator that may not be thecase. Therefore, such optimizations would be invalid.
Overhead from annotations. One other source of concern for efficiency is the overheadcaused by type annotations, and their use at runtime. Type annotations in a TDOS play avery similar role to casts in cast languages (Wadler and Findler, 2009; Siek and Wadler,2010), which are used, for instance, as targets for gradually typed languages. The problem of how to design efficient cast languages is an important topic in the gradual typing
literature, and the overhead caused by casts have been a notorious challenge in that area.
In particular, a main source of overhead comes from casting functions. In calculi such as
the blame calculus, function values need to accumulate casts to avoid raising blame too
early. Thus, function values can have an arbitrary number of casts, which also leads tospace efficiency concerns. Luckily, for λi and λ+i , we do not need to accumulate annotations around function values. Indeed, as shown in Section 4, function values are of theform λ x. e : A → B in λi and λ+i . That is, they only contain a single annotation. In contrast
to cast calculi, the approach used in λi and λ+i , when reduction encounters multiple annotations around a function is to simply replace the type annotation of the value. This process
happens in the typed reduction rule TR- ARROW for functions:TR- ARROW¬eA2 dA1 <: B1B2 <: A2

λ x. e : B1 → B2 ,→(A1 →A2 ) λ x. e : B1 → A2
Moreover, as discussed in Section 5.2, the premise A1 <: B1 is not needed at runtime, andcan be avoided in an implementation. Thus, while the overhead caused by type annotations
is still a concern, we believe that λi and λ+i avoid some of the thornier issues that gradually
typed languages have to deal with. Moreover, annotation replacement could actually havesome advantages over an elaboration approach. Multiple annotations around functions,would result in multiple coercions being applied to the function in an elaboration approach.

52

Taming the Merge Operator

In contrast annotation replacement avoids such coercions and immediately collapses annotations, so that, ultimately, we only need to type-reduce the argument and the result of
the function one time. Nevertheless, a proper assessment of the performance impact ofannotations at runtime is outside of the scope of this work, and left for future work.
Parallel application. Parallel application in λ+i may raise some concern if available inunrestricted ways to programmers. In λ+parallelapplication arises as a consequence ofithe distributivity of intersections over functions. That is, the following is a valid subtyping
statement in λ+i (and BCD subtyping):(A1 → B1 )&(A2 → B2 ) <: A1 &A2 → B1 &B2In essence, an intersection of two functions can be viewed as a single function with theintersections of the inputs and outputs. Thus, parallel application arises naturally in thesemantics of the language in order to support such form of conversions at runtime.
The semantics for the application of merged functions is to apply all of the functions to
the argument. This turns what looks like one function call into two or more function calls
and could have a significant impact on the time complexity of a program. A program thatlooks linear-time could in fact be exponential, due to parallel application. Therefore it isimportant to consider the consequences of parallel application and how they can be mitigated. One option would be to redesign the calculus so that parallel application is avoided.
This would probably require weakening the subtyping relation to avoid type conversions
like the above. However, parallel application is an important aspect of nested composition,and dropping parallel application from the calculus would prevent important applicationsof nested composition. Instead we believe that a better approach is to restrict the use ofparallel application in the source language that targets λ+i . In the following section we will
come back to this topic.
8.3 Design of Source Languages
SEDEL is an existing implementation of a source language that targets calculi closely
related to λi and λ+i . In essence the two implementations of SEDEL (Bi and Oliveira,2018; Bi et al., 2019) target Fi (Alpuim et al., 2017) and Fi+ (Bi et al., 2019), which are,respectively, polymorphic versions of λi and λ+i (but with an elaboration semantics). As
already discussed in Section 2, the examples that we presented in this paper are written
in a monomorphic subset of SEDEL, and can be encoded into λi and λ+i following theencoding proposed by Bi and Oliveira (2018).
While calculi like λi and λ+i are supposed to be closer to source languages, they are stillcore calculi and are not meant to be used directly for programming. Here we discuss some
important considerations for the design of source languages.
Type inference. λi and λ+i employ explicit annotations at runtime to determine the final
result of a program. However, while not too heavy, some of those annotations can becumbersome to write explicitly by programmers. In λ+i , the rules of records essentiallyrequire explicit type annotations when multiple distinct field names exist. For example, thefollowing program is not directly accepted:({m = 1} ,, {n = True}).n

Journal of Functional Programming

53

Instead, to retrieve True, we need to write:(({m = 1} ,, {n = True}) : {n : Bool}).n
The explicit annotation specifies both the field name and the type that we wish to look up.
Note that, since records can have fields with the same names and disjoint types, having thetype is helpful to select from those fields. For simplification, the SEDEL language accepts:({m = 1} ,, {n = True}).ndirectly, and inserts the missing annotation when elaborating to the core language. Once
SEDEL finds a field lookup expression e.n, it infers the type of e and then filters that typeusing the label n. For the example above, the inferred type of record is:({m = 1} ,, {n = True}) : {m : Int} & {n : Bool}and the filtered type is {n : Bool}. That annotation is inserted into the expression, resultingin:(({m = 1} ,, {n = True}) : {n : Bool}).n
Parallel application again. Parallel application is a useful feature. It is used, for instance,in the example shown in Section 2.3, in the SEDEL code:
fac = new[ExtLang] implExt;
e = fac.add (fac.neg (fac.lit 2)) (fac.lit 3)

The add call above is employing parallel application and it will call the two implementations for add in the traits implPrint and implLang. Therefore, parallel applications playa fundamental role in “family polymorphism” style applications, and cannot be entirely
avoided without ruling out interesting applications. Nevertheless, as argued in Section 8.2
allowing a completely unrestricted form of parallel application may be undesirable. One
possibility is to restrict the use of parallel applications in the source language. For instance,
we may consider not allowing merges directly in the source language, and only use themto encode source-level features. In the interests of first-class traits with nested composition, we can use merges in the encoding of traits only. It leads to a language similar tolanguages with family polymorphism and virtual classes (Ernst, 2001). In such languages,
nested composition is limited to nested composition of classes. An alternative option isto keep merges in the source language, but forbid parallel application for such merges.
Therefore, the core language would still have parallel application, but the source language
merges do not. Potentially, we could try to implement an overloading-like semantics forthe source language merges, instead of parallel application.
Furthermore our current dynamic semantics for parallel applications is simple, but naive.
One possible way to optimize parallel application is through specialization. For instance,in the code:
fac = new[ExtLang] implExt;

we could generate a new trait implementation such as:trait facSpecialized ⇒ {lit (x: Double) = {print = x.ToString, eval = x}
add (x:IEval&IPrint) (y:IEval&IPrint) =54Taming the Merge Operator{
print = "(" ++ x.print ++ " + " ++ y.print ++ ")",
eval = x.eval + y. eval}}That is we would just syntactically merge all components recursively, eliminating a lot of
the overhead induced by nested merges. When specialization can be applied, it could leadto very significant performance improvements. However such an approach assumes thatthe source code of the original implementations is known, and we have not looked yet atthe technical details of how to implement this. Nevertheless such a specialization approachis related to flattening of traits (Nierstrasz et al., 2006), which has been used to generate
new traits/classes from the composition of multiple traits.
Finally, we believe that work on the compilation of virtual classes will shed light on how
to optimize parallel application, since virtual classes need to be able to encode code thatis similar to the fac and e definitions above. As part of future work on the compilation of
languages with the merge operator, we plan to look more closely at existing compilation
models for virtual classes, and see whether some of the ideas can be employed to havemore efficient forms of parallel application.
8.4 Extensions
There are several avenues for future work. In the setting of disjoint intersection types,
an obvious extension is disjoint polymorphism (Alpuim et al., 2017), which adds polymorphism into calculi with disjoint intersection types. We discuss two other extensions
next.
First-class record labels. Instead of having two constructs for record and record projection as our current system does, we believe it is also possible to employ first-class labels.
First-class labels are used in some record calculi with extensible rows (Leijen, 2004).
Record {l = 1} would have type Lab l → Int in the new setting, where the type Lab l is
the type of label. Therefore, to project a field against the label l we would apply it to a termof type Lab l. Using first-class labels the parallel application (defined on Figure 17) could
be simplified and unified further. Moreover, the syntactic sort vl would not be needed, aslabels would already be values.
Splittable union types. Although our calculus does not support union types, splittabletypes (defined in Figure 11) have the potential to be extended to union types (A|B). For
example, assume that the rule:
A → C  (A | B) → C  B → C

is added to the existing definition of splittable types. Combined with rule S- BCD - AND,then the following subtyping statement is derivable:(A → C) & (B → C) <: (A | B) → C
This means that two functions with the same input type can be merged and act as a function. Besides this, we believe that it is also possible to add a dual of the rule S- BCD - ANDJournal of Functional Programming55

in the modular BCD subtyping to accomplish more union-related subtyping. We hope toinvestigate this further in the future.
9 Related Work
This section discusses various lines of related work, including calculi with a merge
operator, record calculi and some work on OOP languages.
9.1 Calculi with the merge operator and a direct semantics
Intersection types with a merge operator are a key feature of the Forsythe language of
Reynolds (1988). Reynolds (1991) also studied a core calculus with similarities to λi .
However, merges in Forsythe are restricted and use a syntactic criterion to determine whatmerges are allowed. A merge is permitted only when the second term is a lambda abstraction or a single field record, which makes the structure of merges always biased. To prevent
potential ambiguity, the latter overrides the former when they overlap. If formalized as atree, the right child of every node is a leaf. The only place for primitive types is the leftmost component. Forsythe follows the standard call-by-name small-step reduction, during
which types are ignored. The reduction rules deal with merges by continuously checking if
the second component can be used in the context (abstractions for application, records for
projection). This simple approach, however, is unable to reduce merges when (multiple)
primitive types are required. Reynolds (1997) admitted this issue in his later work. We use
types to select values from a merge and the disjointness restriction guarantees the determinism. Therefore the order of a value in a merge is not a deciding factor on whether thevalue is used.
The calculus λ & proposed by Castagna et al. (1995) has a restricted version of themerge operator for functions only. The merge operator is indexed by a list of types of
its components. Its operational semantics uses the runtime types of values to select the“best approximate” branch of an overloaded function. λ & requires runtime type checking on values, while in TDOS, all type information is already present in type annotations.
Another obvious difference is that λi supports merges of any type (not just functions),
which are useful for applications other than overloading of functions, including: multifield extensible records with subtyping (Oliveira et al., 2016); encodings of objects andtraits (Bi and Oliveira, 2018); dynamic mixins (Alpuim et al., 2017); or simple forms offamily polymorphism (Bi et al., 2018).
Several other calculi with intersection types and overloading of functions have been
proposed (Castagna and Xu, 2011; Castagna et al., 2015, 2014), but these calculi do notsupport a merge operator, and thus avoid the ambiguity problems caused by the construct.
9.2 Calculi with a Merge Operator and an Elaboration Semantics
Instead of a direct semantics, many recent works (Dunfield, 2014; Oliveira et al., 2016;
Alpuim et al., 2017; Bi et al., 2018, 2019) on intersection types employ an elaboration
semantics, translating merges in the source language to products (or pairs) in a target language. With an elaboration semantics the subtyping derivations are coercive (Luo, 1999):
they produce coercion functions that explicitly convert terms of one type to another in thetarget language. This idea was first proposed by Dunfield (2014), where she shows how to56

Taming the Merge Operator

elaborate a calculus with intersection and union types and a merge operator to a standard
call-by-value lambda calculus with products and sums. Dunfield also proposed a directsemantics, which served as inspiration for our work. However, her direct semantics is nondeterministic and lacks subject reduction (as discussed in detail in Section 3.1). Unlike
Forsythe and λ &, Dunfield’s calculus has unrestricted merges and allows a merge to work
as an argument. Her calculus is flexible and expressive and can deal with several programs
that are not allowed in Forsythe and λ &.
To remove the ambiguity issues in Dunfield’s work, the original λi calculus (Oliveira
et al., 2016) forbids overlapping in intersections using the disjointness restriction for all
well-formed intersections. In other words, it does not support unrestricted intersections.
Because of this restriction, the proof of coherence in the original λi is still relatively simple.
Likewise, in the following work on the Fi calculus (Alpuim et al., 2017), which extends λiwith disjoint polymorphism, all intersections must be disjoint. However, the disjointness
restriction causes difficulties because it breaks stability of type substitutions. Stability is a
desirable property in a polymorphic type system that ensures that if a polymorphic typeis well-formed then any instantiation of that type is also well-formed. Unfortunately, withdisjoint intersections only, this property is not true in general. Thus Fi can only prove a
restricted version of stability, which makes its metatheory non-trivial.
Disjointness of all well-formed intersections is only a sufficient (but not necessary)
restriction to ensure an unambiguous semantics. The NeColus calculus (Bi et al., 2018)
relaxes the restriction without introducing ambiguity. In NeColus 1 : Int & Int is allowed,
but the same term is rejected in the original λi . NeColus employs the disjointness restriction only on merges, but otherwise allows unrestricted intersections. Unfortunately, thiscomes at a cost: it is much harder to prove the coherence of elaboration. Both NeColus andFi+ (Bi et al., 2019) (a calculus derived from Fi that allows unrestricted intersections) deal
with this problem by establishing coherence using contextual equivalence and a logicalrelation (Tait, 1967; Plotkin, 1973; Statman, 1985) to prove it. The proof method, however, cannot deal with non-terminating programs. In fact, none of the existing calculi withdisjoint intersection types supports recursion, which is a severe restriction.
We retain the essence of the power of Dunfield’s calculus (modulo the disjointness
restrictions to rule out ambiguity), and gain benefits from the direct semantics. Figure 20
summarizes the key differences between our work and prior work, focusing on the mostrecent work on disjoint intersection types. Note that the row titled “Coercion Free” denotes
whether subtyping generates coercions or not. Our calculi are coercion free, while all othercalculi based on an elaboration semantics employ coercive subtyping.
9.3 Record Calculi with Record Concatenation and Subtyping
As we have seen, in calculi with disjoint intersection types and records, the merge operator concatenates records in a symmetric way. However, designing a record concatenation
operator, no matter symmetric or asymmetric, is a difficult problem in calculi with subtyping, as identified by Cardelli and Mitchell (1991). In both cases, a record can “hide” somefields via subsumption to bypass the restriction on types. As far as we know, no existing
record calculus in the literature supports nested composition. However, there are numerous
designs in the literature with concatenation or subtyping or both.

57

Journal of Functional Programming

Disjointness
Unrestricted Intersections
Determinism or Coherence
Coercion Free
Recursion
Direct Semantics
Subject Reduction
BCD Subtyping

λ,,λi '16Fi

NeColus Fi+

λi

λ+
i

No

Coh.

Coh.

Coh.

Coh.

Det.

Det.

-

-

-

-

Fig. 20. Summary of intersection calculi with the merge operator.
λ,, stands for Dunfield’s calculus. Note that λi '16 is the original one by Oliveira et al.
(2016), whereas λi is the variant introduced in this paper.
( = yes, = no, - = not applicable )Asymmetric concatenation without subtyping. Record concatenation is used by Wand
(1989) to model multiple inheritance. He has a biased operator, which overrides the firstterm by the second if they have conflicting fields. Wand (1989) makes every record types
explicitly state whether a field is present in it or absent with respect to a fixed set of labels,
which could be infinite. It is similar to the algorithm implemented by Rémy (1989) totype-check records in an ML extension, which keeps track of if a field is absent or not.
Symmetric concatenation without subtyping. Harper and Pierce (1991) design a record
calculus with symmetric concatenation. Their system keeps the extension and restriction
operators in terms and types and generalizes them to work on two records (or record types).
A compatibility check is enforced on types, via the typing of record concatenation and typewell-formedness definition. Their type quantification only takes care of negative information. For example, Λa#l.a stands for any type that does not have a field of name l. Although
they avoid subtyping, it is still necessary to reason about type equivalence with the type
operations in their calculus.
A similar disjointness constraint for symmetric record concatenation is employed for by
the language Ur presented by Chlipala (2010), which has a more comprehensive reasoning
on type equivalence. Ur is a dependently typed language with first-class labels, designed
for statically typed meta-programming with type inference. It encodes disjoint assertions
in guarded types. Ur uses type-level computation, including a type-level map operation,
to allow flexible and generic programs to be written using records. The semantics is givenby elaboration, and a translation of Ur programs into terms of the Calculus of Inductive
Constructions ensures type soundness. Like Harper and Pierce’s work, Ur has no subtyping
as it introduces ambiguity. The absence of subtyping avoids the “hidden fields” problem.
Record subtyping without concatenation. Cardelli and Mitchell propose to use extension and restriction as primitive operators instead of concatenation. They introduce type
operators and negative restrictions in record types, so that in their calculus, via bounded
quantification, programmers can declare a polymorphic function that takes any records
lacking certain fields. Like merges in λ+i , extension in their system is conflict-free, whichis ensured by static type-checking. Compared to restriction, we can use type annotations
to drop fields in a record in λ+i . A difference is that the two operators deal with a recordand a field, while our system can handle two records in a merge. As identified by Cardelli

58

Taming the Merge Operator

and Mitchell (1991), with subtyping, a record can “hide” some fields via subsumption to
bypass the restriction on types, which makes it hard to capture the absent fields in record
calculi. Their solution is to add type operations that can encode negative information insubtyping. Corresponding to the term operators, they have two type operators of the same
name: extension on a type requires that the given field is absent from the type; restriction
on a type explicitly excludes the field from it, if it has such a field. For example, {}\l stands
for an empty record with a restriction that cannot have field l. Any subtype cannot have leither. Besides special subtyping rules, they define type equivalence rules to reason abouttype operations on records.
Subtyping-constraint-based calculi. Rémy (1995) and following work by Pottier (2000)
handle both symmetric and asymmetric concatenation in a constraint-based type system.
To deal with record concatenation, type operators or conditional constraints are used toexpress two branches: either a field exists or is absent, mirroring the reduction of programs.
In subtyping, the type of records are distinguished into two forms: rigid record types andflexible record types. A rigid record type of a term reflects all fields in it. Rigid records
have no subtyping, but they can be used in a concatenation with another record. Everyrigid record type corresponds to a flexible record type, which has subtypes and supertypes.
However flexible records cannot be used with concatenation. In λi and λ+i all records are
flexible and they can be used with concatenation. Moreover, the subtyping in their systems
is not expressive enough to support nested composition.
Record calculi as extensions of system F<: . The F<:ρ calculus proposed by Cardelli(1992) extends System F<: by extensible records, and combines row quantification usedin the previously discussed Harper and Pierce (1991)’s work with bounded quantification. F<:ρ does not have record concatenation as a primitive operator. Instead, it has row
extension and restriction. A translation to F<: is provided. Poll (1997) solves the polymorphic record update problem in System F with a restricted formulation of subtyping:it only supports width-subtyping on record types. It has a record-update operator insteadof concatenation. One record-update operation only alters a field in a record. The subtype
checking in its typing rule makes sure the record contains that field of the expected type.
The F# calculus by Zwanenburg (1995) supports intersection types (in its later version (Zwanenburg, 1997) intersection types are eliminated) and record concatenation ina F<: -like system. Similar to λ+i , multi-field records are obtained by concatenating singlefield records, and there is a distributivity rule for records in subtyping as well. They use
a “with” construct for record concatenation which is similar to the merge operator. Like
rule T YP - MERGE, the typing of “with” introduces intersections, and it has a compatibility
pre-condiction for the two terms’ types (written as A#B). Only record types or Top can
be compatible. The concatenation operator is asymmetric. When two concatenated records
have the same label, the right one overwrites the left. Correspondingly, two compatible
types can have common fields as long as for those shared fields, the right one has a subtypeof the left’s , e.g. {l : Int}#{l : Int} & {l : Char}. In contrast, disjointness is symmetric, anda type (unless it is top-like) cannot be disjoint with its subtypes, to ensure the two sides
of a merge coexist safely. To prevent the issue of subsumption “hiding” fields of different types the compatibility checking, they require explicit annotations on merged records.
These annotations are used during elaboration to a target calculus, therefore affecting theJournal of Functional Programming

59

program behavior, like in our calculus. The semantics of F# is given by elaborating into
system F with pairs and records. In this sense, it predates Dunfield’s work. Concatenatedrecords are translated into pairs, where a special “overwriter” function, generated by thecompatibility derivation, is applied to update the overlapped fields in the first record by thesecond one. In Zwanenburg (1995)’s work coherence is left for future work.
9.4 Languages and Calculi with Type-Dependent Semantics
Typed operational semantics. Goguen (1994) uses types in his reduction, similarly to
typed reduction in λi . However, Goguen’s typed operational semantics is designed forstudying meta-theoretic properties, especially strong normalization, and is not aimed todescribe type-dependent semantics. Unlike TDOS, in typed operational semantics, thereduction process does not use the additional type information to guide reduction. Instead,the combination of well-typedness and computation provides inversion principles for proving various metatheoretical properties. Typed operational semantics has been applied
to several systems. These include simply typed lambda calculi (Goguen, 1995), calculi
with dependent types (Goguen, 1994; Feng and Luo, 2009) and higher-order subtyping (Compagnoni and Goguen, 2003). Note that the semantics of these systems does notdepend on typing, and the untyped (type-erased) reduction relations are still presented todescribe how to evaluate programs.
Type classes (Wadler and Blott, 1989; Kaes, 1988) are an approach to parametric overloading used in languages like Haskell. The commonly adopted compilation strategy for
it is the dictionary passing style elaboration (Wadler and Blott, 1989; Hall et al., 1996;
Chakravarty et al., 2005,?). Other mechanisms inspired by type classes, such as Scala’s
implicits (Oliveira et al., 2010), Agda’s instance arguments (Devriese and Piessens, 2011)
or Ocaml’s modular implicits (White et al., 2014) have an elaboration semantics as well. In
one of the pioneering works of type classes, Kaes (1988) gives two formulations for a direct
operational semantics. One of them decides the concrete type of the instance of overloadedfunctions at run-time, by analyzing all arguments after evaluating them. In both Kaes’ workand the following work by Odersky et al. (1995), the run-time semantics has some restrictions with respect to type classes. For example, overloading on return types (needed forexample for the read function in Haskell) is not supported. Interestingly, the semantics of
λi allows overloading on return types, which is used whenever two functions coexist on amerge. For a detailed example, please refer to Section 7.2.
Gradual typing. (Siek and Taha, 2006) has become popular over the last few years.
Gradual typing is another example of a type-dependent mechanism, since the success or
not of an (implicit) cast may depend on the particular type used for the implicit cast. Thus
the semantics of a gradually typed language is type-dependent. Like other type-dependent
mechanisms the semantics of gradually typed source languages is usually given by a (typedependent) elaboration semantics into a cast calculus, such as the Blame calculus (Wadlerand Findler, 2009) or the Threesome calculus (Siek and Wadler, 2010).
Multiple dispatching. (Clifton et al., 2000; Chambers and Chen, 1999; Muschevici et al.,2008; Park et al., 2019) generalizes object-oriented dynamic dispatch to determine theoverloaded method to invoke based on the runtime type of all its arguments. Similarly

60

Taming the Merge Operator

to TDOS, much of the type information is recovered from type annotations in multiple
dispatching mechanisms, but, unlike TDOS, they only use input types to determine thesemantics.
9.5 Dealing with Conflicts in OOP
There is a rich literature in OOP with various solutions for dealing with (method) conflicts. As we have mentioned throughout the article, the approach to deal with conflicts
by employing disjointness and a symmetric merge operator is closely related to the trait
model (Schärli et al., 2003) in OOP. In the trait model, the idea is that the composition of
traits should only be accepted if there are no conflicts: i.e. conflicts should result in errors.
To resolve errors the trait model typically allows operations for renaming and/or removing
methods from an inherited trait. We can resolve conflicts in the same way, using subtyping to hide (remove) some values in a merge. Bi and Oliveira (2018) have shown how tobuild a source language with first-class traits on top of a calculus with a symmetric merge
operator. An alternative approach would be to have an asymmetric merge operator, suchas the one from Dunfield (2014). In such a case, conflicts would be automatically resolved
by simply employing the order of composition. Such a semantics is closely related to the
traditional semantics for mixins (Bracha and Cook, 1990; Flatt et al., 1998). However, thisapproach is prone to subtle errors arising from the implicit overriding of values/methods
triggered by the automatic (and implicit) resolution of conflicts.
Other approaches to conflicts in class-based languages. Several other approaches todeal with conflicts have been studied in the context of OOP. C++ supports a very expressivemodel of multiple inheritance that accepts two classes A and B with conflicting method
implementations to be inherited by a third class C. To deal with method invocations thathave multiple conflicting implementations, programmers in C++ can upcast C to either A or
B and then the ambiguity is removed because the static type (A or B) is used to decide whichof the methods to invoke. A simple formal model of such a mechanism in C++ (and someextensions) was described by Wang et al. (2018). A closely related approach was proposedby Flatt et al. (1998) in the context of mixins for a Java-like setting. The idea there is alsothat if a class inherits from multiple mixins with conflicting methods, then invocations ofconflicted methods can still be disambiguated by first upcasting the class to the mixin withthe method implementation that the programmer wishes to invoke. This approach is more
flexible than the traditional biased approach of mixin inheritance that employs the orderof mixins in composition to automatically override methods with conflicts. Furthermore,
it avoids the issues of unintentional errors due to accidental overriding of methods. In
such approaches nominal types play an important role, since the nominal types enabledistinguishing possible overlapping (or even equal) structural types. Our work is done in
the context of languages with structural types and thus it is closer to the work on record
calculi. However the addition of nominal types would be interesting to investigate andcould allow for improved mechanisms for conflict resolution.
Delegation-based languages. More generally, the very dynamic nature of merges isclosely related to delegation-based OOP languages (Lieberman, 1986; Kniesel, 1999;
Fisher and Mitchell, 1995; Ungar and Smith, 1988; Ostermann, 2002; Büchi and Weck,Journal of Functional Programming

612000). Delegation, originally introduced by Lieberman (1986), is a form of dynamic inheritance. With dynamic inheritance the inherited implementation is not statically known.
This is in contrast to static inheritance (which is widely adopted by mainstream OOP languages), where the inherited class must be known statically: in mainstream OOP languages,
when using class A extends B, B is some concrete (statically known) class. Delegation
can itself be further classified into two difference forms: static delegation and dynamic
delegation (Kniesel, 1999). In static delegation, the inherited implementation may be statically unknown, but it cannot be changed after it is “bound” to the object. In dynamic
delegation, the inherited implementation is stored in a mutable reference in the object andcan be changed at any time. The SEDEL language, for instance, adopts a static delegation
model, since the self-reference is immutable.
The Self language (Ungar and Smith, 1988) was the first OOP language to employ delegation. JavaScript has a closely related model and is directly inspired by Self. In Self
and JavaScript the idea is that an object has a property that holds a link to another object,which is called the prototype. The prototype object can have a prototype of its own, and soon. This offers a very dynamic model where prototype objects can be changed at runtime,by simply mutating the prototype reference. In other words, Self and JavaScript follow adynamic delegation approach. Due to their dynamically typed nature, there is no support
for statically detecting conflicts in JavaScript or Self.
Research on type systems for delegation-based languages is much less explored compared with class-based languages. Fisher and Mitchell (1995) were among the first to study
type systems for delegation. Kniesel (1999) further explored this space and has investigatedways to deal with issues arising from conflicts. In his model, he avoids most accidental overriding conflicts, by adopting a rule that a method m in one of the parents can only
(implicitly) override another method implementation with the same name in another parent,
if the two parents have a common parent class. This way, unrelated methods with the same
name cannot be accidentally overridden. The work by Ostermann (2002) adapts the idea offamily polymorphism to a delegation-based setting, and offers some of the advantages ofnested composition that is enabled in λi+ . There are a few other statically typed approaches
to delegation in the context of OOP programming (Büchi and Weck, 2000; Schaefer et al.,2011). Overall the main difference is that we are looking at foundational calculi using
intersection types and a merge operator in this article, instead of looking at the semantics
of high-level OOP languages. One application of the calculi in this paper is indeed to model
high-level programming abstractions for OOP languages, but that is not the focus of thiswork. In contrast the aforementioned related work on delegation is specifically focused on
the semantics of higher-level OOP languages and language mechanisms.
9.6 BCD Subtyping Algorithms
Pierce (1989) developed an algorithm for a form of subtyping close to BCD subtyping
using a queue of types. His algorithmic decision procedure le(σ , τ, τ) is equivalent to thedeclarative judgment σ ≤ τ → τ, where τ is the queue, containing known argument typesof the right-hand-side function type. When τ is a function type τ1 → τ2 , its argument type
τ1 is added to the queue. When σ is an intersection type σ1 & σ2 , the queue is duplicatedon both sub-branches in order to reflect the distributivity rule, by distributing the argument

62

Taming the Merge Operator

types to both components of an intersection type. The rule for function types, top types andintersection types then take care of argument types in the queue. Bi et al. (2018) adapted
Pierce’s algorithm to BCD subtyping and extended it with record types without majordifficulties.
The decidability of BCD subtyping is shown in several other works (Kurata and
Takahashi, 1995; Rehof and Urzyczyn, 2011; Statman, 2015) through manual proofs,
and there are also proofs formalized in Coq (Laurent, 2012; Bessai et al., 2016). Bessai
et al. (2019) developed a fast algorithm verified in Coq. Their algorithm is presented as arelational abstract machine specification, with a long proof due to the mismatch between
the styles of the declarative system and algorithmic system. In contrast, our algorithm isdefined in a simple relational form, keeping the modularity of existing rules, resulting ina novel, simple and concise formulation of the metatheory for the algorithm. Of course,
the two lines of work have quite distinct goals: while we emphasize the modularity andsimplicity of the metatheory, Bessai et al. are interested in a fast algorithm, which justifies
the additional complexity in the metatheory of their approach.
Muehlboeck and Tate (2018) developed a framework for subtyping algorithms withintersection and union types. They also showed a variant that supports minimal relevant
logic B+, which is a generalized system with intersection and union types, subsuming
BCD subtyping. To decide A <: B, they rewrite A with (a generalized version of) rule OSDISTA RR as much as possible. In contrast, we split B to make the types match. Siek (2019),
inspired by Laurent (2019), proposed a new subtyping system and proved the transitivity
lemma directly. Siek keeps the judgment form A <: B (like us), but most subtyping rules
require changes, and are less modular than our rules. Siek’s transitivity proof involves a size
measure, while we avoid any size measure by using an alternative relation of types (proper
types), which exploits the properties of our splittable type relation. Both works formalize
the transitivity property, as well as soundness and completeness to BCD subtyping in proof
assistants.
9.7 Parallel Reduction in Union-Related Calculi
Parallel reduction for typing unions. As discussed in Section 7.2, λ+i applies a mergeof multiple functions to the input together, and reduces every component in the resulting
merge simultaneously. Although their system does not have merges, Barbanera et al. (1995)
also employed a similar evaluation strategy called parallel beta-reduction in a calculus
with intersection and union types. They consider beta-redexes rather than components ina merge. Instead of reducing the leftmost beta-redex, all occurrences of the same redex
are reduced together. Likewise, their motivation is a typing rule that does not preserve
types under conventional beta-reduction. This typing rule eliminates union types. If e has
type A | B, the rule considers two cases: every occurrence of e has type A or has typeB, and type-checks the expression twice under the two assumptions. Since beta-reduction
can change the syntax form of such subterms, it has to be done in parallel. This kind of
reduction strategy was proposed by Knuth (1971), and formalized in (Barendregt, 1984,
Chapter 13), and is known as Gross-Knuth reduction.

Journal of Functional Programming63

10 Conclusion
In this work, we showed how a type-directed operational semantics allows us to address theambiguity problems of calculi with a merge operator. Therefore, with the TDOS approach,
we can answer the question of how to give a direct operational semantics for both thegeneral merge operator in a setting with intersection types, as well as, calculi with record
concatenation and subtyping. Both of these problems are well-known to be challenging in
the literature, while at the same time having important practical applications. Comparedwith the elaboration approach, having a direct semantics avoids the translation process
and a target calculus. This simplifies both informal and formal reasoning. For instance,
establishing the coherence of elaboration in NeColus (Bi et al., 2018) requires much
more sophistication than obtaining the determinism theorem in λ+i . Furthermore, the proof
method for coherence in NeColus cannot deal with non-terminating programs, whereas
dealing with recursion is straightforward in λi and λ+i . The TDOS approach exploits type
annotations to guide reduction. The key component of TDOS is typed reduction, whichallows values to be further reduced depending on their type.
Acknowledgements: We are grateful to anonymous reviewers and our colleagues Yaoda
Zhou, Andong Fan, Yaozhu Sun, Baber Rehman for their valuable comments which helped
improve the presentation and our understanding of this work. We also thank Yaozhu forimplementing our TDOS. This work has been sponsored by Hong Kong Research Grants
Council projects number 17209519 and 17209520.
Conflicts of Interest: None.

References
Ahmed, A. J. (2006) Step-indexed syntactic logical relations for recursive and quantified types.
Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006,
Proceedings. Springer. pp. 69–83.
Alpuim, J., d. S. Oliveira, B. C. & Shi, Z. (2017) Disjoint polymorphism. Programming Languages
and Systems - 26th European Symposium on Programming, ESOP 2017, Uppsala, Sweden, April
22-29, 2017, Proceedings. Springer. pp. 1–28.
Barbanera, F., Dezani-Ciancaglini, M. & De’Liguoro, U. (1995) Intersection and union types: syntax
and semantics. Information and Computation. 119(2), 202–230.
Barendregt, H. (1984) The lambda calculus - its syntax and semantics. Studies in logic and thefoundations of mathematics.
Barendregt, H., Coppo, M. & Dezani-Ciancaglini, M. (1983) A filter lambda model and thecompleteness of type assignment. The journal of symbolic logic. 48(4).
Bessai, J., Dudenhefner, A., Düdder, B. & Rehof, J. (2016) Extracting a formally verified subtyping
algorithm for intersection types from ideals and filters. TYPES.
Bessai, J., Rehof, J. & Düdder, B. (2019) Fast verified bcd subtyping. In Models, Mindsets, Meta:
The What, the How, and the Why Not?. vol. 11200 of Lecture Notes in Computer Science. Springer,
Cham. pp. 356–371.
Bi, X., d. S. Oliveira, B. C. & Schrijvers, T. (2018) The essence of nested composition. 32nd
European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018,
Amsterdam, The Netherlands. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. pp. 22:1–
22:33.

64

Taming the Merge Operator

Bi, X. & Oliveira, B. C. d. S. (2018) Typed first-class traits. 32nd European Conference on ObjectOriented Programming, ECOOP 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. pp.
9:1–9:28.
Bi, X., Xie, N., d. S. Oliveira, B. C. & Schrijvers, T. (2019) Distributive disjoint polymorphism forcompositional programming. Programming Languages and Systems - 28th European Symposiumon Programming, ESOP 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings. Springer.
pp. 381–409.
Bracha, G. & Cook, W. R. (1990) Mixin-based inheritance. Conference on Object-Oriented
Programming Systems, Languages, and Applications / European Conference on Object-Oriented
Programming (OOPSLA/ECOOP), Ottawa, Canada, October 21-25, 1990, Proceedings. ACM. pp.
303–311.
Büchi, M. & Weck, W. (2000) Generic wrappers. European Conference on Object-Oriented
Programming (ECOOP).
Cardelli, L. (1992) Extensible records in a pure calculus of subtyping. Digital. Systems ResearchCenter.
Cardelli, L. & Mitchell, J. (1991) Operations on records. Mathematical Structures in Computer
Science. 1, 3–48.
Cardelli, L. & Wegner, P. (1985) On understanding types, data abstraction, and polymorphism. ACM
Comput. Surv. 17(4), 471–522.
Castagna, G., Ghelli, G. & Longo, G. (1995) A calculus for overloaded functions with subtyping.
Inf. Comput. 117(1), 115–135.
Castagna, G., Nguyen, K., Xu, Z. & Abate, P. (2015) Polymorphic functions with set-theoretic
types: Part 2: Local type inference and type reconstruction. Proceedings of the 42nd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai,
India, January 15-17, 2015. ACM. pp. 289–302.
Castagna, G., Nguyen, K., Xu, Z., Im, H., Lenglet, S. & Padovani, L. (2014) Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. The 41st Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, 2014.
ACM. pp. 5–18.
Castagna, G. & Xu, Z. (2011) Set-theoretic foundation of parametric polymorphism and subtyping.
Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming,
ICFP 2011, Tokyo, Japan, September 19-21, 2011. ACM. pp. 94–106.
Chakravarty, M. M. T., Keller, G. & Jones, S. L. P. (2005) Associated type synonyms. Proceedingsof the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005,
Tallinn, Estonia, September 26-28, 2005. ACM. pp. 241–253.
Chakravarty, M. M. T., Keller, G., Jones, S. L. P. & Marlow, S. (2005) Associated types with class.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. ACM. pp. 1–13.
Chambers, C. & Chen, W. (1999) Efficient multiple and predicated dispatching. Proceedings ofthe 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages &Applications (OOPSLA ’99), Denver, Colorado, USA, November 1-5, 1999. ACM. pp. 238–255.
Chlipala, A. (2010) Ur: statically-typed metaprogramming with type-level record computation. ACM
Sigplan Notices. 45(6), 122–133.
Clifton, C., Leavens, G. T., Chambers, C. & Millstein, T. D. (2000) Multijava: modular openclasses and symmetric multiple dispatch for java. Proceedings of the 2000 ACM SIGPLAN
Conference on Object-Oriented Programming Systems, Languages & Applications (OOPSLA
2000), Minneapolis, Minnesota, USA, October 15-19, 2000. ACM. pp. 130–145.
Compagnoni, A. B. & Goguen, H. (2003) Typed operational semantics for higher-order subtyping.
Inf. Comput. 184(2), 242–297.
Cook, W. R. & Palsberg, J. (1989) A denotational semantics of inheritance and its correctness.
Object-Oriented Programming: Systems, Languages and Applications (OOPSLA).
Coppo, M., Dezani-Ciancaglini, M. & Venneri, B. (1981) Functional characters of solvable terms.
Math. Log. Q. 27(2-6), 45–58.

Journal of Functional Programming

65

Davies, R. & Pfenning, F. (2000) Intersection types and computational effects. Proceedings ofthe Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00),
Montreal, Canada, September 18-21, 2000. ACM. pp. 198–208.
Devriese, D. & Piessens, F. (2011) On the bright side of type classes: instance arguments in agda.
Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming,
ICFP 2011, Tokyo, Japan, September 19-21, 2011. ACM. pp. 143–155.
Dunfield, J. (2014) Elaborating intersection and union types. J. Funct. Program. 24(2-3), 133–165.
Dunfield, J. & Pfenning, F. (2003) Type assignment for intersections and unions in call-by-value
languages. Foundations of Software Science and Computational Structures, 6th International
Conference, FOSSACS 2003, Warsaw, Poland, Proceedings. Springer. pp. 250–266.
Ernst, E. (2001) Family polymorphism. Proceedings of the 15th European Conference on ObjectOriented Programming. Berlin, Heidelberg. Springer-Verlag. p. 303–326.
Facebook. (2014) Flow. https://flow.org/.
Feng, Y. & Luo, Z. (2009) Typed operational semantics for dependent record types. Proceedings
Types for Proofs and Programs, Revised Selected Papers, TYPES 2009, Aussois, France, 12-15th
May 2009. pp. 30–46.
Fisher, K. & Mitchell, J. (1995) A delegation-based object calculus with subtyping. Fundamentals ofComputation Theory.
Flatt, M., Krishnamurthi, S. & Felleisen, M. (1998) Classes and mixins. POPL ’98, Proceedings ofthe 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1998.
ACM. pp. 171–183.
Freeman, T. S. & Pfenning, F. (1991) Refinement types for ML. Proceedings of the ACM
SIGPLAN’91 Conference on Programming Language Design and Implementation (PLDI). ACM.
pp. 268–277.
Goguen, H. (1994) A typed operational semantics for type theory. Ph.D. thesis. University of
Edinburgh, UK.
Goguen, H. (1995) Typed operational semantics. Typed Lambda Calculi and Applications,
Second International Conference on Typed Lambda Calculi and Applications, TLCA ’95, 1995,
Proceedings. Springer. pp. 186–200.
Hall, C. V., Hammond, K., Jones, S. L. P. & Wadler, P. (1996) Type classes in haskell. ACM Trans.
Program. Lang. Syst. 18(2), 109–138.
Harper, R. & Pierce, B. (1991) A record calculus based on symmetric concatenation. Proceedingsof the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New
York, NY, USA. Association for Computing Machinery. pp. 131–142.
Huang, X. & Oliveira, B. C. d. S. (2020) A type-directed operational semantics for a calculus with amerge operator. 34th European Conference on Object-Oriented Programming, ECOOP 2020.
Kaes, S. (1988) Parametric overloading in polymorphic programming languages. ESOP ’88, 2ndEuropean Symposium on Programming, Proceedings. Springer. pp. 131–144.
Kniesel, G. (1999) Type-safe delegation for run-time component adaptation. European Conference
on Object-Oriented Programming (ECOOP).
Knuth, D. E. (1971) Examples of formal semantics. Symposium on Semantics of Algorithmic
Languages. Springer.
Kurata, T. & Takahashi, M. (1995) Decidable properties of intersection type systems. Proceedings of
the Second International Conference on Typed Lambda Calculi and Applications. Springer-Verlag.
p. 297–311.
Laurent, O. (2012) Intersection types with subtyping by means of cut elimination. Fundamenta
Informaticae. 121(1-4), 203–226.
Laurent, O. (2019) Intersection subtyping with constructors. Proceedings Twelfth Workshop on
Developments in Computational Models and Ninth Workshop on Intersection Types and Related
Systems (DCM 2018 and ITRS 2018). pp. 73–84.
Leijen, D. (2004) First-class labels for extensible rows. Technical Report UU-CS-2004-51. Dept. ofComputer Science, Universiteit Utrecht. UTCS Technical Report.
Lieberman, H. (1986) Using prototypical objects to implement shared behavior in object oriented

66

Taming the Merge Operator

systems. Object-Oriented Programming Systems, Languages, and Applications (OOPSLA).
Luo, Z. (1999) Coercive subtyping. J. Log. Comput. 9(1), 105–130.
Microsoft. (2012) TypeScript. https://www.typescriptlang.org/.
Muehlboeck, F. & Tate, R. (2018) Empowering union and intersection types with integrated
subtyping. Proc. ACM Program. Lang. 2(OOPSLA), 112:1–112:29.
Muschevici, R., Potanin, A., Tempero, E. D. & Noble, J. (2008) Multiple dispatch in practice.
Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming,
Systems, Languages, and Applications, OOPSLA 2008, October 19-23, 2008, Nashville, TN,
USA. ACM. pp. 563–582.
Nierstrasz, O., Ducasse, S. & Schärli, N. (2006) Flattening traits. Journal of Object Technology. 5(4),129–148.
Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M.,
Stenman, E. & Zenger, M. (2004) An overview of the Scala programming language. Technicalreport. École Polytechnique Fédérale de Lausanne.
Odersky, M., Wadler, P. & Wehr, M. (1995) A second look at overloading. Proceedings of the seventhinternational conference on Functional programming languages and computer architecture, FPCA
1995. ACM. pp. 135–146.
Oliveira, B. C. d. S., Moors, A. & Odersky, M. (2010) Type classes as objects and implicits.
Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming,
Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe,
Nevada, USA. ACM. pp. 341–360.
Oliveira, B. C. d. S., Shi, Z. & Alpuim, J. (2016) Disjoint intersection types. Proceedings of the 21st
ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan,
September 18-22, 2016. ACM. pp. 364–377.
Ostermann, K. (2002) Dynamically composable collaborations with delegation layers. European
Conference on Object-Oriented Programming (ECOOP).
Palsberg, J. & Zhao, T. (2004) Type inference for record concatenation and subtyping. Inf. Comput.
189(1), 54–86.
Park, G., Hong, J., Jr., G. L. S. & Ryu, S. (2019) Polymorphic symmetric multiple dispatch withvariance. Proc. ACM Program. Lang. 3(POPL), 11:1–11:28.
Pierce, B. & Steffen, M. (1997) Higher-order subtyping. Theoretical Computer Science. 176(1), 235–
282.
Pierce, B. C. (1989) A decision procedure for the subtype relation on intersection types with boundedvariables. Technical report. School of Computer Science, Carnegie-Mellon University.
Pierce, B. C. (1991) Programming with Intersection Types and Bounded Polymorphism. Ph.D. thesis.
Carnegie Mellon University.
Pierce, B. C. & Turner, D. N. (1998) Local type inference. Proceedings of ACM Symposium on
Principles of Programming Languages. pp. 252–265.
Plotkin, G. (1973) Lambda-definability and logical relations.
Poll, E. (1997) System F with width-subtyping and record updating. International Symposium on
Theoretical Aspects of Computer Software. Springer. pp. 439–457.
Pottier, F. (2000) A 3-part type inference engine. European Symposium on Programming. Springer.
pp. 320–335.
Pottinger, G. (1980) A type assignment for the strongly normalizable λ -terms. To HB Curry: essays
on combinatory logic, lambda calculus and formalism. pp. 561–577.
RedHat. (2011) Ceylon. https://ceylon-lang.org/.
Rehof, J. & Urzyczyn, P. (2011) Finite combinatory logic with intersection types. International
Conference on Typed Lambda Calculi and Applications.
Rémy, D. (1989) Type checking records and variants in a natural extension of ml. Proceedings of the
16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 77–88.
Rémy, D. (1995) A case study of typechecking with constrained types: Typing record concatenation.
Presented at the workshop on Advances in types for computer science at the Newton Institute,Cambridge, UK.

Journal of Functional Programming

67

Reynolds, J. C. (1988) Preliminary design of the programming language Forsythe. Technical Report
CMU-CS-88-159. Carnegie Mellon University.
Reynolds, J. C. (1991) The coherence of languages with intersection types. Theoretical Aspects ofComputer Software, International Conference TACS ’91, Sendai, Japan, September 24-27, 1991,
Proceedings. Springer. pp. 675–700.
Reynolds, J. C. (1997) Design of the programming language Forsythe. In ALGOL-like languages.
Springer. pp. 173–233.
Schaefer, I., Bettini, L. & Damiani, F. (2011) Compositional Type-Checking for Delta-oriented
Programming. Proceedings of the tenth international conference on Aspect-oriented softwaredevelopment, AOSD ’11. ACM. pp. 43–56.
Schärli, N., Ducasse, S., Nierstrasz, O. & Black, A. P. (2003) Traits: Composable units of behaviour.
ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Proceedings. Springer.
pp. 248–274.
Siek, J. G. (2019) Transitivity of subtyping for intersection types. CoRR. abs / 1906.09709.
Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. Scheme and Functional
Programming Workshop.
Siek, J. G. & Wadler, P. (2010) Threesomes, with and without blame. Proceedings of the 37th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid,
Spain, January 17-23, 2010. ACM. pp. 365–376.
Statman, R. (1985) Logical relations and the typed λ -calculus. Inf. Control. 65(2/3), 85–97.
Statman, R. (2015) A finite model property for intersection types. Electronic Proceedings in
Theoretical Computer Science. 177, 1–9.
Tait, W. W. (1967) Intensional interpretations of functionals of finite type I. J. Symb. Log. 32(2),198–212.
Ungar, D. & Smith, R. B. (1988) Self: the power of simplicity (object-oriented language). ThirtyThird IEEE Computer Society International Conference, Digest of Papers.
Wadler, P. (1998) The expression problem. Posted on the Java Genericity mailing list.
Wadler, P. & Blott, S. (1989) How to make ad-hoc polymorphism less ad-hoc. Conference Record of
the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas,
USA, January 11-13, 1989. ACM Press. pp. 60–76.
Wadler, P. & Findler, R. B. (2009) Well-typed programs can’t be blamed. Programming Languages
and Systems, 18th European Symposium on Programming, ESOP 2009, York, UK, March 22-29,
2009. Proceedings. Springer. pp. 1–16.
Wand, M. (1989) Type inference for record concatenation and multiple inheritance. Proceedings.
Fourth Annual Symposium on Logic in Computer Science. pp. 92–97.
Wang, Y., Zhang, H., d. S. Oliveira, B. C. & Servetto, M. (2018) FHJ: A formal model for hierarchical dispatching and overriding. 32nd European Conference on Object-Oriented Programming,
ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands.
White, L., Bour, F. & Yallop, J. (2014) Modular implicits. Proceedings ML Family/OCaml Users andDevelopers workshops, ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014. pp. 22–63.
Wright, A. K. & Felleisen, M. (1994) A syntactic approach to type soundness. Inf. Comput. 115(1),38–94.
Xie, N., Oliveira, B. C. d. S., Bi, X. & Schrijvers, T. (2020) Row and bounded polymorphism via
disjoint polymorphism. 34th European Conference on Object-Oriented Programming, ECOOP
2020.
Zwanenburg, J. (1995) Record concatenation with intersection types.
Zwanenburg, J. (1997) A type system for record concatenation and subtyping. Technical report.
Eindhoven University of Technology.