A Type-Directed Operational Semantics
For a Calculus with a Merge Operator
Xuejing Huang
The University of Hong Kong, China
xjhuang@cs.hku.hk

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

Abstract
Calculi with disjoint intersection types and a merge operator provide general mechanisms thatcan subsume various other features. Such calculi can also encode highly dynamic forms of object
composition, which capture common programming patterns in dynamically typed languages (such as
JavaScript) in a fully statically typed manner. Unfortunately, unlike many other foundational calculi(such as System F , System F<: or Featherweight Java), recent calculi with the merge operator lacka (direct) operational semantics with standard and expected properties such as determinism andsubject-reduction. Furthermore the metatheory for such calculi can only account for terminating
programs, which is a significant restriction in practice.
This paper proposes a type-directed operational semantics (TDOS) for λ:i : a calculus withintersection types and a merge operator. The calculus is inspired by two closely related calculi by
Dunfield (2014) and Oliveira et al. (2016). 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 direct semantics for λ:i that has both properties. To fully obtain determinism, theλ:i calculus employs a disjointness restriction proposed in Oliveira et al.’s λi calculus. As an added
benefit the TDOS approach deals with recursion in a straightforward way, unlike λi and subsequentcalculi where recursion is problematic. To further relate λ:i to the calculi by Dunfield and Oliveira etal. we show two results. Firstly, the semantics of λ:i is sound with respect to Dunfield’s small-stepsemantics. Secondly, we show that the type system of λ:i is complete with respect to the λi typesystem. All results have been fully formalized in the Coq theorem prover.
2012 ACM Subject Classification Theory of computation → Type theory; Software and its engineering → Object oriented languages; Software and its engineering → Polymorphism
Keywords and phrases operational semantics, type systems, intersection types
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2020.26
Supplementary Material ECOOP 2020 Artifact Evaluation approved artifact available athttps://doi.org/10.4230/DARTS.6.2.9.
https://github.com/XSnow/ECOOP2020
Funding This work has been sponsored by Hong Kong Research Grant Council projects number
17210617 and 17209519.
Acknowledgements We thank the anonymous reviewers for their helpful comments.

1

Introduction

The merge operator was firstly introduced by Reynolds in the Forsythe language [43] over 30
years ago. It has since been studied, refined and used in some language designs by multiple
researchers [2, 5, 9, 20, 23, 39]. At its essence the merge operator allows creating values that
can have multiple types (encoded as intersection types [18, 41]). For example, with the merge
operator, the following program is valid:
let x : Int & Bool = 1 , , True in (x + 1, not x)
Artifact* Easy to
ed
R
nt

alu

*

se
eu

* onsistO
EC O C P ** Complete

*

t
en

*
A EC E* Well Docume v

at e d© Xuejing Huang and Bruno C. d. S. Oliveira;licensed under Creative Commons License CC-BY
34th European Conference on Object-Oriented Programming (ECOOP 2020).
Editors: Robert Hirschfeld and Tobias Pape; Article No. 26; pp. 26:1–26:32
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

26:2

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

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 theexpression (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 workon intersection types has focused on refinement intersections [21, 24, 28], which only increase
the expressive power of types. In systems with refinement intersections, types can simply
be erased during compilation. However, in those systems the intersection type Int & Bool isinvalid since Int and Bool are not refinements of each other. In other systems, including many
OO languages with intersection types [25, 34, 36, 42], the type Int & Bool has no inhabitants
and the simple program above is inexpressible. The merge operator adds expressiveness toterms and allows constructing values that inhabit the intersection type Int & Bool.
There are various practical applications for the merge operator. One benefit, as Dunfield [23] argues, is that the merge operator and intersection types provide “general mechanismsthat subsume many different features”. This is important because often a new type system
feature involves extending the metatheory and implementation, which can be non-trivial. If
instead we provide general mechanisms that can encode such features, then adding new features will become a lot easier. Dunfield has illustrated this point by showing that multi-fieldrecords, overloading and forms of dynamic typing can all be easily encoded in the presenceof the merge operator. More recently, the merge operator has been used in calculi withdisjoint intersection types [2, 5, 20] to encode several non-trivial object-oriented features,
which enable highly dynamic forms of object composition not available in current mainstream
languages such as Scala or Java. These include first-class traits [4], dynamic mixins [2],and forms of family polymorphism [5]. These features allow, for instance, capturing widelyused and expressive techniques for object composition used by JavaScript programmers (andprogrammers in other dynamically typed languages), but in a completely statically type-safemanner [2,4]. For example, in the SEDEL language [4], 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(super : Trait[Person], idNumber : Int) : Trait[Student] =trait inherits super ⇒ { // 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 they can be constructed dynamically (at run-time). In the program above
inheritance is encoded as a merge in the core language with disjoint intersection types usedby SEDEL.
Despite over 30 years of research, the semantics of the merge operator has proved to bequite elusive. Because of its foundational importance, we would expect a simple and clear
direct semantics to exist for calculi with a merge operator. After all, this is what we get forother foundational calculi such as the simply typed lambda calculus, System F , System Fω , thecalculus of constructions, System F<: , Featherweight Java and others. All these calculi havea simple and elegant direct operational semantics (often presented in a small-step style [55]).
While for the merge operator there have been efforts in the past to define a direct operationalsemantics, these efforts have placed severe limitations that disallow many of the applications
previously discussed or they lacked important properties. Reynolds [44] was the first to lookat this problem, but in his calculus the merge operator is severely limited (for instance a
merge of two functions is not possible). Castagna [9] studied another calculus, where only
merges of functions are possible. Pierce [39] was the first to briefly consider a calculus with

X. Huang and B. C. d. S. Oliveira

26:3

an unrestricted merge operator (called glue in his own work). He discussed an extension toF∧ with a merge operator but he did not study the dynamic semantics with the extension.
Finally, Dunfield [23] 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 the merge
operator indirectly by elaboration to another calculus. This elaboration semantics is type-safeand 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 important drawbacks. Firstly, reasoning about the elaboration semantics
is much more complex: to understand the semantics of programs with the merge operator
we have to understand the translation and semantics of the target calculus. This complicates
informal and formal reasoning. Secondly, a fundamental property in an elaboration semantics
is coherence [44] (which ensures that the meaning of a program is not ambiguous). Allexisting calculi with disjoint intersection types prove coherence, but this currently comes at
a high price: the calculi and proof techniques employed to prove coherence can only deal
with terminating programs. A severe limitation in practice!
This paper presents a type-directed operational semantics (TDOS) for λ:i : a calculus withintersection types and a merge operator [43]. λ:i is inspired by closely related calculi by
Dunfield [23] and Oliveira et al. (λi ) [20], but addresses two key difficulties in the dynamic
semantics of calculi with a merge operator. The first one is the type-dependent nature of themerge operator. This difficulty is addressed by using types in the TDOS to guide reduction,
which is crucial to prove subject-reduction. The second difficulty is that a fully unrestricted
merge operator is inherently ambiguous. For instance the merge 1, , 2 can evaluate to both 1
and 2. Therefore some restriction is still necessary for a deterministic semantics. To fully
obtain determinism, the λ:i calculus uses the disjointness restriction that is employed in λi andseveral other calculi using disjoint intersection types, and two important new notions: typed
reduction and consistency. Typed reduction is a reduction relation that can further reducevalues under a certain type. In other words, type annotations influence operational behavior:
two programs that differ only in type annotations may behave differently. Consistency is anequivalence relation on values, that is key for the determinism result. Determinism in TDOS
offers the same guarantee that 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 subsequentcalculi where recursion is very problematic for proving coherence.
To further relate λ:i to the calculi by Dunfield and Oliveira et al. we show two results.
Firstly, we show that the type system of λ:i is complete with respect to the type system of λi .
Secondly, the semantics of λ:i is sound with respect to Dunfield’s semantics. In our work we
use two variants of λ:i : one that follows Dunfield’s original formulation of subtyping, andanother with a more powerful subtyping relation inspired by Bi et al. [5]. The more powerfulsubtyping relation enables λ:i to account for merges of functions in a natural way, which
was awkward in λi . For the variant with the extension we also require a minor extension to
Dunfield’s operational semantics. The two variants of the λ:i calculus and its metatheory
have been fully formalized in the Coq theorem prover.
In summary, the contributions of this paper are:
The λ:i calculus and its TDOS: We present a TDOS for λ:i : a calculus with intersection
types and a merge operator. The semantics of λ:i is both deterministic and it has subjectreduction.

ECOOP 2020

26:4

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Support for non-terminating programs: Our new proof methods can deal withrecursion, unlike the proof methods used in previous calculi with disjoint intersection
types [5, 6], 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.
Relation with other calculus with intersection types: We relate λ:i with the calculi
proposed by Dunfield and Oliveira et al (λi ). In short all programs that are accepted in
λi can type-check with our type system, and the semantics of λ:i is sound with respect to
Dunfield’s semantics.
Coq formalization: All the results presented in this paper have been formalized in the
Coq theorem prover and they are available in the supplementary material.

2

Overview

This section gives an overview of the type-directed operational semantics for λ:i . We firstprovide some background about the applications of the merge operator. Then we introduce
Dunfield’s untyped semantics [23], and identify its problems: the non-determinism of thesemantics and the lack of subject-reduction. Dunfield’s semantics is nonetheless used to
guide the design of our own TDOS. We show how the TDOS of λ:i uses type annotations toguide reduction, thus obtaining a deterministic semantics that also has the subject-reduction
property.

2.1

First-Class Traits: An Application of the Merge Operator

To give an idea of the kinds of applications for calculi with a merge operator, we briefly present
one existing application: typed first-class traits [4]. Traits [46] in object-oriented programming
provide a model of multiple inheritance. Both traits and mixins [27] encapsulate a collectionof related methods to be added to a class. When composing multiple traits/mixins, conflicts
are dealt differently. Mixins use the order of composition to determine which implementation
to pick. Traits require programmers to explicitly resolve the conflicts instead, and rejectcompositions with conflicts. Merges with disjoint intersection types are closely related totraits because merges with conflicts are also rejected.
Here we borrow an example from the SEDEL language [4] to demostrate how it encodes(typed) first-class traits and dynamic inheritance via the merge operator.
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..."};In SEDEL traits are elaborated into a core calculus with disjoint intersection types and amerge operator. A trait can be viewed as a function taking a self argument and producing
a record. In this example, the record, which contains three fields, is encoded as a mergeof three single field records. Because all the fields have distinct field names, the merge isdisjoint and the definition is accepted. Similarly to a JavaScript class, in the trait editor, thedoCut method calls the onKey method via the self reference and it is dynamically dispatched.
What is more, traits in SEDEL have a self type annotation which is similar to Scala [36]. In
this example, the type of the self reference is the intersection of two record types Editor andX. Huang and B. C. d. S. Oliveira

26:5

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 of self must be satisfied when later composing editor withother traits, i.e. an implementation of the method version should be provided.
The interesting features in SEDEL are that traits are first-class and inheritance can be
dynamic. The following example illustrates such features:type Spelling = {check : String};
spell_mixin (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"}

The above function takes a trait as an argument, and returns a trait as a result. The
argument base is a trait of type Trait[Editor & Version, Editor], where the two types denotetrait requirements and functionality respectively. The trait editor has type Trait[Editor& Version, Editor], since it requires Editor & Version and only provides those method
specified by Editor. Therefore, editor can be used as an argument for spell_mixin. Notethat unlike mainstream OOP languages like Java, the inherited trait (which would correspondto a superclass in Java) is parametrized, thus enabling dynamic inheritance. In SEDEL thechoice of the inherited trait (i.e. the superclass) can happen at run-time, unlike in languages
with static inheritance (such as Java or Scala). Finally, also note the use of the keyword
override to override on_key. Without such keyword the definition of spell_mixin would be
rejected due to a conflict (or a violation of disjointness), since base already provides animplementation of on_key. For a more detailed description of SEDEL and first-class traits
we refer the reader to the work by Bi et al. [4].

2.2Background: Dunfield’s Non-Deterministic Semantics

Dunfield studied the semantics of a calculus with intersection types and a merge operator.
The interesting aspect of her calculus is the merge operator, which 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 andas a term of type B. Intersection types and the merge operator in Dunfield’s calculus are
similar to pair types and pairs. Indeed, a program written with pairs that behaves identicallyto the program shown in Section 1 is:
let x : (Int, Bool) = (1, True) in ( fst x + 1, not (snd x) )However while for pairs both the introductions and eliminations are explicit, with the merge
operator the eliminations (i.e. projections) are implicit and driven by the types of the terms.
Dunfield exploits this similarity to give a type-directed elaboration semantics to her calculus.
The elaboration transforms merges into pairs, intersection types into pair types 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). Most
expressions are standard, except the merges (E1 , , E2 ). The calculus also includes a canonical
top value >, and allows variables to be values. Note that the original Dunfield’s calculus
uses a different notation for intersection types (A ∧ B), and supports union types (A ∨ B).

ECOOP 2020

26:6

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

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

T ype
Expr
V alueE

E0(Operational semantics of Dunfield’s calculus)
DStep-appl

DStep-appr

E1

E10

E1 E2

E10 E2DStep-fix

fix x. EE[x 7→ fix x. E]

E2

E20

V1 E2

V1 E20DStep-beta(λx. E) V

E[x 7→ V ]DStep-mergel

DStep-merger

E1

E2

E1 , , E2E10E10 , , E2

V 1 , , E2

E20

V1 , , E20

DStep-unmergel

DStep-unmerger

DStep-split

E 1 , , E2

E1 , , E2

E

E1

E2

E ,, E

Figure 1 The syntax and non-deterministic small-step semantics of Dunfield’s calculus.

Union types are not supported by λ:i , since it is based on the λi calculus [20] with disjoint
intersection types, which does not have unions either. For a better comparison, we adjust
the syntax and omit union types in Dunfield’s system.
Operational Semantics. The bottom part of Figure 1 presents the reduction rules. Theinteresting construct is the merge operator, as all other 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: a merge of two expressions (which do not even need to be twovalues) can step to its left subexpression (by rule DStep-unmergel) or the right one (byrule DStep-unmerger). Any expressions can split into two by rule DStep-split. Therefore,
even though the reduction rules may have already reached a value form, it is still possible tostep further using rule DStep-split.
Problem 1: No Subject-Reduction. A major problem of this operational semantics is thatit does not preserve types. Note that reduction is oblivious of types, so a term can reduce totwo other terms with potentially different (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 (using rule DStepunmergel) or the boolean (using rule DStep-unmerger). In Dunfield’s calculus the term
1 , , True can have multiple types, including Int or Bool or even Int & Bool. As a consequence,the semantics is not type-preserving in general.
What is worse, a well-typed expression can reduce to an expression that is ill-typed:(1 , , λx. x + 1) 2

12This reduction leads to an ill-typed term (with any type) because we drop the lambda insteadof the 1 in the merge.

X. Huang and B. C. d. S. Oliveira

26:7

Problem 2: Non-determinism. Even in the case of type-preserving reductions there canbe another problem. Because of the pair of unmerge rules (rule DStep-unmergel andrule DStep-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 DStep-split):
1,, 2(1 , , 2) , , (1 , , 2)

In other words the semantics is non-deterministic.
Note that Dunfield’s operational semantics is an overapproximation of the intended
behavior. In her work, it is used to provide a soundness result for her elaboration semantics,
which is type-safe (but still ambiguous).

2.3

A Type-Driven Semantics for Type Preservation

An essential problem is that the semantics cannot ignore the types if the reduction is meant
to be type-preserving. Dunfield notes that “For type preservation to hold, the operationalsemantics would need access to the typing derivation” [23]. 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 tocreate valid λ:i terms as we will see in Section 5. We discuss the main challenges and key
ideas of the design of λ:i next.
Type-driven Reduction. Our operational semantics follows a standard call-by-value smallstep reduction and it is closely related to Dunfield’s semantics. However, type annotations
play an important role in the reduction rules and are used to guide reduction. For example, in
λ:i we can write explicitly annotated expressions such as (1 , , True) : Int and (1 , , True) : Bool.
For those expressions the following reductions are valid:(1 , , True) : Int ,→ 1

(1 , , True) : Bool ,→ True

In contrast the following reductions are not possible:(1 , , True) : Bool ,→ 1(1 , , True) : Int ,→ TrueNote also that in λ:i the meaning of expression 1 , , True without any type annotation can
only be a corresponding value 1 , , True that does not drop any information.
Typed Reduction. The crucial component in the operational semantics that enables the useof type information during reduction is an auxiliary typed reduction relation v ,→A v 0 that isused when we want some value to match a type. Typed reduction is where type informationfrom annotations in λ:i “filters” reductions that are invalid due to a type mismatch. Typed
reduction takes a value and a type (which can be viewed as inputs), and gives a unique valueof that type as output. Note that this process may result in further reduction of the value,
unlike many other languages where values can never be further reduced. Typed reduction isused in two places during reduction:
ECOOP 2020

26:8

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Step-annov

Step-beta

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

v ,→A v 0

v ,→A v 0

The first place where typed reduction is used is in rule Step-annov. When reduction
encounters a value with a type annotation A it uses typed reduction to do further reduction
depending on the type A. To see typed reduction in action, consider a simple merge ofprimitive values such as 1 , , True , , ‘c’ with an annotation Int & Char. Using rule Step-annov
typed reduction is invoked, resulting in:
1 , , True , , ‘c’ ,→Int & Char 1 , , ‘c’We could have type-reduced the same value under a similar type but where the two types in
the intersection are interchanged:
1 , , True , , ‘c’ ,→Char & Int ‘c’ , , 1
Both typed reductions are valid and they illustrate the ability of typed reduction to create avalue that matches exactly with the shape of the type.
The second place where typed reduction is used is in rule Step-beta. In a function
application, the actual argument could be a merge containing more components than what
the function expects. One example is (λx. x + 1 : Int → Int) (1 , , True). Since the merge
term (1 , , True) provides an integer 1, the redundant components (the True in this case)are useless, and sometimes even harmful. Consider a function λx. (x , , False) with type
Int → Int & Bool, applied to (1 , , True). If we performed direct substitution of the argumentin the lambda body, this would result in 1 , , True , , False. This brings ambiguity, and theterm is not well-typed, as we shall see in Section 2.5. Therefore, before substitution, thevalue must be further reduced with typed reduction under the expected type of the function
argument. Thus the value that is substituted in the lambda body is 1 (but not 1 , , True),and the final result is 1 , , False.
These examples show some non-trivial aspects of typed reduction, which must decompose
values, and possibly drop some of the components and permute other components. The
details of the typed reduction relation will be discussed in Section 4. As we shall see functions
introduce further complications.

2.4

The Challenges of Functions

One of the hardest challenges in designing the semantics of λ:i was the design of the rules forfunctions. We discuss the challenges next.
Return Types Matter. As we have seen above, the input type annotation of lambdas isnecessary during beta reduction. However, it is not enough to distinguish among multiple
functions in a merge (e.g. (λx. x + 1) , , (λx. True)) without run-time type checking. Unlike
primitive values, whose types can be told by their forms, for functions, we need the type of thefunction (including the output type) to select the right function from a merge. Therefore, in
λ:i all functions are annotated with both the input and output types. With such annotations
we can deal with programs such as:((λf.f 1) : (Int → Int) → Int) ((λx. x + 1) : Int → Int , , (λx. True) : Int → Bool)X. Huang and B. C. d. S. Oliveira

26:9

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.
To select the right function from the merge, the types of the functions are used to guide thereduction of the merge. This avoids the need for run-time type-checking, which would beotherwise necessary to recover the full type of functions.
Annotation Refinement. Given a value, for any of its supertypes, typed reduction gives
a result. Since functions are values, sometimes this leads to the refinement of the type
annotation of lambdas. Following the convention introduced by previous works [20], → haslower precedence than &, which means A → B & C equals to A → (B & C). Consider a single
function λx. x , , True : Int → Int & Bool to be reduced under type Int & Bool → Int. To let
the function 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
expected input type of the function and helps to adjust the input value before substitution
in beta reduction. 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 bethought as an integer and can be safely merged with another boolean, for example. In short,the actual λ:i reduction is:((λx. x , , True) : Int → Int & Bool) : Int & Bool → Int,→ (λx. x , , True) : Int → Int

2.5

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
proposed by Oliveira et al. [20] and the novel notion of consistency. Both disjointness andconsistency play a fundamental role in the proof of determinism.
Disjointness. Two types are disjoint (written as A ∗ B), if any common supertypes thatthey have are top-like types (i.e. supertypes of any type; written as eCd).
I Definition 1 (Disjoint Types).
A ∗ B ≡ ∀C, if A <: C and B <: C then eCd
Intuitively, 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
with any types [2]. Since every value of a top-like type has the same effect, typed reduction
unifies them to a fixed result. Thus the disjointness checking in the following typing ruleguarantees that e1 and e2 can be merged safely, without any ambiguities. For example, thistyping rule does not accept 1 , , 2 or True , , 1 , , False, as two subterms of the merge haveoverlapped types (in this case, the same type Int and Bool, respectively).
Γ ` e1 : AΓ ` e2 : BΓ ` e1 , , e2 : A & B

A∗B
Etyp-merge

ECOOP 2020

26:10A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Consistency. Recall the split rule (rule DStep-split) in Dunfield’s semantics: E
E , , E.
It duplicates terms in a merge. Similar things can happen in our typed reduction if the typehas overlapping parts, which is allowed, for example, in an expression 1 : Int & Int. Notethat in 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, , 1
Note that the disjointness restriction does not allow sub-expressions in a merge to have thesame type: 1 , , 1 cannot type-check with rule Etyp-merge. To obtain type preservation,
there is a special (run-time) typing rule for merges of values, where a novel consistency checkis used (written as v1 ≈ v2 ):· ` v1 : A· ` v2 : BΓ ` v1 , , v2 : A & B

v 1 ≈ v2
Etyp-mergev

Mainly, consistency allows values to have overlapped parts as far as they are syntacticallyequal. For example, 1 , , True and 1 , , ‘c’ are consistent, since the overlapped part Int in bothof merges is 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 have disjoint types, they must be consistent. For merges of suchvalues, both rule Etyp-mergev and rule Etyp-merge can be applied, and the types always
coincide. In λ:i , consistency is defined in terms of typed reduction:
I Definition 2 (Consistency). Two values v1 and v2 are said to be consistent (written v1 ≈ v2 )if, for any type A, the result of typed reduction for the two values is the same.
v1 ≈ v2 ≡ ∀ A, if v1 ,→A v10 and v2 ,→A v20 then v10 = v20
Although the specification of consistency is decidable and an equivalent algorithmic definition
exists, it is not required. In practice, in a programming language implementation, therule Etyp-mergev may be omitted, since, as stated, its main purpose is to ensure that
run-time values are type-preserving.
Finally, note that λi [20] is stricter than λ: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. The idea of allowing unrestricted intersections, while only having the
disjointness restriction for merges, was first employed in the NeColus calculus [5]. λ: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, unrestricted intersections
can be used to encode bounded quantification [8], whereas with disjoint intersections only
such an encoding does not work [6].

3The λ:i Calculus: Syntax, Subtyping and Typing

This section presents the syntax, subtyping, and typing of λ:i : a calculus with intersection
types and a merge operator. This calculus is a small variant of the λi calculus [20] (whichitself is inspired by Dunfield’s calculus [23]) extended with annotated expressions, explicit
subsumption and fixpoints. The explicit type annotations and subtyping are necessary forthe type-directed operational semantics of λ:i and to preserve determinism. The addition of
fixpoints illustrates the ability of TDOS to deal with non-terminating programs, which arestill not supported by calculi that rely on elaboration and semantic coherence proofs [5, 6].

X. Huang and B. C. d. S. Oliveira

3.1

26:11

SyntaxThe syntax of λ:i is:
T ype
Expr
V alueContext

A, B ::= Int | Top | A → B | A & B
e ::= x | i | > | e : A | e1 e2 | λx.e : A → B | e1 , , e2 | fix x.e : Av ::= 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 andthe 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 and Contexts. The meta-variable v ranges over values. Values include integers, thecanonical > value, lambda abstractions and merges of values. Typing contexts are standard.
Γ tracks the bound variables x with their type A.

3.2

Subtyping and Disjointness

The subtyping rules of the form A <: B are shown on the top of Figure 2. These subtyping
rules, except for rule S-toparr, were first introduced by Davies and Pfenning [21], and areused in λi as well. The original subtyping relation is known to be reflexive and transitive [21].
We proved the reflexivity and transitivity of the extended subtyping relation as well. Thereare 3 rules regarding intersection types. Together they define A & B as the greatest lower
bound of A and B.
Top-like Types and Arrow Types. Intuitively, a top-like type is both a supertype and asubtype of Top, including the Top type and intersections of top-like types. The newly added
rule S-toparr enlarges top-like types to include arrow types when their return types are
top-like. A simple unary relation that captures top-like types inductively is defined on thebottom of Figure 2. The following theorem states the correctness and completeness of thedefinition.
I Lemma 3 (Soundness and Completeness of the Definition of Top-like Types).
eAd if and only if Top <: A
Rule S-toparr is inspired by the following rule in BCD-style subtyping [3] (and adopted by
Bi et al. [5]):Top <: Top → Top

BCD-toparr

ECOOP 2020

26:12A Type-Directed Operational Semantics for a Calculus with a Merge Operator

A <: B(Subtyping)
S-arr

S-z

S-top

Int <: Int

A <: Top

S-andr

B1 <: A1

S-toparr

A2 <: B2

A1 <: A2

A1 → A2 <: B1 → B2
S-andl1

A1 <: A3A1 <: A2 & A3
S-andl2

Top <: B2

A1 <: A3A2 <: A3

A <: B1 → B2

A1 & A2 <: A3

A1 & A2 <: A3

eAd(Top-like types)
TL-andeAd

eBd

eA & Bd

TL-topeTopd

TL-arreBdeA → Bd

Figure 2 Subtyping rules of λ:i and definition of top-like types.

Since BCD-style subtyping includes a transitivity rule as an axiom, with this rule, Int → Top
and Int → (Top → Top) are supertypes (and also subtypes) of Top. Due to the lack of
built-in transitivity rule in λ:i ’s subtyping, the above consequence has to be expressed more
explicitly in the adapted rule S-toparr. We will come back to our motivation for including
rule S-toparr in Section 3.3.
Disjointness. In Section 2.5, the specification of disjointness is presented. Such specification
is a slightly more liberal version of the definition originally used in λi . In particular in our
definition A and B themselves can be top-like types, which was forbidden in λi . An equivalentalgorithmic definition of disjointness (A ∗a B) is presented in Appendix A, which is the sameas the definition in the NeColus calculus [5].
I Lemma 4 (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.

3.3

Typing

The expression typing judgment Γ ` e : A is standard. It says that in the typing environment
Γ the expression e is of type A. Unlike λi , there is no well-formedness restriction on
types1 . This generalization is inspired by the calculus NeColus [5], where the well-formedness
constraints are removed from λi , and expressions like 1 : Int & Int are allowed. In other words
the calculus supports unrestricted intersections as well as disjoint intersection types (which
are the only kind of intersections supported in λi ).
The type system, shown in Figure 3, is syntax-directed. Most typing rules directly follow
the declarative type system of λi , including the merge rule Etyp-merge, where disjointness
is used. When two expressions have disjoint types, any parts from each of them do nothave overlapping types. Therefore, their merge does not introduce ambiguity. With this1

The wellformedness and typing rules for λi can be found in Section 5.2.

X. Huang and B. C. d. S. Oliveira

26:13

Γ`e:A

(Typing)Etyp-top

Etyp-litΓ ` > : TopΓ ` i : Int

Etyp-var

Etyp-anno

x:A ∈ Γ

Γ`e:B

Γ`x:A

Etyp-abs

B <: AΓ ` (e : A) : A
Etyp-appΓ, x : A ` e : B
C <: AB <: DΓ ` (λx. e : A → D) : C → D

Γ, x : A ` e : AΓ ` e1 : A → BΓ ` e2 : AΓ ` (fix x. e : A) : AΓ ` e1 e2 : B

Etyp-fix

Etyp-merge

Etyp-mergev

Γ ` e1 : AΓ ` e2 : B
A∗B· ` v1 : A· ` v2 : B
v1 ≈ v2Γ ` e1 , , e2 : A & BΓ ` v1 , , v2 : A & B

Figure 3 Type system of λ:i .

restriction, rule Etyp-merge does not accept expressions like 1, , 2 or even 1, , 1. On theother hand, the novel rule Etyp-mergev allows consistent values to be merged regardless of
their types. It accepts 1 , , 1 while still rejecting 1, , 2. It is for values only, and values areclosed. Therefore the type judgments appearing in it as premises should have empty context,
which is denoted by ·. Together the two rules support the determinism and type preservationof the TDOS, as discussed in Section 2.5.
Top-Like Types and Merges of Functions. We can finally come back to the motivation to
include rule S-toparr in subtyping and depart from both Dunfield calculus and λi , which do
not have such a rule. Without the rule S-toparr in subtyping, no arrow types are top-like,therefore two arrow types A → B and C → D are never disjoint in terms of Definition 1, as
they have a common supertype A & C → Top. Consequently, we can never 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 λi an ad-hoc solution is proposed, by forcing the matterand employing the syntactic definition of top-like types in Figure 2 in disjointness. However
this means that in λi Lemma 3 is false, since top-like function types are not supertypes ofTop. In contrast, the approach we take in λ:i is to add the rule S-toparr in subtyping. Now
Top <: (A & C → Top) is derivable and thus A & C → Top is genuinely a top-like type. Inturn this makes merges of multiple functions typeable without losing the intuition behind
top-like types.
Type-Checking for Lambda Abstractions. Rule Etyp-abs can be thought as a combinationof the standard typing rule and the subsumption rule. A well-typed lambda abstraction canhave multiple types with the same return type. Its type annotation indicates the principal
input type and the return type. Thus the input type can be any subtype of the principal
one, since arrow types are contravariant in their argument types. While the principal input
type describes the lambda’s expectation on its argument, the annotated return type ensures
the type of the evaluated result of lambdas. It just needs to be a supertype of the inner
expression of the lambda. Rule Etyp-abs is inspired by the “distributed” use of subsumption
in the λ& calculus [9].
ECOOP 2020

26:14

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Explicit Subsumption. Unlike many calculi where there is a general subsumption rule that
can apply anywhere, in λ:i subsumption needs to be explicitly triggered by a type annotation(except for lambdas, as explained above). The annotation rule Etyp-anno acts as explicit
subsumption and assigns 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 alone isinsufficient to prevent some ambiguous terms, as shown in the following example.
Subsumption
Etyp-merge
Subsumption· ` 1 : Int
Int <: Top· ` 1 : Top· ` 2 : Int
Top ∗ Int· ` 1 , , 2 : Top & Int· ` 1 , , 2 : Int & Int

Top & Int <: 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 Etyp-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. Finally, the use of an
explicit subsumption rule is a simpler alternative to bidirectional type-systems employed inother calculi with disjoint intersection types. Bidirectional type-checking is also capable ofcontrolling subsumption, but adds more complexity.
Principal Types. The principal type of a value is the most specific one among all of its
types, i.e. it is the subtype of any other type of the term. Its definition is syntax-directed.
I Definition 5 (Principal types). typep hvi calculates the principal type of value v.
typep h>i = Top
typep hni = Inttypep hλx. e : A → Bi = A → B
typep hv1 , , v2 i = typep hv1 i & typep hv2 i
I Lemma 6 (Principal Types). For any value v, if its principal type is A, then
1. if · ` v : B then A <: B.
2. if · ` v : B and B ∗ C then A ∗ C.
3. · ` v : A.

4

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 tosay, there is only one way to reduce an expression according to the small-step relation, andthe process preserves types and never gets stuck.

X. Huang and B. C. d. S. Oliveira

26:15

v ,→A v 0

(Typed reduction)

TReduce-lit

TReduce-top

i ,→Int i

v ,→Top >TReduce-toparr

eBdv ,→A→B λx. > : Top → B

TReduce-arrow¬eDd
C <: AB <: D
λx. e : A → B ,→C→D λx. e : A → D
TReduce-mergevl

v1 ,→A v10

TReduce-andv ,→A v1

v ,→B v2

v ,→A & B v1 , , v2
TReduce-mergevr

A ordinary

v1 , , v2 ,→A v10v2 ,→A v20

A ordinary

v1 , , v2 ,→A v20

Figure 4 Typed reduction of λ:i .

4.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 v 0
reduces the value v under type A, producing a value v 0 that has type A. It arises when givena value v of some type, where A is a supertype of the type of v, and v needs to be converted
to a value compatible with the supertype A. The typed reduction ensures that values andtypes have a strong correspondence. If a value is well-typed, its principal type can be told
directly by looking at its syntactic form.
Figure 4 shows the typed reduction relation. Rule TReduce-top expresses the factthat Top is the supertype of any type, which means that any value can be reduced undertype Top. Similarly, rule TReduce-toparr indicates that any value reduces to a lambda
abstraction λx. > : Top → B under a top-like arrow type A → B. Although it is not the
only inhabited value of type A → B, the reduction result has to be fixed for determinism.
Rule TReduce-lit expresses that an integer value reduced under the supertype Int is justthe integer value itself. Rule TReduce-arrow states that a lambda value λx. e : A → B,
under a non-top-like type C → D, evaluates to λx. e : A → D if C <: A and B <: D. The
restriction that C → D is not top-like avoids overlapping with rule TReduce-toparr.
Importantly rule TReduce-arrow changes the return type of lambda abstractions. For
example:(λx. x , , 2 : Char → Char & Int) ,→(Char & Int→Char) λx. x , , 2 : Char → CharIntersections and Merges. In the remaining rules, we first decompose intersections. Then
we only need to consider types that are not intersections, which are called ordinary types [21]:A ordinary(Ordinary types)
O-top

O-int

O-arrow

Top ordinary

Int ordinary

A → B ordinary

ECOOP 2020

26:16

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

We take care of the value by going through every merge, until both value and types are in abasic form. Rule TReduce-mergevl and rule TReduce-mergevr are a pair of rules for
reducing merges under an ordinary type. Since the type is not an intersection, the resultcontains no merge. Usually, we need to select between the left part and right part of amerge according to the type. The values of disjoint types do not overlap on non-top-liketypes. For example, 1 , , (λx. x : Int → Int) ,→Int 1 selects the left part. For top-like types,
no matter which rule is applied, the reduction result is determined by the type only, as
rule TReduce-top and rule TReduce-toparr suggest.
Rule TReduce-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 rulemay duplicate values. For example 1 ,→Int & Int 1 , , 1. Such duplication requires special care,since the merge violates disjointness. The specially designed typing rule (rule Etyp-mergev)
uses the notion of consistency (discussed in Section 4.2) instead of disjointness to type-checka merge of two values. Note also that such duplication implies that sometimes it is possible
to use either rule TReduce-mergevl or rule TReduce-mergevr to reduce a value. For
example, 1 , , 1 ,→Int 1. The consistency restriction (Definition 2) in rule Etyp-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 TReduce-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
typed reduced by some type, its principal type must be a subtype of that type.
I Lemma 7 (Typed reduction on top-like types). If eAd, v1 ,→A v10 , and v2 ,→A v20 thenv10 = v20 .
When typed reduction is under a top-like type, the result only depends on the type.
I Lemma 8 (Transitivity of typed reduction). If v ,→A v1 , and v1 ,→B v2 , then v ,→B v2 .
Typed reduction produces the same result whenever it is done directly or indirectly.
I Lemma 9 (Typed reduction respects subtyping). If v ,→A v 0 , then typep hvi <: A.
This lemma relates typed reduction and subtyping. It states that if a well-typed value canbe typed reduced by type A, its principal type must be a subtype of A.

X. Huang and B. C. d. S. Oliveira

4.2

26:17

Consistency and Type Soundness of Typed Reduction

Consistent values, as specified in Definition 2, introduce no ambiguity in typed reduction.
Consider one type, if two consistent values both can reduce under the type, they should
produce the same result. The consistency restriction ensures that duplicated values in amerge type-check, but it still rejects merges with different values of the same type. A valueof a top-like type is consistent with any other value. It only type reduces under top-liketypes, which leads to a fixed result decided by the type.
Relating Disjointness and Consistency. Assuming that two values have disjoint types,
according to Lemma 6, their principal types must be disjoint as well. From Lemma 9, we canconclude that when the two values both reduce under a type, that type must be a common
supertype of their principal types, which is known to be top-like (Definition 1). Furthermore,
Lemma 7 implies that their reduction results are always the same under such top-like types,
so they are consistent (Definition 2).
I Lemma 10 (Consistency of disjoint values). If A ∗ B, · ` v1 : A, and · ` v2 : B then v1 ≈ v2 .
Determinism and Type Soundness of Typed Reduction. The merge construct makes it
hard to design a deterministic operational semantics. Disjointness and consistency restrictions
prevent merges 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 10). When the two typed reduction rules for merges (rule TReduce-mergevl andrule TReduce-mergevr) overlap, no matter which one is chosen, either value reduces tothe same result due to consistency (Definition 2). Indeed our typed reduction relation always
produces a unique result for any legal combination of the input value and type. This serves
as a foundation for the determinism of the operational semantics.
I Lemma 11 (Determinism of Typed Reduction). For every well-typed v (that is there is some
type B such that · ` v : B), if v ,→A v1 and v ,→A v2 then v1 = v2 .
Via the transitivity lemma (Lemma 8) and the above determinism lemma, we obtain thefollowing property: any reduction results of the given value are consistent.
I Lemma 12 (Consistency after Typed Reduction). If v is well-typed , and v ,→A v1 , andv ,→B v2 then v1 ≈ v2 .
The lemma shows that the reduction result of rule TReduce-and is always made of consistentvalues, which is needed in type preservation via the typing rule Etyp-mergev. Then a(generalized) type preservation lemma on typed reduction can be proved.
I Lemma 13 (Preservation of Typed reduction). If · ` v : B and v ,→A v 0 then · ` v 0 : A.
In the particular case where A = B, this lemma shows that typed reduction preserves types.
However, more generally, it shows that if a value is well-typed under a type B and it can be
type reduced under another type A then the reduced value is always well-typed at type A.
Finally, the typed reduction progress lemma is:
I Lemma 14 (Progress of Typed Reduction). If · ` v : A, and A <: B, then ∃v 0 , v ,→B v 0 .

ECOOP 2020

26:18A Type-Directed Operational Semantics for a Calculus with a Merge Operator

e ,→ e0(Reduction)

Step-appl

Step-appr

e1 e2 ,→ e01 e2

v1 e2 ,→ v1 e02

e1 ,→ e01

Step-fix

e2 ,→ e02

fix x. e : A ,→ e[x 7→ fix x. e : A]

Step-mergel

Step-merger

Step-anno

e1 , , e2 ,→ e01 , , e2v1 , , e2 ,→ v1 , , e02

e : A ,→ e0 : A

e1 ,→ e01

Step-beta

e2 ,→ e02

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

e ,→ e0

Step-annov

v ,→A v 0

v : A ,→ v 0

Figure 5 Call-by-value reduction of λ:i .

4.3

Reduction

The reduction rules are presented in Figure 5. Most of them are standard. Rule Step-beta
and rule Step-annov are the two rules relying on typed reduction judgments. Rule Stepbeta says that a lambda value λx. e : A → B applied to value v reduces by replacing thebound variable x in e by v 0 . Importantly v 0 is obtained by type reducing v under type
A. In other words, in rule Step-beta further (typed) reduction may be necessary on theargument depending on its type. This is unlike many other calculi where values are in a final
form and no further reduction is needed (thus the value v can be directly substituted). The
rule Step-annov says that an annotated v : A can be reduced to v 0 if v type reduces to v 0
under type A.
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 torule Step-annov and rule Step-beta.
I Theorem 15 (Determinism of ,→). If · ` e : A, e ,→ e1 , e ,→ e2 , then e1 = e2 .
I Theorem 16 (Type Preservation of ,→). If · ` e : A, and e ,→ e0 then · ` e0 : A.
I Theorem 17 (Progress of ,→). If · ` e : A, then e is a value or ∃e0 , e ,→ e0 .

5Relationship to Dunfield’s Calculus and λi

Dunfield’s calculus [23] and λi [20] are two calculi that directly inspired λ:i . In this section,
we discuss the relationship between λ:i and them. First, we show that λ:i ’s TDOS and aslightly extended version of Dunfield’s non-deterministic operational semantics are related.
The need for extending Dunfield’s original semantics is mostly due to the addition of therule S-toparr in subtyping, which Dunfield does not have. In Section 6 we also discuss avariant of λ:i (which does not include rule S-toparr) and show that such variant requires

X. Huang and B. C. d. S. Oliveira

|i |
|>|
| λx. e : A → B || fix x. e : A ||e : A|| e1 e2 || e1 , , e2 |

26:19

=
=
=
=
=
=
=

i
>
λx. | e |fix x. | e ||e|| e1 | | e2 || e1 | , , | e2 |Figure 6 Type erasure for λ:i expressions.

no changes to Dunfield’s original semantics. The other relationship is between λ:i ’s typesystem and λi ’s type system. The former comparison shows the soundness of the operationalsemantics of λ:i with respect to Dunfield’s semantics. The latter one proves that λ:i ’s typesystem is at least as expressive as, if not stronger than, λi ’s.
Type Erasure. Differently from the other two systems, λ: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 system and λi . The only
exception is fixpoints, which λi does not have. The annotation erasure function is defined in
Figure 6. Note that for every value v in λ:i , | v | is a value as well.

5.1

Soundness with respect to Dunfield’s Operational Semantics

Dunfield’s original reduction rules are presented in Fig 1. We extend her operational semantics
with the following two rules. The full reduction rules can be found in the appendix.
E

E0(The extension of Dunfield’s calculus)
DStep-topE>

DStep-toparr

>

λx. >

Rule DStep-top states that any value can be reduced to >, corresponding to A <: Top.
Rule DStep-toparr says that the value > can be reduced to a lambda which returns>, suggested by the subtyping rule S-toparr. Together with merge rules, the extended
reduction can reduce any term to a value under a top-like type. Dunfield avoids having arule DStep-top by performing a simplifying elaboration step advance:Γ ` V : Top ,→ >Dunfield-Typing-T

With such a rule, values of type Top are directly translated into >, and do not need any
further reduction in the target language. Accordingly, in her source language, there is no rule
to convert these values to >. We do not have such an elaboration step and we have already
added rule DStep-toparr, so instead, we extend the original semantics with the two rules.
Soundness. Given Dunfield’s extended semantics, we can show a theorem that each step in
the TDOS of λi corresponds to zero, one, or multiple steps in Dunfield’s semantics.
I Theorem 18 (Soundness of ,→ with respect to Dunfield’s semantics). If e ,→ e0 , then| e | ∗ | e0 |.

ECOOP 2020

26:20A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Γ |= A(Type wellformedness)
Wf-andWf-topWf-intΓ |= TopΓ |= Int

Wf-arrΓ |= A

Γ |= B

Γ |= A → B

Γ |= A
Γ |= BA ∗i B
Γ |= A & B

Γ |= E : A(Typing)
ITyp-lam

ITyp-topΓ |= > : Top

ITyp-litΓ |= i : Int

x:A ∈ ΓΓ |= AΓ, x : A |= E : B

Γ |= x : A

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

ITyp-varITyp-app

ITyp-merge

Γ |= E1 : A → B
Γ |= E2 : A

Γ |= E1 : A
Γ |= E2 : B
A ∗i B

Γ |= E1 E2 : B

Γ |= E1 , , E2 : A & B

ITyp-subΓ |= E : A

AlBΓ |= E : B

Figure 7 The declarative type system of λi .

A necessary lemma for this theorem is the soundness of typed reduction.
I Lemma 19 (Soundness of Typed Reduction with respect to Dunfield’s semantics). If v ,→A v 0 ,then | v | ∗ | v 0 |.
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 TReduce-mergevl (or rule TReduce-mergevr),
corresponding to rule DStep-unmergel (or rule DStep-unmerger). And rule TReduceand (v ,→A & B v1 , , v2 if v ,→A v1 and v ,→B v2 ) can be understood as a combination of
spliting (rule DStep-split V
V , , V ) and further reduction on each component separately.
In Section 6, we present another variant of λ:i , which has the same subtyping relation
as Dunfield’s system (minus union types). The same soundness theorem is proved for thatvariant without any modifications to Dunfield’s operational semantics.

5.2

Completeness with respect to the Type System of λi

λi drops union types and introduces the disjointness restriction to Dunfield’s system. Whenintroducing λi , Oliveira et al. proposed an algorithmic and a declarative type system. The
two type systems were shown to be equally expressive. For the declarative type system there
is still the possibility of ambiguity due to the presence of an (implicit) subsumption rule (seealso the discussion in Section 3.3). However, annotations in the bidirectional algorithmic
type system ensure that well-typed terms in λi are unambiguous and subsumption is kept
under control.
The type system of λ:i is based on the declarative type system of λi , with three mainchanges:X. Huang and B. C. d. S. Oliveira

26:21

1. λ:i forces the subsumption rule to be explicitly triggered by a type annotation.
2. λ:i supports fixpoints while λi does not.
3. λ:i has an additional rule for the merge of values (rule Etyp-mergev), which is required
to prove type preservation, since duplicated values can occur in merges after reduction.
Some details need to be explained before presenting the completeness theorem. Firstly,
because they are irrelevant, rules related to products and projection operators in λi aredropped. Secondly, the subtyping in λ:i is stronger due to the added rule S-toparr. Thirdly,
top-like types are disjoint with any type in λ:i , while the disjointness in λi is restricted to
types which are not top-like. The definition of λi ’s subtyping and disjointness can be foundin the appendix.
I Theorem 20 (Completeness of Typing with respect to λi ). If Γ |= E : A, then there exists
some e such that Γ ` e : A and E = | e |.
The above theorem shows that the type system of λ:i is able to type check any well-typed
terms in λi , with proper type annotations inserted based on the typing derivation. It is built
on the completeness of subtyping and disjointness of λ:i . The result means that λi ’s typesystem (or any type system equivalent to it) can be used as a surface language where manyof the explicit annotations of λ:i are inferred automatically. That is to say, the λi calculus
can be translated without loss of expressivity or flexibility into λ:i .
To further show that some type inference with recursion is feasible, we extended thebi-directional type system of λi with recursion, and replaced the subtyping and disjointnessby λ:i ’s. We designed an elaboration from the extended system to λ:i and proved the following
theorem. The typing rules can be found in the appendix.
I Theorem 21 (Completeness of Typing with respect to the Extended Bidirectional Type Systemof λi ). If Γ ` E ⇒ A ,→ e or Γ ` E ⇐ A ,→ e, then Γ ` e : A.

6

Discussion

This section discusses one variant of λ:i , which is also formalized in Coq. The variant follows
the subtyping relation in λi and Dunfield’s calculus strictly and does not support multiple
functions in merges. Some possible extensions to our work are also discussed.

6.1

A Variant of λ:i

In Section 5.1, we validate the TDOS of λ:i via a soundness theorem (Theorem 18) withrespect to an extended operational semantics of Dunfield’s calculus. In this section, we
discuss a variant of λ:i that requires no extension to Dunfield’s operational semantics. Its
syntax and typing rules can be found in the appendix. Instead of adding rule S-toparr,this variant keeps the same subtyping relation as Dunfield’s and adapts the definition of
top-like types and disjointness, losing the ability to have multiple functions in a merge.
Consequently, it is possible to prove the following soundness theorem on this variant without
any modifications on Dunfield’s operational semantics2 .
I Theorem 22 (Soundness of ,→ in the simple variant). If e ,→ e0 , then | e |∗| e0 |.

The above theorem states that each step taken by the TDOS corresponds to a series of
reduction in the original operational semantics of Dunfield’s calculus.

2

For the syntax and rules of Dunfield’s system, please refer to Section 2.

ECOOP 2020

26:22A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Besides soundness, this variant keeps the other important properties of λi : determinism,type preservation and progress. A completeness theorem with respect to the type system of
λi is established as well.
I Theorem 23 (Completeness of Typing in the simple variant). If Γ |= E : A in λi , then there
exists some e such that Γ ` e : A in the variant and E = | e |.
Designing the Variant. As presented in Section 5.1, there are two reduction rules in
λ:i that are related to the extension of Dunfield’s operational semantics: rule TReduce-top(v ,→Top >) and rule TReduce-toparr. They reduce values under top-like types into a
unified form. Without rule S-toparr, no arrow types are top-like, thus the latter is removed
from the variant. However there is still rule TReduce-top, which is not accounted for in
Dunfield’s original system. While we believe that such a rule fits in spirit well with theremaining non-deterministic rules, it is interesting to see if it is possible to model a calculus
without it (and without extending Dunfield semantics at all).
Reducing a value v under type Top, in fact, can be thought as seeking an inhabited valueof Top which acts like v. In Dunfield’s original semantics there is no way to convert a value
to >, which is our source of difficulties. Dunfield solves this problem by having a typing rule
for values that allows any value to have type Top. This works well in her setting because she
can have ambiguous terms. Unfortunately, it does not work well in our setting because, as
discussed in detail in Section 3.3, allowing values to be implicitly typed as Top provides away to bypass the disjointness restrictions. We overcome the problem instead by introducing
a new value construct v : Top in our variant. This new form of value inhabits the Top typebut, unlike > it does not forget about the original value v (which can be of any type). Thus
the original value v, can be recovered by erasing the wrapped annotation.
TRed-top

v ,→Top v : Top
Although the new rule then corresponds to v
v after annotation erasure, it breaks
determinism as a merge can reduce to either its left or right component, leading to different
results, e.g. 1, , True ,→Top 1 : Top and 1, , True ,→Top True : Top. To solve this problem we
directly reduce the value before splitting merges by excluding Top from ordinary types.
To use the new construct for expressions and mix it with annotated terms, values andexpressions are separated into two syntactic categories in the variant (but all values canbe treated as expressions hvi). The partition results in some tedious rules in the reduction
relation. For instance, hv1 i , , hv2 i ,→ hv1 , , v2 i reduces a merge of two values to a merged
value.

6.2

Improvements and Extensions

Less Checks on Reduction. In rule TReduce-arrow (in Figure 4), the premise C <: A is
actually redundant for the purposes of reduction. Since we only care about well-typed terms
being reduced, such a 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 another role 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 principal type of the reduced value and the reduction type. (See Lemma 9: If v ,→A v 0 ,then typep hvi <: A). One could wonder if this property is unnecessary because it may be

X. Huang and B. C. d. S. Oliveira

26:23

derived by type preservation of reduction. Note that whenever typed reduction is called ina 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 typep hvi <: 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. In future work we would like to look at thisissue more closely and try to discard the premise by taking full advantage of the type system.
Distributive Subtyping. Although the subtyping of λ:i allows multiple functions in a merge,
it lacks the distributive subtyping rule for intersection types that has been employed in somerecent calculi [5, 6]. The distributivity of intersections over arrows ((A → B1 ) & (A → B2 ) <:A → B1 & B2 ) [3] is well accepted for its theoretical elegance. But it is also well-known forbeing troublesome. Mainly, there are two challenges for adapting distributive subtyping to
λ:i .
The rule indicates that a merge of functions can be applied. While the current typing
rule can check such application with suitable annotations, designing new reduction rules
is necessary. A promising solution is to have a rule allows parallel application like
(v1 , , v2 ) v ,→ v1 v , , v2 v.
Function types are no longer “ordinary”. In λ:i , the intuition behind ordinary types is that
their typed reduction results never contains merges, which is necessary for determinism.
With distributivity, typed reduction may produce a merge under a single function type.
For example, λx. ‘c’ : Int → Char , , λx. x : Int → Int ,→Int→Char & Int λx. ‘c’ : Int →Char , , λx. x : Int → Int. In the typed reduction of λ:i , intersections are split into basic
units. However, it is not straightforward to split a function type.

7

Related Work

7.1

Calculi with the Merge Operator and a Direct Semantics

Intersection types with a merge operator are a key feature of Reynolds’ Forsythe language [43].
Reynolds studied a core calculus [43] with similarities to λ:i . However, merges in Forsythe
are restricted and use a syntactic criterion to determine what merges 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 merge always biased. To prevent potential ambiguity, thelatter overrides the former when overlapped. Note that the structure of merge in Forsythe isalways biased. If formalized as a tree, 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-namesmall-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 admits this issue in his later
work [45]. In λ:i types are used 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 the value is used or not.
The calculus λ& proposed by Castagna et al. [9] has a restricted version of the merge
operator for functions only. The merge operator is indexed by a list of types of its components.
The operational semantics uses the run-time types of values to select the “best approximate”
branch of an overloaded function. λ& requires run-time type checking on values, while

ECOOP 2020

26:24

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

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

NeColus [5] Fi+ [6]Dunfield’s[23]

λi [20]Fi [2]

No

Coh.

Coh.

Coh.

Coh.

-

-

-

-

Figure 8 Summary of intersection calculi with the merge operator ( = yes,applicable).

λ:i

Det.

= no, - = notin TDOS, all type information is present already in type annotations. Another obvious
difference is that λ:i supports merges of any types (not just functions), which are useful for
applications other than overloading of functions, including: multifield extensible records with
subtyping [20]; encodings of objects and traits [4]; dynamic mixins [2]; or simple forms offamily polymorphism [5].
Several other calculi with intersection types and overloading of functions have been
proposed [10–12], but these calculi do not support a merge operator, and thus avoid theambiguity problems caused by the construct.

7.2

Calculi with a Merge Operator and an Elaboration Semantics

Instead of a direct semantics, many recent works [2, 5, 6, 20, 23] on intersection types employ
an elaboration semantics, translating merges in the source language to products (or pairs) ina target language. With an elaboration semantics the subtyping derivations are coercive [33]:they produce coercion functions that explicitly convert terms of one type to another in thetarget language. This idea was first proposed by Dunfield [23], where she shows how toelaborate 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 own work. However, her direct semantics is
non-deterministic and lacks subject-reduction (as discussed in detail in Section 2.2). 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 thatare not allowed in Forsythe and λ&.
To remove the ambiguity issues in Dunfield’s work, the λi calculus [20] forbids overlapping
in intersections using the disjointness restriction for all well-formed intersections. In otherwords, λi does not support unrestricted intersections. Because of this restriction, the proof
of coherence in λi is still relatively simple. Likewise, in following work on the Fi calculus [2],which extends λi with 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
type is well-formed then any instantiation of that type is also well-formed. Unfortunately,with disjoint intersections only, this property is not true in general. Thus Fi can only provea 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 [5] relaxes the restriction
without introducing ambiguity. In NeColus 1 : Int & Int is allowed, but the same term is

X. Huang and B. C. d. S. Oliveira

26:25

rejected in λi . In other words, NeColus employs the disjointness restriction only on merges,
but otherwise allows unrestricted intersections. Unfortunately, this comes at a cost: it ismuch harder to prove the coherence of elaboration. Both NeColus and Fi+ [6] (a calculus
derived from Fi that allows unrestricted intersections) deal with this problem by establishingcoherence using contextual equivalence and a logical relation [40,49,50] to prove it. The proof
method, however, cannot deal with non-terminating programs. In fact none of the existing
calculi with disjoint 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 8
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. λ:i is coercion free, while all other calculi basedon an elaboration semantics employ coercive subtyping. Next we give more detail on theadvantages of a direct semantics over the elaboration semantics and proof methods employedin previous 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 semantics we canessentially employ a style similar to equational reasoning in functional programming todirectly reason about programs written in λ:i . For example, it takes a few reasoning steps towork out the result of (λx. x + 1 : Int → Int) (2 , , ‘c’):(λx. x + 1 : Int → Int) (2 , , ‘c’),→ (2 + 1) : Int,→ 3 : Int,→ 3{by Step-beta and typed reduction of argument under Int}{by Step-anno and usual reduction rules for arithmetic}{by Step-annov and typed reduction of 3 under Int}

Here reasoning is easily justifiable from the small-step reduction rules and type-directed
reduction. In fact building tools (such as some form of debugger), that automate such kindof reasoning should be easy using the TDOS rules.
However, with an elaboration semantics, the (precise) reasoning steps to determine thefinal result are much more complex. Firstly the expression has to be translated into thetarget language before reducing to a similar target term. Figure 9 shows this elaboration
process in λi , where an expression in the source language is translated into an expression in atarget 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 together
with the introduction of coercions into the program makes it much 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{by a rule similar to Step-appr and reduction rules for pairs}{by beta reduction rule}{by usual reduction rules for arithmetic}

ECOOP 2020

26:26

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

T-mergeT-ann...
· ` (λx. x + 1 : Int → Int) ⇒ Int → Int
··
··
··

T-app

...
· ` (2 , , ‘c’) ⇒ Int & Char····λx. x + 1
··
··
·

T-sub

· ` (λx. x + 1 : Int → Int) (2 , , ‘c’) ⇒ Int(2 , ‘c’)

Sub-andl
Int & Char <: Int

fst· ` (2 , , ‘c’) ⇐ Int
fst (2 , ‘c’)
(λx. x + 1) (fst (2 , ‘c’))Figure 9 Elaboration of the expression (λx. x + 1 : Int → Int) (2 , , ‘c’) into a target calculus withproducts.

A final issue is that sometimes it is not even possible to translate back the value of the target
language into an equivalent “value” on the source. For instance in the NeColus calculus [5]
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 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 aprogram. Since the main point of semantics is to give clear and simple rules to understand themeaning 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 the coherence. Our λ:i calculus, on the other hand, hasa deterministic 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. To relate themrequires 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 from the
NeColus source calculus. NeColus, forbids terms like (1 , , 2) and thus cannot produce a target
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.

X. Huang and B. C. d. S. Oliveira

26:27

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 [1], but this is left for future work(and it is non-trivial). λ: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.

7.3

Languages and Calculi with Type-Dependent Semantics

Typed Operational Semantics Goguen [29] uses types in its reduction judgment, 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 the
reduction 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 [30], calculi with dependent types [26, 29]
and higher-order subtyping [17]. Note that the semantics of these systems does not dependon typing, and the untyped (type-erased) reduction relations are still presented to describe
how to evaluate programs.
Type classes [32, 52] are an approach to parametric overloading used in languages like
Haskell. The commonly adopted compilation strategy for it is the dictionary passing styleelaboration [13, 14, 31, 52]. Other mechanisms inspired by type classes, such as Scala’s
implicits [19], Agda’s instance arguments [22] or Ocaml’s modular implicits [54] have anelaboration semantics as well. In one of the pioneering works of type classes, Kaes [32] gives
two formulations for a direct operational semantics. One of them decides the concrete type of
the instance of overloaded functions at run-time, by analyzing all arguments after evaluatingthem. In both Kaes’ work and a following work by Odersky et al. [37], the run-time semantics
has some restrictions with respect to type classes. For example, overloading on return types(needed for example for the read function in Haskell) is not supported. Interestingly, thesemantics of λ:i allows overloading on return types, which is used whenever two functions
coexist on a merge.
Gradual typing [47] has become popular over the last few years. Gradual typing is anotherexample 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 (type-dependent) elaboration
semantics into a cast calculus, such as the Blame calculus [53] or the Threesome calculus [48].
Static binding of fields and method overloading in Java [51] make use of type annotations
computed in a preprocessing phase. For each method invocation, the annotation states theargument type of the most specific method applicable according to the static types. Basedon the annotation and the run-time type (class) of the object, a dynamic lookup function
yields a proper method at run-time. This allows static method overloading works across theinheritance hierarchy, together with dynamic dispatch. Multiple dispatching [15, 16, 35, 38]
generalizes object-oriented dynamic dispatch to determine the overloaded method to invoke
based on the run-time type of all its arguments. Similarly 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 the semantics.

ECOOP 2020

26:28A Type-Directed Operational Semantics for a Calculus with a Merge Operator

8

Conclusion

In this work we presented a TDOS for λ:i : a calculus that includes intersection types andan expressive unbiased merge operator. Among all similar calculi, λ:i is the first to have a
direct operational semantics that is both deterministic and has subject-reduction. 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 [5] requires much more sophistication
than obtaining the determinism theorem in λ:i . Furthermore the proof method for coherencein NeColus cannot deal with non-terminating programs, whereas dealing with recursion isstraightforward in λ:i . The semantics of λ:i exploits type annotations to guide reduction.
The key component of TDOS is typed reduction, which allows values to be further reduced
depending on their type. For the future we would like to develop further the TDOS approachin the setting of disjoint intersection types. Some interesting extensions include support for
distributive subtyping [3], disjoint polymorphism [2] and iso-recursive types with the Amber
rule [7].

References1

Amal J. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types.
In Peter Sestoft, editor, Programming Languages and Systems, 15th European Symposiumon Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory
and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings,
volume 3924 of Lecture Notes in Computer Science, pages 69–83. Springer, 2006. doi:
10.1007/11693024_6.

2João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. Disjoint polymorphism. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on
Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory
and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 1–28. Springer, 2017.
doi:10.1007/978-3-662-54434-1_1.

3

Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda modeland the completeness of type assignment 1. The journal of symbolic logic, 48(4), 1983.

4

Xuan Bi and Bruno C. d. S. Oliveira. Typed first-class traits. In Todd D. Millstein, editor,
32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018,
Amsterdam, The Netherlands, volume 109 of LIPIcs, pages 9:1–9:28. Schloss Dagstuhl Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.ECOOP.2018.9.

5Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The essence of nested composition.
In Todd D. Millstein, editor, 32nd European Conference on Object-Oriented Programming,
ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands, volume 109 of LIPIcs, pages
22:1–22:33. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.
ECOOP.2018.22.

6Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. Distributive disjoint
polymorphism for compositional programming. In Luís Caires, editor, Programming Languages
and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of theEuropean Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech
Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science,
pages 381–409. Springer, 2019. doi:10.1007/978-3-030-17184-1_14.

7

Luca Cardelli. Amber. In Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet, editors,
Combinators and Functional Programming Languages, Thirteenth Spring School of the LITP,
Val d’Ajol, France, May 6-10, 1985, Proceedings, volume 242 of Lecture Notes in Computer
Science, pages 21–47. Springer, 1985. doi:10.1007/3-540-17184-3_38.

X. Huang and B. C. d. S. Oliveira

8

Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism.
ACM Comput. Surv., 17(4):471–522, 1985. doi:10.1145/6041.6042.

9

Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded functions
with subtyping. Inf. Comput., 117(1):115–135, 1995. doi:10.1006/inco.1995.1033.

10

Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, and Pietro Abate. Polymorphic functions
with set-theoretic types: Part 2: Local type inference and type reconstruction. In Sriram K.
Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January
15-17, 2015, pages 289–302. ACM, 2015. doi:10.1145/2676726.2676991.

11

Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, and Luca
Padovani. Polymorphic functions with set-theoretic types: part 1: syntax, semantics, andevaluation. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA,
USA, January 20-21, 2014, pages 5–18. ACM, 2014. doi:10.1145/2535838.2535840.

12

Giuseppe Castagna and Zhiwu Xu. Set-theoretic foundation of parametric polymorphismand subtyping. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors,
Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming,
ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 94–106. ACM, 2011. doi:10.1145/
2034773.2034788.

13

Manuel M. T. Chakravarty, Gabriele Keller, and Simon L. Peyton Jones. Associated typesynonyms. In Olivier Danvy and Benjamin C. Pierce, editors, Proceedings of the 10th ACM
SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia,
September 26-28, 2005, pages 241–253. ACM, 2005. doi:10.1145/1086365.1086397.

14

Manuel M. T. Chakravarty, Gabriele Keller, Simon L. Peyton Jones, and Simon Marlow.
Associated types with class. In Jens Palsberg and Martín Abadi, editors, Proceedings ofthe 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 1–13. ACM, 2005.
doi:10.1145/1040305.1040306.

15

Craig Chambers and Weimin Chen. Efficient multiple and predicated dispatching. In Brent
Hailpern, Linda M. Northrop, and A. Michael Berman, editors, Proceedings of the 1999 ACM
SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications(OOPSLA ’99), Denver, Colorado, USA, November 1-5, 1999, pages 238–255. ACM, 1999.
doi:10.1145/320384.320407.

16

Curtis Clifton, Gary T. Leavens, Craig Chambers, and Todd D. Millstein. Multijava: modular
open classes and symmetric multiple dispatch for java. In Mary Beth Rosson and Doug Lea,
editors, Proceedings of the 2000 ACM SIGPLAN Conference on Object-Oriented Programming
Systems, Languages & Applications (OOPSLA 2000), Minneapolis, Minnesota, USA, October
15-19, 2000, pages 130–145. ACM, 2000. doi:10.1145/353171.353181.

17

Adriana B. Compagnoni and Healfdene Goguen. Typed operational semantics for higher-ordersubtyping. Inf. Comput., 184(2):242–297, 2003. doi:10.1016/S0890-5401(03)00062-2.

18

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters ofsolvable terms. Math. Log. Q., 27(2-6):45–58, 1981. doi:10.1002/malq.19810270205.

19

Bruno C. d. S. Oliveira, Adriaan Moors, and Martin Odersky. Type classes as objects andimplicits. In William R. Cook, Siobhán Clarke, and Martin C. Rinard, editors, Proceedingsof the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems,
Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada,USA, pages 341–360. ACM, 2010. doi:10.1145/1869459.1869489.

20

Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. Disjoint intersection types. In Jacques
Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN
International Conference on Functional Programming, ICFP 2016, Nara, Japan, September
18-22, 2016, pages 364–377. ACM, 2016. doi:10.1145/2951913.2951945.

26:29

ECOOP 2020

26:30A Type-Directed Operational Semantics for a Calculus with a Merge Operator

21

Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Martin
Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21,
2000, pages 198–208. ACM, 2000. doi:10.1145/351240.351259.

22

Dominique Devriese and Frank Piessens. On the bright side of type classes: instance arguments
in agda. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceedingof the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011,
Tokyo, Japan, September 19-21, 2011, pages 143–155. ACM, 2011. doi:10.1145/2034773.
2034796.

23

Jana Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133–165,
2014. doi:10.1017/S0956796813000270.

24

Jana Dunfield and Frank Pfenning. Type assignment for intersections and unions in callby-value languages. In Andrew D. Gordon, editor, Foundations of Software Science andComputational Structures, 6th International Conference, FOSSACS 2003 Held as Part of
the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw,
Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science,
pages 250–266. Springer, 2003. doi:10.1007/3-540-36576-1_16.

25

Facebook. Flow. https://flow.org/, 2014.

26

Yangyue Feng and Zhaohui Luo. Typed operational semantics for dependent record types. In
Tom Hirschowitz, editor, Proceedings Types for Proofs and Programs, Revised Selected Papers,
TYPES 2009, Aussois, France, 12-15th May 2009, volume 53 of EPTCS, pages 30–46, 2009.
doi:10.4204/EPTCS.53.3.

27

Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In
David B. MacQueen and Luca Cardelli, editors, POPL ’98, Proceedings of the 25th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, CA,
USA, January 19-21, 1998, pages 171–183. ACM, 1998. doi:10.1145/268946.268961.

28

Timothy S. Freeman and Frank Pfenning. Refinement types for ML. In David S. Wise, editor,
Proceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and
Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, pages 268–277. ACM,
1991. doi:10.1145/113445.113468.

29

Healfdene Goguen. A typed operational semantics for type theory. PhD thesis, University of
Edinburgh, UK, 1994. URL: http://hdl.handle.net/1842/405.

30

Healfdene Goguen. Typed operational semantics. In Mariangiola Dezani-Ciancaglini and
Gordon D. Plotkin, editors, Typed Lambda Calculi and Applications, Second International
Conference on Typed Lambda Calculi and Applications, TLCA ’95, Edinburgh, UK, April
10-12, 1995, Proceedings, volume 902 of Lecture Notes in Computer Science, pages 186–200.
Springer, 1995. doi:10.1007/BFb0014053.

31

Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip Wadler. Type classes inhaskell. ACM Trans. Program. Lang. Syst., 18(2):109–138, 1996. doi:10.1145/227699.227700.

32

Stefan Kaes. Parametric overloading in polymorphic programming languages. In Harald
Ganzinger, editor, ESOP ’88, 2nd European Symposium on Programming, Nancy, France,
March 21-24, 1988, Proceedings, volume 300 of Lecture Notes in Computer Science, pages
131–144. Springer, 1988. doi:10.1007/3-540-19027-9_9.

33

Zhaohui Luo. Coercive subtyping. J. Log. Comput., 9(1):105–130, 1999. doi:10.1093/logcom/
9.1.105.

34

Microsoft. Typescript. https://www.typescriptlang.org/, 2012.

35

Radu Muschevici, Alex Potanin, Ewan D. Tempero, and James Noble. Multiple dispatch inpractice. In Gail E. Harris, editor, 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, pages 563–582. ACM, 2008. doi:10.1145/1449764.
1449808.

X. Huang and B. C. d. S. Oliveira

36

37

38

39
40
41
42
43
44

45
46

47
48

49
50
51

52

53

26:31

Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane
Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. An
overview of the scala programming language. Technical report, École Polytechnique Fédérale
de Lausanne, 2004.
Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In John
Williams, editor, Proceedings of the seventh international conference on Functional programming
languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28,
1995, pages 135–146. ACM, 1995. doi:10.1145/224164.224195.
Gyunghee Park, Jaemin Hong, Guy L. Steele Jr., and Sukyoung Ryu. Polymorphic symmetricmultiple dispatch with variance. Proc. ACM Program. Lang., 3(POPL):11:1–11:28, 2019.
doi:10.1145/3290324.
Benjamin C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD
thesis, Carnegie Mellon University, December 1991.
Gordon Plotkin. Lambda-definability and logical relations, 1973.
Garrel Pottinger. A type assignment for the strongly normalizable λ-terms. To HB Curry:
essays on combinatory logic, lambda calculus and formalism, pages 561–577, 1980.
Redhat. Ceylon. https://ceylon-lang.org/, 2011.
John C Reynolds. Preliminary design of the programming language Forsythe. Technical
Report CMU-CS-88-159, Carnegie Mellon University, 1988.
John C. Reynolds. The coherence of languages with intersection types. In Takayasu Ito andAlbert R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference
TACS ’91, Sendai, Japan, September 24-27, 1991, Proceedings, volume 526 of Lecture Notes in
Computer Science, pages 675–700. Springer, 1991. doi:10.1007/3-540-54415-1_70.
John C Reynolds. Design of the programming language Forsythe. In ALGOL-like languages,
pages 173–233. Springer, 1997.
Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P. Black. Traits: Composable units of behaviour. In Luca Cardelli, editor, ECOOP 2003 - Object-Oriented Programming, 17th European Conference, Darmstadt, Germany, July 21-25, 2003, Proceedings, volume 2743 of Lecture Notes in Computer Science, pages 248–274. Springer, 2003.
doi:10.1007/978-3-540-45070-2_12.
Jeremy G Siek and Walid Taha. Gradual typing for functional languages. In Scheme andFunctional Programming Workshop, 2006.
Jeremy G. Siek and Philip Wadler. Threesomes, with and without blame. In Manuel V.
Hermenegildo and Jens Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January
17-23, 2010, pages 365–376. ACM, 2010. doi:10.1145/1706299.1706342.
Richard Statman. Logical relations and the typed λ-calculus. Inf. Control., 65(2/3):85–97,
1985. doi:10.1016/S0019-9958(85)80001-2.
William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log.,
32(2):198–212, 1967. doi:10.2307/2271658.
David von Oheimb and Tobias Nipkow. Machine-checking the java specification: Proving typesafety. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java, volume 1523 of Lecture
Notes in Computer Science, pages 119–156. Springer, 1999. doi:10.1007/3-540-48737-9_4.
Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad-hoc. In
Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages, Austin, Texas, USA, January 11-13, 1989, pages 60–76. ACM Press, 1989. doi:
10.1145/75277.75283.
Philip Wadler and Robert Bruce Findler. Well-typed programs can’t be blamed. In Giuseppe
Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practiceof Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture
Notes in Computer Science, pages 1–16. Springer, 2009. doi:10.1007/978-3-642-00590-9_1.

ECOOP 2020

26:32A Type-Directed Operational Semantics for a Calculus with a Merge Operator

54

55

Leo White, Frédéric Bour, and Jeremy Yallop. Modular implicits. In Oleg Kiselyov andJacques Garrigue, editors, Proceedings ML Family/OCaml Users and Developers workshops,
ML/OCaml 2014, Gothenburg, Sweden, September 4-5, 2014, volume 198 of EPTCS, pages
22–63, 2014. doi:10.4204/EPTCS.198.2.
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf.
Comput., 115(1):38–94, 1994. doi:10.1006/inco.1994.1093.