Resolution as Intersection Subtyping via Modus Ponens
KOAR MARNTIROSIAN and TOM SCHRIJVERS, KU Leuven, Belgium
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, Hong Kong
GEORGIOS KARACHALIAS, Tweag, Paris
Resolution and subtyping are two common mechanisms in programming languages. Resolution is used byfeatures such as type classes or Scala-style implicits to synthesize values automatically from contextual
type information. Subtyping is commonly used to automatically convert the type of a value into anothercompatible type. So far the two mechanisms have been considered independently of each other. This paper
shows that, with a small extension, subtyping with intersection types can subsume resolution. This has
three main consequences. Firstly, resolution does not need to be implemented as a separate mechanism.
Secondly, the interaction between resolution and subtyping becomes apparent. Finally, the integration ofresolution into subtyping enables first-class (implicit) environments. The extension that recovers the power ofresolution via subtyping is the modus ponens rule of propositional logic. While it is easily added to declarative
subtyping, significant care needs to be taken to retain desirable properties, such as transitivity and decidabilityof algorithmic subtyping, and coherence. To materialize these ideas we develop λiMP , a calculus that extends a
previous calculus with disjoint intersection types, and develop its metatheory in the Coq theorem prover.
CCS Concepts: • Software and its engineering → Functional languages; Object oriented languages;
Semantics.
Additional Key Words and Phrases: resolution, nested composition, family polymorphism, intersection types,
coherence, modus ponens
ACM Reference Format:
Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias. 2020. Resolution as
Intersection Subtyping via Modus Ponens. Proc. ACM Program. Lang. 4, OOPSLA, Article 206 (November 2020),
30 pages. https://doi.org/10.1145/3428274

1

INTRODUCTION

Subtyping is a well-known programming language feature. It is most notably employed in objectoriented languages, but there are many other uses of subtyping in the literature [Barendregt
et al. 1983; Chen 2003; Gay and Hole 2005; Pierce and Sangiorgi 1996]. Subtyping automaticallyconverts the type of a value into another compatible type. One particular form of subtyping arises
from intersection types [Barendregt et al. 1983; Reynolds 1991]. Intersection types support—among
others—a form of finitary overloading [Castagna et al. 1992]. For example, in various systems withintersection types, it is possible to build overloaded functions such as:
f : (Int -> Int) & (Char -> Char) = succ ,, toUpper
Authors’ addresses: Koar Marntirosian, mardikoh15@gmail.com; Tom Schrijvers, KU Leuven, Leuven, Belgium; Bruno C. d. S.
Oliveira, bruno@cs.hku.hk, The University of Hong Kong, Hong Kong; Georgios Karachalias, georgios.karachalias@tweag.io,
Tweag, Paris.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2020 Copyright held by the owner/author(s).
2475-1421/2020/11-ART206
https://doi.org/10.1145/3428274

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206

206:2

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

The merge operator (,,) allows the function f to behave as both the succ and the toUpper functions.
Thus, f can be applied both to an integer and to a character. When applied to an integer, f behaves
like the successor function, whereas when applied to a character f capitalizes its input. The
automatic selection of the appropriate behavior (from the overloaded definition f) is based on thetype of the input, which triggers an upcast induced by the subtyping relation. For instance, in thecase of the application f 3, the input of the function must be Int and therefore, the following
upcast is triggered in such an application:(Int -> Int) & (Char -> Char) <: Int -> Int
Resolution is another programming language mechanism. Haskell type classes [Wadler and Blott1989] employ resolution to automatically search for and compose instances of type classes. Resolutionis also used by Scala’s implicits [Oliveira et al. 2010]. Many other programming languages havemechanisms similar to type classes and implicits [Devriese and Piessens 2011; Sozeau and Oury
2008a; White et al. 2015], and consequently employ a form of resolution. Type classes and implicits
can also be used to define overloaded functions. For example, in Haskell, we may define:class Over a where f :: a -> ainstance Over Int where f = succ
instance Over Char where f = toUpper
This achieves an overloaded behavior similar to the intersection types version of f. Indeed, theHaskell version of f can also be applied both to an integer and to a character with similar results.
However, in Haskell, the selection of the right function in the application f 3 uses resolution. In
Haskell (and languages with implicits) there is an implicit environment that stores information abouttype class instances. When class methods are used, resolution searches the implicit environment tofind the right instance or to combine existing instances to find a suitable method implementation.
The function f illustrates the similarities and overlapping use cases for subtyping and resolution.
However there are also various use cases that are not in common. On the one hand, with subtyping
we can, for instance, have Int -> Int <: Int -> Top. Such a conversion is typically notallowed by resolution mechanisms documented in the literature [Hall et al. 1996; Odersky et al.
2017; Oliveira et al. 2012; Schrijvers et al. 2019; Wadler and Blott 1989]. On the other hand, a key
feature of resolution is its ability to compose instances (or implicits). For instance, suppose that wewant an overloaded version of f for lists of integers. With type classes we can define the instance:
instance Over Int => Over [Int] where
f []
= []
f (x : xs) = f x : f xs
Note that here the context Over Int is not necessary in Haskell, but for illustration purposes, we
add the redundant context. With this instance, if we call f [1,2,3], then the result is [2,3,4].
For this to work, resolution needs to find an instance for Over [Int]. While no instance directly
matches the required type, resolution composes the instance for lists with the instance for integers
to build an instance of the appropriate type. The ability to perform such compositions is lacking in
traditional mechanisms with subtyping and intersection types.
This paper shows that, with a small extension, subtyping with intersection types can in factsubsume forms of resolution. The extension that is necessary to recover the power of resolution
via subtyping is essentially the logical rule for modus ponens:
A⊢B →CA⊢B
Modus Ponens

A⊢C

Modus ponens states that if from A one can conclude both B → C and B then one can also conclude
C. The key idea in this paper is that we can adapt modus ponens to subtyping, and thus enable its
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:3

power (and the essential power of resolution). To accomplish this, we simply reinterpret entailment(A ⊢ B) as subtyping (A <: B). Modus ponens captures the essence of composition that is necessary
to enable the following derivation:(Int -> Int) & ((Int -> Int) -> [Int] -> [Int]) <: [Int] -> [Int]which could be used in a language with intersection types and subtyping, to find an overloaded
implementation of f in a call such as f [1,2,3] (just like the version with type classes).
While modus ponens is easy to add in a declarative version of subtyping, significant care needs tobe taken to retain desirable properties, such as transitivity and decidability of subtyping. Our workbuilds and extends upon the NeColus calculus [Bi et al. 2018]—or λi+ —which has both transitivity
and decidability of subtyping, as well as coherence of the elaboration semantics. However, NeColus
does not support modus ponens. Extending the proofs of transitivity, decidability and coherence of
NeColus to support modus ponens is highly non-trivial. The key difficulty is that modus ponens
makes the context in which a type appears relevant for resolution (which is not the case in NeColus).
Adding modus ponens to subtyping, and viewing resolution as a special case of subtyping, comeswith important advantages. Firstly, resolution does not need to be implemented as a completely
separate mechanism. This can make implementations as well as metatheory more compact, because
the two mechanisms are generalized into a single relation. Secondly, the interaction between
resolution and subtyping becomes apparent, which contrasts with the current state-of-the-art where
it is ignored.1 Indeed, various foundational calculi related to Scala formalize either subtyping [Aminet al. 2016, 2012] or implicits [Odersky et al. 2017; Oliveira et al. 2012; Schrijvers et al. 2019], but
usually not both. The only exception is the recent work by Jeffery [2019], which studies a calculus
with both features (but where resolution and subtyping are modeled independently). Finally, theintegration of resolution into subtyping enables first-class (implicit) environments. That is, we cancreate (implicit) environments (encoded as intersection types), use them as arguments, or returnthem from functions. This is impossible in existing approaches for type classes and calculi with
implicits, as there is no explicit notion of a type for environments.
To materialize these ideas we develop λiMP : a calculus that extends the NeColus calculus (acalculus with disjoint intersection types [Oliveira et al. 2016]) and develop its metatheory in the
Coq theorem prover. In summary, the contributions of this work are:
• Resolution as subtyping: We extend subtyping of intersection types with modus ponens.
This enables composing components from intersections to solve subtyping problems, and(together with other standard intersection rules) subsumes forms of resolution.
• The λiMP calculus: We develop a concrete calculus that illustrates the idea of subtyping as
resolution. The calculus is an extension of NeColus [Bi et al. 2018]. We prove several basic
properties, including type-safety, which is proved via an elaboration into the target language
λMP
c , a simply typed lambda calculus extended with coercions.
• Algorithmic subtyping for λiMP : We incorporate modus ponens in the NeColus subtyping
algorithm by (1) restructuring it in two mutually recursive judgments—one of which builds
coercions by accumulating them in a continuation-passing form—and (2) adding a loop
detector for termination. Our Coq proofs show that our algorithm subsumes that of NeColus,
and is sound, complete and terminating; this establishes that the subtyping of λiMP is decidable.
The proofs of termination and transitivity, which is used to show completeness, are both
highly non-trivial. The former uses different arguments for three different kinds of loops,
including reasoning about the effectiveness of loop detection. The latter consists of 7 mutually
1 For example, GHC issue ticket 17295 is a closely related problem, caused by an unexpected interaction between resolution

and overlapping “intersections”.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:4

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

recursive lemmas with complex interdependencies. To establish the well-foundness of their
proof we employ the AProVE tool [Giesl et al. 2017].
• Conditional Coherence for λiMP : Establishing coherence of λiMP is also a challenging
technical goal. The addition of modus ponens makes it a lot harder due to the ability tocompose information. We formulate a non-trivial extension of the canonicity relation of
NeColus, based on which we build a mechanized partial coherence proof in the Coq theorem
prover.
The supplementary material contains a Coq mechanization of the definitions (4k lines) and theorems(5.6k lines) in this paper, as well as a prototype implementation in Haskell (~820 lines).
An extended version of this paper, containing appendices, can be found online, by following thislink: https://arxiv.org/abs/2010.06216.
2

BACKGROUNDThis section introduces background on resolution, coercive subtyping, intersection types and theiruse in programming languages.
2.1

Coercive Subtyping, Resolution and their Computational Interpretation

This paper brings together two different programming language features: (implicit) resolution as
used in Haskell type classes and Scala implicits on the one hand, and type-directed coercive subtyping
on the other hand. While these two features are very different on the surface, they are in fact both
based on similar computational interpretations of logical inference. The different rules of logicalinference they use are compatible. In this paper we show how to extend this compatibility to thelanguage design level and how to ensure properties that, while typically of no concern for logicalinference, are key for programming languages, like coherence and decidable type checking.
In the sequent notation, the judgment A ⊢ B asserts that proposition B can be inferred fromproposition A. An inference rule provides a way to construct a valid (or true) judgment. For instance,
the inference ruleA⊢A
states that the judgment A ⊢ A (from A follows A) is valid for any proposition A.
The A ⊢ B judgment can be given a computational interpretation following the “propositions as
types” approach [Wadler 2015]. This means that we take the types of a programming language as
the possible propositions. The judgment A ⊢ B then means that there exists a computable functionthat turns values of type A into values of type B. We call this function the (computational) evidence
for the judgment. The evidence for a judgment follows from the inference rules that have beenused to establish that judgment. For instance, the evidence for the trivial A ⊢ A judgment above isthe identity function λx .x. A more advanced inference rule is that for transitivity
A⊢B
B ⊢C
A⊢C
which allows to conclude C from A provided that B can be concluded from A and C from B. Givenevidence f for B ⊢ C and evidence д for A ⊢ B, the evidence for A ⊢ C is λx .д (f x).
Coercive Subtyping. A first programming language application of this mechanism is coercive
subtyping [Luo 1999]. In this case we write A <: B instead of A ⊢ B and call A and B subtype andsupertype respectively, rather than premise and conclusion. Also we call the associated evidence ofthe judgment a coercion. Unlike other forms of subtyping, coercive subtyping changes the runtime
representation of a value of type A when upcasting to type B. This change is accomplished by
the coercion. Even though the coercion is executed at runtime, it is already statically known at
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

object Test {class P
class Q
class U}

206:5// proposition P// proposition Q// proposition U

implicit def f(implicit o : P) : Q = new Q()
implicit def g(implicit o : Q) : U = new U()
implicit val p : P = new P()// P -> Q// Q -> U// P

val u : U = implicitly[U]// triggers resolution from// the implicit environment

Fig. 1. Encoding of the judgment P → Q, Q → U , P ⊢ U as a Scala program.

what point in the program it needs to be performed, namely at the point in the static type system
where an appeal is made to subtyping. In order to introduce the coercion, coercive subtyping cantherefore make use of a static program transformation approach called (type-directed) elaboration.
Elaboration uses the information of static typing to transform a program with implicit appeals to
subtyping into a program with explicit applications of coercions. For example, consider a function fthat expects a value of type B and a value v of type A where A <: B. Hence, in the function call f v
there is a type mismatch that the type system bridges by appealing to subtyping. Elaboration thentransforms this function call into f (c v) where c is the coercion for A <: B. The explicit coercion
application replaces the implicit appeal to subtyping.
Resolution. A rather different application of logic inference in programming languages are
implicits in Scala. In their basic form, they involve an environment of premises that the programmer
can populate and extend with particular types and values of those types as evidence. Functions cantake implicit parameters which the type system fills in by searching values of the appropriate typein the implicit environment. Elaboration turns those implicit parameters into explicit ones. Thisbehavior is extended with the modus ponens inference rule, to make it more powerful.
The computational evidence associated to this rule, shown in Section 1, is λx .(f x) (д x) where fis the evidence for A ⊢ B → C and д for A ⊢ B. The modus ponens rule can be applied recursively,
e.g. to establish B from A by modus ponens via D → B and D, and we call the general reasoning
principle recursive resolution.
Resolution in Scala. As a concrete example of resolution in programming languages, consider the
judgment
P → Q, Q → U , P ⊢ U
In this statement, P implies Q, Q implies U and P holds as a fact. Thus, we can conclude that U
holds by straightforward logical reasoning.
Figure 1 illustrates how to encode the judgment in Scala. In this Scala program, we encode propositions as classes, and we define a few implicit rules that are added to the "implicit environment" of
Scala. The definition of f encodes P → Q, the definition of g encodes Q → U and the definition ofp encodes that P holds. In the definition of the value u, we trigger resolution (via the implicitly
keyword), which essentially searches the implicit environment and attempts to compose the rules
and facts in the implicit environment, to find a value of type U. This value will be given eventuallyby the synthesized expression g(f(p)).
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:6

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

Essentially, in logic, resolution can be seen as a mechanism for proof search. In programming
languages, resolution is a mechanism that searches for values of a given type by using the rules andfacts of the implicit environment. It can be viewed as a type-directed form of program synthesis.
The connection to our work is that we interpret the resolution relation as subtyping, andthe conjunction of propositions in the environment as intersections. Thus, the above judgment
corresponds to:(P → Q)&(Q → U )&P <: Uusing subtyping and intersection types.
Haskell type classes also employ resolution, but there are several superficial differences to Scala
implicits. The name spaces of implicit values—called type classes—is separate from that of othertypes and has global scope. Moreover type classes are used as a mechanism for overloading function
names. Yet, in essence, just like Scala implicits, type classes are based on the modus ponens inference
rule for constructing wanted evidence for types in terms of given evidence of other types. We will
look at type classes in more detail in Section 3.
2.2

Different Interpretations for Intersection Types in the Literature

There are several different interpretations of intersection types in the literature. Intersection types
date back to work from Coppo et al. [1981] and Pottinger [1980] and were first used to characterize
the strongly normalizable terms of the λ-calculus.
Following Forsythe [Reynolds 1988], intersection types were used in various other programming
languages, including CDuce [Benzaken et al. 2003] and Object Oriented languages like TypeScript2 ,Flow [Raskin 1974], Ceylon3 and Scala [Odersky 2010], enabling multiple inheritance [Pierce 1991].
They were also studied as part of the syntax of several calculi, to enable various forms of polymorphism such as finitary function overloading [Castagna et al. 1992], bounded polymorphism [Pierce
1997] and evaluation-order polymorphism [Dunfield 2015]. Refinement types is yet another feature
where intersection types has been studied [Davies and Pfenning 2000; Dunfield 2007; Freeman and
Pfenning 1991]. However, in those systems the type Int & Bool is invalid, since Int and Bool are
not refinements of each other.
Note that intersection types alone only increase the expressive power of types. While languages
with intersection types do not necessarily have a merge operator, the latter adds expressive power tothe terms. This term construct has been used in various, but usually limited, forms like in Forsythe
or in the work of Castagna et al. [1992], discussed in Section 7.
The use of intersection types in this paper follows the interpretation of Dunfield [2012] who has
proposed a particular flavor of intersection types with an unrestricted merge operator, allowing theconstruction of values that inhabit intersection types such as Int & Bool. In her work, Dunfield uses
coercive subtyping, based on the inference rules for the logical conjunction operator. In particular,
conjunction elimination is expressed in two rules:A∧B ⊢AA∧B ⊢B

Here, we write A&B, instead of A ∧ B, to denote an intersection type. The runtime representation ofvalues of type A&B is a tuple (v, w) where v has type A and w has type B. The coercions associatedwith the two inference rules are respectively π1 and π 2 , the projection on respectively the first andsecond component of the tuple. Dunfield observes that her formulation of the calculus does not
eliminate ambiguous expressions. However, recent work by Oliveira et al. [2016] remedies thisissue by introducing a notion of disjoint intersection types.
2 https://www.typescriptlang.org/
3 https://ceylon-lang.org/

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:7

Our proposed design fits well with this interpretation, i.e. intersection types as a mechanism to
implicitly provide coercions on pairs. Our source language provides a layer of convenience on topof an ordinary target language with pairs, by generating various types of coercions involving pairs.
In particular, the modus ponens rule is just one of the possible coercions involving pairs.
3

OVERVIEWThis section gives an overview of our work. We are mainly interested in the type-based overloading
and resolution capability at the core of type classes or implicits. In what follows, we use Haskell
type classes for illustration, but we could have used Scala implicits (or other similar mechanisms)
just as well. We start by establishing the relationship between type-based overloading based ontype classes and/or implicits and disjoint intersection types. Then we explain the key idea of ourwork to add modus ponens to the subtyping relation for a calculus with (disjoint) intersection types
to recover resolution. Finally, we discuss several technical challenges that need to be addressed forthis addition to work.
3.1

Type-based Overloading with Type Classes

Type classes in Haskell were initially meant to provide a less ad-hoc mechanism to overloading. In
Section 1 we have already seen a simple example of an overloaded function f defined via a typeclass. Overloading with type classes is based on parametric polymorphism [Reynolds 1974]. All
type classes require at least one type argument. This type argument is used to specify the places inthe signatures of overloaded methods where different types can occur. For the type class Over the
method f :: a -> a can be overloaded both on the input type and the output type and those two
types need to be the same for a particular overloading.
Conventionally, type class instances cannot overlap. That is, two instances for a type class mustuse distinct types. This property is satisfied by the three instances in Section 1:
instance Over Int where ...
instance Over Char where ...
instance Over Int => Over [Int] where ...
Adding a fourth instance for a type that is distinct from those in the previous instances (i.e. Int, orChar or [Int]) is allowed. For example, the following Bool instance is allowed:
instance Over Bool where f = not
However adding another instance for integers is not allowed:
instance Over Int where f x = x + 2 -- rejected!
The compiler complains that there is already another instance in scope for Over Int.
Overlapping instances and ambiguity. The restriction of non-overlapping instances is put into
place to ensure that there is no ambiguity in a program. If the second instance for integers were
accepted then the definition:p = f 1-- ambiguous: could be 2 or 3
would be ambiguous as it could choose either of the two integer instances.
3.2

The Merge Operator and Disjoint Intersection Types

The merge operator, originally proposed by Reynolds [1988], adds expressive power to intersection
types. In most calculi with intersection types, a type such as Int&Char is not inhabited, since these
two types are disjoint (i.e. do not have values in common), so their intersection is empty. With themerge operator, however, it is possible to build values that inhabit such an intersection type. For
example:Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:8

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachaliasv : Int & Char = 1 ,, 'c'In the definition of v, the merge operator (,,), is used to build a value of type Int&Char froman integer and a character. In calculi with a merge operator, intersection types are similar toconventional pair types. The merge operator is used to build values of the intersection types,
similarly to how we build values for pairs. The main difference to pairs and pair types is that whilefor pairs the eliminations (i.e. projections such as fst and snd) are explicit, for intersection types
they are implicit and driven by the type system.
Disjointness and ambiguity. The merge operator is powerful, but without any restrictions it iseasy to have ambiguous programs. For instance, consider the following value:n : Int & Int = 1 ,, 2
If we use n in an expression such as n + 1 there could be two possible results (2 and 3) dependingon what integer gets selected from the merge.
Disjoint intersection types [Oliveira et al. 2016] were proposed to solve ambiguity problems incalculi with intersection types and a merge operator. The key idea is to introduce a restriction on
merges: a valid merge can only be built from two values with disjoint types. Two types are disjoint
if the only supertypes that they have in common are top-like types [Oliveira et al. 2016]. This
restriction prevents the merged value n from type-checking, while accepting v. Furthermore, forprevious calculi with disjoint intersection types it has been proven that the disjointness restriction
is sufficient to guarantee coherence [Reynolds 1991], a correctness property that rules out any
ambiguity. This property is important for calculi with non-deterministic semantics, where wellformed expressions can take on multiple meanings, and ensures that these meanings are equivalent,in the sense that the program which the initial expression models will always behave the same.
3.3

Disjoint Merges, Non-Overlapping Instances and Resolution

Disjointness checks for merges and non-overlap checks for type class instances are closely related.
The non-overlap check for type classes can be viewed as a simple form of disjointness checking. If
we ignore polymorphic types, then the non-overlap check is simply testing whether two types are
distinct4 , which is subsumed by a disjointness check for merges.
Type class instances as merges. The fact that disjointness checking relates/subsumes to nonoverlapping checking is crucial for expressing code analogous to type class instances as merges.
Consider a variant of f in Section 1:
f : (Int -> Int) & (Char -> Char) & ((Int -> Int) -> [Int] -> [Int])= succ ,, toUpper ,, listInstance
where listInstance is analogous to the type class instance Over [Int] from Section 1, with thetype ((Int -> Int) -> [Int] -> [Int]). Here, the merge creates an overloaded function andchecks that the three implementations have disjoint types. This is similar to checking whether
Over Int, Over Char and Over [Int] overlap. Therefore, we can essentially express type classinstances through merges, whose components define the methods of the instances for overloading.
Resolution via Modus Ponens. While we can express some type class instances with disjoint
intersection types, an important “class” of instances cannot be expressed because previous work on
disjoint intersection types lacks resolution. That is, in previous work a program such as:
p : [Int] = f [1,2,3]
4 With polymorphism we also need to account for instantiation. For example the type [Int] is not equal to [a], but it does

instantiate [a]. So two instances C [a] and C [Int] (for some type class C) overlap.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:9

would not type check because [Int] -> [Int], which is the type that f needs to have, is not asupertype of the type of f. However the addition of modus ponens changes this and [Int] -> [Int]becomes a supertype of the type of f, thus enabling the above use of f.
3.4

First-Class Environments

Viewing instances/implicits as merges opens up the possibility of new and interesting features for
programming with implicit values and resolution. In particular, unlike type class instances (which
are second class), merges are first-class. In other words, we can pass merged values as argumentsor return them as results. This is not possible with type class instances. An instance declaration is
top-level, but we cannot create instances on the fly.5
To illustrate the use of first-class environments, consider a program that processes data from asensor measuring temperatures. The temperatures are collected at fixed time intervals, and thesensor may fail to read temperatures (for example due to temperatures being too high, low or tosome unknown error). The sensor data is collected in a text file using a sequence of numbers or
strings (for errors) separated by commas. For instance:
32,-9,"LOW",10,"ERROR"
With Haskell type classes one may be tempted to use the Read type class:class Read a whereread :: String -> ato process the String using the existing instances of the Read class:instance Read Int where ...
instance Read String where ...
instance Read a => Read [a] where ...
instance (Read a, Read b) => Read (Either a b) where ...
The programmer’s hope here would be that we could interpret the type of sensor values as [Either
String Int], and then simply employ resolution to compose the above instances:
read "32,-9,\"LOW\",10,\"ERROR\"" :: [Either String Int]
However this does not work because the input string is not in the correct format to be parsed by
the Read instances. In Haskell the Read instances for types such as Either a b and [a] use the
Haskell syntax6 . The read method provided by Read [Either String Int] would require thestring:"[Right 32, Right -9, Left \"LOW\", Right 10, Left \"ERROR\"]"
Because Haskell does not allow more than one instance of a type class for the same type, it is notpossible to use alternative instances for Either a b and [a]. There are various workarounds forthis issue, but none of these is ideal.
A solution using first-class environments. An alternative approach to solve this problem is touse merges to encode first-class environments for instances of Read. We present such a solution
using the λiMP calculus (assuming a few convenience source language features). For the purposesof illustration and readability we assume the following definition of Read:
type Read a = String -> aand we also assume built-in types for lists and sum types (i.e. modeling, respectively, Haskell’s
List a and Either a b). Given those, we can model four Haskell instances for Read:
5 Though recent work by Winant and Devriese [2018] aims to rectify this.
6 The Haskell format requires that strings to be read as Either a b values start with a Left or Right substring. For list

values, the string should start and end with opening and closing brackets.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:10

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

readInt : Read Int = ...
readString : Read String = ...
readEitherSI : Read String -> Read Int -> Read (Either String Int) = ...
readSensor : Read (Either String Int) -> Read [Either String Int] = ...
Here, readInt and readString behave just like the corresponding Haskell instances, while
readEitherSI and readSensor are custom instances that read values in the sensor format. With
intersection types and the merge operator we can define both the type of environments for instancesthat read sensor data, and the environment that collects the above instances:type SensorEnv = Read Int & Read String& (Read String -> Read Int -> Read (Either String Int))& (Read (Either String Int) -> Read [(Either String Int)])
env : SensorEnv = readInt ,, readString ,, readEitherSI ,, readSensor
Finally, the parseSensor function parametrizes over a suitable sensor environment:parseSensor (read : SensorEnv) (s: String) : [Either String Int] = read s
Calling parseSensor with env can parse strings in the expected format for sensor data. Moreover, an additional advantage of the parseSensor function is that it is decoupled from concrete
implementations of Read. For instance, if later we want to express sensor data using Haskell’s own
format for Read instances, we just have to provide an alternative environment:
haskEnv : SensorEnv = readInt ,, readString ,, readEither ,, readList
where readEither and readList behave just like the Haskell instances for Read (Either a b)
and Read [a]. By calling parseSensor with haskEnv as its first argument, the system will infer
an instance of the same type, but taken from the newly provided environment encoding, haskEnv.
Without the modus ponens rule in subtyping, the same functionality would require a more verbose
program, where both the provided environment and the parser function should be parametrized
over the alternative instances for Either String Int and [Either String Int], and whereapplication of instances should be explicit:
type PSensor = (Read Int -> Read String -> Read (Either String Int)))-> (Read (Either String Int) -> Read [Either String Int])-> Read Int & Read String& Read (Either String Int) & Read [Either String Int]
env' (rEitherSI : Read Int -> Read String -> Read (Either String Int))(rList: Read (Either String Int) -> Read [Either String Int]): Read Int & Read String & Read (Either String Int) & Read [Either String Int]= readInt ,, readString ,, (rEitherSI readInt readString),, (rList (rEitherSI readInt readString))
parseSensor' (rEither : Read Int -> Read String -> Read (Either String Int )))(rList: Read (Either String Int) -> Read [Either String Int])(readArg : PSensor) (s : String): [Either String Int]= readArg rEither rList s
In summary, modus ponens captures the essence of resolution and brings convenience to programmers by automatically composing instances. This is also the reason why resolution is heavily
used by Haskell and Scala programmers. In addition, the integration of modus ponens into a system
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:11

with intersection subtyping adds expressive power that is not available in Haskell or Scala. In
contrast to Haskell, implicit environments are first-class. With respect to Scala, viewing resolution
as subtyping makes obvious how the two features interact, which we discuss in more detail next.
3.5

Interaction Between Subtyping and Resolution

In languages like Scala, which supports both subtyping and resolution, we expect that the two
mechanisms interact. For example, here is a simple Scala program that requires both mechanisms:
class A {}class B extends A {}implicit val v : B = new B() {}; // adds v to the implicit environment
val u : A = implicitly // resolves to v
This program defines two classes A and B. The value v is marked with an implicit keyword, which
has the effect of adding v to the implicit environment, so that it can be used by resolution later.
In the definition of u, implicitly triggers resolution to search for a value of type A. The search
succeeds and resolves to v which has type B, a subtype of A. Clearly this only works if resolution
accounts for subtyping.
The Scala compiler accepts this program and its implementation of resolution does indeed
account for subtyping. However there is very little work formalizing the (non-trivial) interaction
between resolution and subtyping. Most foundational calculi for Scala formalize subtyping, but
not resolution [Amin et al. 2016, 2012]. Similarly, works that formalize resolution typically do notaccount for subtyping [Odersky et al. 2017; Oliveira et al. 2012; Schrijvers et al. 2019].
One advantage of making resolution a part of subtyping is that the interaction between the two
mechanisms then becomes trivial. For instance, the following program:a : Int= 1
b : Int & Char= a,,'c'u (env : Int&Char) : Int = env
is roughly analogous to the previous Scala program, except that we use a first-class environment(the argument env of function u) instead of an implicit environment. In this case resolution triggers
a search for an integer in the body of u, which is successful because Int&Char <: Int. Other more
complex interactions between subtyping and resolution, such as in:(Int -> Top -> Bool) & Int<: String -> Boolwork as well. In this case the two types in the intersection need to be composed with modus ponens
to obtain Top -> Bool and Top -> Bool <: String -> Bool via subtyping.
3.6

Technical challenges

To formalize our integration of resolution and subtyping, we create the λiMP calculus by extending
the NeColus calculus with the modus ponens rule. While the extension is seemingly a small change,
it has far-reaching consequences with respect to the metatheory. Conceptually, this is due to thefact that modus ponens invalidates much of the reasoning about types in the NeColus metatheory.
In NeColus it is possible to consider the syntactic components of types in isolation. This is nolonger possible in λiMP because one component may interact with another through modus ponens.
This affects coherence: the disjointness constraint of NeColus is insufficient for λiMP and needs
to be tightened. Also the coherence proof requires a considerably more complex canonicity relationthat features a form of context dependency to capture the possible interaction between typecomponents.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:12

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

TypesA, B, C
Terms
E
Typing Contexts Γ

Nat | ⊤ | A → B | A & B
x | ⊤ | i | λx . E | E 1 E 2 | E 1 , , E 2 | E : A• | Γ, x : A

F
FF

Fig. 2. λiMP Syntax
Γ ⊢E ⇒A⇝e

Type Synthesis⊢Γ⊢ΓΓ ⊢ ⊤ ⇒ ⊤ ⇝ ⟨⟩T-top

Γ ⊢ E 1 ⇒ A1 → A2 ⇝ e1

x : A∈ΓΓ ⊢ i ⇒ Nat ⇝ iT-natΓ ⊢x ⇒A⇝x

Γ ⊢ E 1 ⇒ A1 ⇝ e1

T-app

Γ ⊢E :A⇒A⇝e

Γ ⊢ E 2 ⇒ A2 ⇝ e 2⊢d A1 & A2

Γ ⊢ E 1 , , E 2 ⇒ A1 & A2 ⇝ ⟨e1, e2 ⟩Γ ⊢E ⇐A⇝e

T-var

Γ ⊢E ⇐A⇝eΓ ⊢ E 2 ⇐ A1 ⇝ e2

Γ ⊢ E 1 E 2 ⇒ A2 ⇝ e1 e2⊢ΓT-annoT-mergeType Checking
Γ⊢E⇒B⇝eΓ, x : A ⊢ E ⇐ B ⇝ eΓ ⊢ λx . E ⇐ A → B ⇝ λx : |A|. e

T-abs

B <: A ⇝ cΓ ⊢E ⇐A⇝ce

T-sub

Fig. 3. Bidirectional Typing

Algorithmic subtyping is also affected by this. The algorithm no longer terminates naturally andrequires a loop detector. This makes the termination proof a lot harder. Moreover, the size-based
induction used to prove transitivity for the algorithmic subtyping of NeColus breaks. Instead,our transitivity proof involves 7 mutually recursive lemmas and relies on the AProVE automatic
termination checker to establish their well-foundedness.
The following sections set up λiMP and explain these aspects in detail.
4

THE λiMP CALCULUS

Syntax. Figure 2 shows the syntax of λiMP . It is the same as that of NeColus, but—for the sake ofconciseness—without records. Types A, B, C include naturals Nat, the top type ⊤, function types
A → B and intersection types A & B . Terms E include variables x , natural numbers i , the top value⊤, function abstractions λx . E, function applications E 1 E 2 , merges E 1 , , E 2 and (type-)annotatedterms E : A.
Bidirectional Typing. The type system of λiMP , shown in Figure 3, is bidirectional and thus
has two modes: the synthesis mode (⇒) and the checking mode (⇐). The synthesis judgment
Γ ⊢ E ⇒ A ⇝ e means that we can synthesize type A from expression E in context Γ, while thechecking judgment Γ ⊢ E ⇐ A ⇝ e checks whether E has given type A. As usual, type annotations
switch from synthesis to checking mode (rule T-anno). We reserve further discussion over the parts
highlighted in gray for Section 4.2.
The rules are identical to those of NeColus with one notable difference. Rule T-merge not only
requires the types A1 and A2 of the two subterms to be disjoint, A1 ∗ A2 , but also requires them
to be internally disjoint, ⊢d A1 and ⊢d A2 , all summarised in the internal disjointness premise⊢d A1 & A2 of the rule. The two disjointness conditions are discussed in Section 4.4.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

A <: B ⇝ c

206:13

SubtypingA1 <: A2 ⇝ c1

S-reflA <: A ⇝ id | A |A2 <: A3 ⇝ c2

A1 <: A3 ⇝ c2 ◦ c1
A2 <: B2 ⇝ c2

B1 <: A1 ⇝ c1

A1 → A2 <: B1 → B2 ⇝ c1 → c2
A <: B1 ⇝ c1

A <: B2 ⇝ c2

A <: B1 & B2 ⇝ ⟨c1, c2 ⟩

S-and

S-top
S-trans

S-topArr
S-arr⊤ <: ⊤ → ⊤ ⇝ top→

S-andlS-andr|A|, |B |A & B <: A ⇝ π 1|A|, |B |A & B <: B ⇝ π2

| A | , | B1 | , | B2 |(A → B1 ) & (A → B2 ) <: A → B1 & B2 ⇝ dist→
A <: B1 ⇝ c1

A <: ⊤ ⇝ top | A |S-distArr

A <: B1 → B2 ⇝ c2

A <: B2 ⇝ c2

S-mp
c1

Fig. 4. Declarative Specification of Subtyping

The judgment ⊢ Γ used in the premise of rules T-top, T-nat and T-var expresses that the typing
context Γ is well-formed, i.e. it holds no duplicate variables. Its definition can be found in Appendix B.
4.1

Declarative Subtyping

Figure 4 declaratively specifies the subtyping relation of λiMP . The judgment A <: B ⇝ c statesthat A is a subtype of B and produces coercion c. Intuitively, c captures the way to convert valuesof type A into values of type B .
BCD-Style Subtyping. All but the last subtyping rule are the same as those of NeColus andoriginate from the BCD type system [Barendregt et al. 1983]. Rules S-refl, S-trans and S-top ensurethat subtyping is a partial order with ⊤ as greatest element. Rule S-arr is the standard subtyping rule
for function types, while rules S-andl, S-andr and S-and are standard for intersection types. Rules
S-distArr and S-topArr are standard BCD subtyping rules; the former enables nested composition [Biet al. 2018], while the latter provides a more unified treatment of top-like types in the meta-theoryof the language: without that rule, we cannot have A → B <: ⊤ → ⊤, if A is not top-like itself.
Modus Ponens. Our calculus extends the subtyping relation of NeColus with one new rule, S-mp,
which corresponds to the Modus Ponens inference rule of propositional logic. It states that if A
is a subtype of both B1 → B2 and of B1 , then it is also a subtype of B2 . While this extensionof subtyping is conceptually small, it has far-reaching consequences for the meta-theory of thelanguage.
4.2

Elaboration Semantics

Following NeColus we assign a semantics to λiMP by means of an elaboration. The target of theelaboration is λMP
c , which is the simply typed lambda-calculus extended with products and coercions.
Pairs are the elaboration target of merges (rule T-merge), while coercions explicitly witness theimplicit use of subtyping in λiMP (rule T-sub).
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:14

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

τ F Nat | ⟨⟩ | τ1 → τ2 | τ1 × τ2
e F x | ⟨⟩ | i | λx : τ . e | e1 e2 | ⟨e1, e2 ⟩ | c e
c F idτ | c1 ◦ c2 | topτ | c1 → c2 | π1τ1 ,τ2 | π2τ1 ,τ2 | ⟨c1, c2 ⟩ | top→ | distτ→1 ,τ2 ,τ3 |c1 c2Typing contexts ∆ F • | ∆, x : τValuesv F ⟨⟩ | i | λx : τ . e | ⟨v1, v2 ⟩ | (c1 → c2 ) v | top→ v | (distτ→1 ,τ2 ,τ3 ) v
Types
Terms
CoercionsFig. 5. λMP
Syntaxcc ⊢ τ1 ▷ τ2
c1 ⊢ τ 1 ▷ τ 2c2

e1 −→ e2

Coercion Typing

Small-Step Operational Semantics

c2 ⊢ τ1 ▷ (τ2 → τ3 )c1 ⊢ τ 1 ▷ τ 3

CT-mp

step-mp(c2c1 ) v −→ (c2 v ) (c1 v )Fig. 6. λMP
Coercion Typing and Operational Semantics (new rules)c

The λMPCalculus. Figure 5 shows the syntax of λMPcc . This syntax is nearly identical to that of
NeColus’ target language. There are only two differences, both situated in the coercions c. These
coercions express the conversion of a term from one type to another. The reason why we use
a separate syntactic sort of coercions for this—rather than encoding the conversions as regularfunction terms—is that it facilitates the coherence proof. Each coercion form corresponds to aparticular subtyping rule (Figure 4). The first and main difference to NeColus’ target calculus is that,
because we have a new modus ponens subtyping rule in λiMP , there is also a new corresponding
coercion form c1 c2 in λMP
to witness it. The second and minor difference is that we havecannotated several existing coercion forms with type information in order to facilitate type checking.
Figure 6 lists the new inference rules in the type system and small-step operational semanticsof λMPto support the new coercion form. The full definitions of these relations can be foundcin Appendix A. The coercion typing rule CT-mp essentially replicates the subtyping rule S-mp of
Figure 4, but now with λMP
types. The new small-step rule, step-mp, splits up an application of acmodus ponens coercion c2 c1 to value v into separate coercion applications c2 v and c1 v where
the former should yield a function that is applied to the latter.
How the features of λiMP are mapped to λMP
is given in the grey parts of Figures 4 and 3. IncMPthose figures the meta-function | · | transforms λi types to λMP
types, and extends naturally toctyping contexts. Its definition is in Appendix B.
4.3

Target and Elaboration Metatheory

We have formally investigated the metatheory of our calculus, λiMP , and of its target language, λMPc ,and mechanised it in Coq.
Target Language. Firstly, we have proven that the key metatheoretical properties of λMP
are notcinvalidated by the new coercion form. Indeed, λMP
is
type
safe:
c
Theorem 4.1 (Preservation). If • ⊢ e : τ and e −→ e ′, then • ⊢ e ′ : τ .
Theorem 4.2 (Progress). If • ⊢ e : τ , then either e is a value or there is an e ′ such that e −→ e ′.
Moreover, every well-typed λMP
term is normalising.
c
Theorem 4.3 (Normalisation). If • ⊢ e : τ then there exists a value v such that e −→∗ v .
Here −→∗ , is the reflexive transitive closure of −→.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

A∗B

206:15

Disjointness
A1 ∗ B
D-topL⊤∗A

A2 ∗ B

D-topRA ∗ B1A∗⊤

A1 & A2 ∗ B

D-andRA ∗ B1 & B2

A ∗ B2A2 ∗ B
D-mpL

D-mpR

(A1 → A2 ) ∗ B⊢d A

A ∗ B2

D-andLA ∗ (B1 → B2 )Internal Disjointness
ID-nat⊢d NatID-top
⊢d ⊤

⊢d B

A∗B
ID-arr⊢d A → B

⊢d A

⊢d B

ID-and⊢d A & B

Fig. 7. Disjointness conditions

Elaboration. Also, the elaboration of λiMP to λMP
preserves well-typing.
c
Theorem 4.4 (Coercions Preserve Types). If A <: B ⇝ c, then c ⊢ |A| ▷ |B |.
Theorem 4.5 (Elaboration Preserves Types).
• If Γ ⊢ E ⇒ A ⇝ e, then |Γ| ⊢ e : |A|.
• If Γ ⊢ E ⇐ A ⇝ e, then |Γ| ⊢ e : |A|.
The meta-function |Γ| translates a source typing context Γ to a target one. The full definition
can be found in Appendix B.
4.4

Disjointness Conditions

Figure 7 shows the rules for disjointness (top) and internal disjointness (bottom).
Disjointness. The purpose of the disjointness condition is to avoid ambiguous expressions like
1, , 2. Judgment A ∗ B conservatively captures the notion that the common supertypes of A and B
are all top-like. The first 4 rules of Figure 7, for the top type and intersection types, are the same as
those of NeColus. We turn our focus to the new rules D-mpL and D-mpR, added to accommodate the
new modus ponens subtyping rule. While they can be combined to recover NeColus’ D-arr rule7 ,B1 ∗ B2
D-arr(A1 → B1 ) ∗ (A2 → B2 )they cannot be used to recover the NeColus axioms Nat ∗ (A → B ) and (A → B ) ∗ Nat. On
the contrary, λiMP does not consider the types Nat and Bool → Nat to be disjoint. For the sakeof conciseness and compositionality, the disjointness definition is conservative. Indeed, merging
any expressions of those two types does not lead to ambiguity. Yet, if we merge two expressions
whose types contain the above two types, ambiguity can in fact arise. Consider the example((true , , (λx . 1) : Bool → Nat) , , 2) : Nat. The elaborated form of the merge expression on theleft of the outer type annotation is the tuple ⟨⟨true, λx : Bool. 1⟩, 2⟩. The outer type annotation
will trigger the subtyping mechanism, first via rule T-anno and then through rule T-sub, in orderto produce a value of type Nat. This example is ambiguous, because it can produce—throughsubtyping—two different values of this type: 2 by projecting on the right component of the outertuple, and 1 by projecting on the left component of the outer tuple and using modus ponens toapply (λx : Bool. 1) to true. The respective subtyping derivations and the coercions they generate
are shown in Figure 8. For similar reasons, expressions (λx . 1) : Bool → Nat , , (2 , , true) and7 This rule states that two arrow types are disjoint if their codomains are disjoint.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:16

Example (a)Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

B×(B→N), N

S-andr(B & (B → N)) & N <: N ⇝ π2

B & (B → N) <: B ⇝ π1B, B→N

Example (b)B & (B → N) <: B → N ⇝ π2B, B→N

B×(B→N), N(B & (B → N)) & N <: B & (B → N) ⇝ π1

(B & (B → N)) & N <: N ⇝ (π 2B, B→N

B & (B → N) <: N ⇝ π2B, B→N
π1B, B→N ) ◦ π1

B×(B→N), N

π 1B, B→N

S-mp
S-transFig. 8. Example subtyping derivations. Types Bool and Nat are abbreviated here as B and N, respectively.

(2 , , (λx . 1) : Bool → Nat) , , true are also ambiguous. In all three cases, the component types of amerge will not be disjoint.
The two new rules D-mpL and D-mpR bring the notion of disjointness between two types closer tothe notion of no-overlaps between two (or more) instances. Types B and A → B are not disjoint,
similarly to how two Haskell instances C Int and D Int => C Int overlap.
Harmless overlaps and (non-)ambiguity. Note that not all forms of overlap introduce semantic
ambiguity. In particular, we identify two such harmless cases. Firstly, in the presence of an overlap,
it can still be the case that there is only one way to resolve a value of a given (overlapping) type.
For example, in the term 2 , , (λx . 1) : Bool → Nat of type Nat & (Bool → Nat), the types Nat andBool → Nat overlap, but there is only one applicable way to resolve a value of type Nat, because
there is no Bool value to feed to the function (λx . 1) : Bool → Nat. Secondly, expressions of an
overlapping type are harmless when all possible resolution paths for a wanted type result in thesame inferred value. For example, the term (1 , , 1), while containing an overlap, is unambiguous.
Because of the disjointness condition imposed over merges, the source calculus conservatively
rejects expressions that fall under either of the two harmless forms of overlap, when they are
explicitly written by the programmer. However, they are still possible implicitly, through a type
annotation, which invokes subtyping. For example, we can encode the rejected term (1 , , 1) as
1 : Nat & Nat, which is accepted and semantically same. Its full typing derivation is in Appendix E.
Internal Disjointness. The internal disjointness predicate, ⊢d A, requires that the two components
of any intersection type that appear in A are disjoint. Intuitively, ⊢d A ensures that if A <: B , thenB can only contain harmless overlaps.
The internal disointness condition is imposed on the subterms of a merge in rule T-merge. Again
this is a conservative measure to avoid ambiguity, this time of a more convoluted nature thatinvolves nested merges interleaved with subtyping. Here is a minimal ambiguous example toillustrate the problem:((true , , b2n) : Nat & (Bool → Nat) , , false) : NatThis example features b2n, which we assume to be a built-in function of type Bool → Nat thatmaps true to 1 and false to 0. The inner merge has type Bool & (Bool → Nat), but is converted
to type Nat & (Bool → Nat) by means of the type annotation, which triggers the subtyping
mechanism. The latter produces a coercion that is then applied on (the elaborated form of) thesubterm true , , b2n. The corresponding value is 1 , , b2n, which could not be written explicitly
because Nat and Bool → Nat are not considered disjoint. Yet, because this value is not explicitly
written by the programmer, but implicitly produced through subtyping, we know that the overlap
is harmless. Indeed, while the expression 1 , , b2n potentially produces two different values of typeNat, one of those requires a Bool, which is not available at this point.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:17

However, the outer merge with false provides the missing Bool value, making the outer Nat type
annotation ambiguously yield both 0 and 1 as possible results. The disjointness check rejects noneof the two merges in the example. Here, the internal disjointness constraint comes in. It catches
the ambiguity problem at the outer merge where it identifies 1 , , b2n as unfit to merge with.
Internal disjointness inherits the conservative behavior of the (binary) disjointness condition, as
witnessed in rule ID-arr. This rule regards the case of a function type A → B that potentially is asupertype of some internally disjoint type, say A′ (formally, A′ <: A → B ). If A′ is not a subtype
of A (thus, A′ <: A does not hold), then rule S-mp does not apply. In fact, it becomes impossible toimplicitly produce B from A′ and, therefore, unnecessary to demand internal disjointness of B .
The indifference of rule ID-arr around domains of arrow types is justified by the intuition that if
a supertype of an internally disjoint type contains overlaps, then those are harmless. A functionof type A → B is unambiguous if it outputs unambiguous values of type B , given unambiguous
input values of type A. This implies the requirement that A is also internally disjoint. However,at this point, only values produced implicitly from A′ are considered, and these can only containharmless ambiguity. Indeed, explicit values can be added only through the merge operator, thus
falling under rule ID-and. Thus, unambiguity is ensured for A.
5

ALGORITHMIC SUBTYPINGIn this section, we present an algorithm that decides the subtyping relation of Figure 4.
In the declarative specification of the subtyping relation (Figure 4), rules S-trans and S-mp hinder
the decidability of subtyping: they both require guessing an appropriate intermediate type (A2 in
the former, and B1 in the latter). We address this by employing a technique originating from proof
search known as focusing [Andreoli 1992]. The general strategy for checking a constraint of the form
A <: B is to structurally analyze (focus on) B , and when it is stripped down to a base type do thesame for A. This task is performed by two mutually-recursive judgments, the first focusing on theright type B , and the second focusing on the left type A. This technique has already been employed
by Bi et al. [2018]—and, before that, by Pierce [1989]—though with a single all-in-one judgment.
Our algorithm separates the two phases for clarity (and ease of reasoning) and also deals with theadditional complexity introduced by rule S-mp. Unfortunately, the support for modus ponens greatly
complicates the algorithm’s proofs of transitivity and termination. For the former, we had to comeup with an approach external to Coq, involving the AProVE termination checker [Giesl et al. 2017],
to establish well-foundedness. In the remainder of the section we describe the subtyping algorithm
in detail (Section 5.1), as well as its most important meta-theoretical properties (Section 5.2). We
follow the earlier convention to highlight the parts of the rules that concern coercion generation.
5.1

The Subtyping Algorithm

In Figure 9, we present the algorithmic subtyping judgment A ≺: B ⇝ c; the algorithmic counterpart of the declarative judgment A <: B ⇝ c of Section 4.1. The main judgment is defined interms of two auxiliary, mutually-recursive judgments L ⊢R A ≺: B ⇝ c and L; M; A0 ; X ⊢L A ≺:B ⇝ X ′, each focusing on the right or the left component of a type inequality, respectively. We
explain the former in Section 5.1.1 and the latter in Section 5.1.2.
Preliminaries. Meta-variables L and M stand for queues of types. The algorithm uses them tocapture the left-hand sides of arrow types. Operation L →→ B converts a queue L back into a type,given the right-hand side type B . It is inductively defined as follows:
[] →
→B =B
(A, L) →→ B = A → (L →→ B)
Meta-variable X denotes algorithmic contexts. An algorithmic context is merely the Cayley representation of a coercion: a function from coercions to coercions. Given a coercion c, we can convert
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:18

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

A ≺: B ⇝ c

Algorithmic Subtyping[] ⊢R A ≺: B ⇝ cA-mainA ≺: B ⇝ c

L ⊢R A ≺: B ⇝ cRight Focusing

L ⊢R A ≺: B1 ⇝ c1

L ⊢R A ≺: B2 ⇝ c2

B1 , B2
L ⊢R A ≺: B1 & B2 ⇝ JLK&
◦ ⟨c1, c2 ⟩L, B1 ⊢R A ≺: B2 ⇝ cAR-arrAR-andL ⊢R A ≺: B1 → B2 ⇝ c
L; []; A; (λc.c) ⊢L A ≺: Nat ⇝ X

AR-natAR-top
L ⊢R A ≺: ⊤ ⇝ JLK⊤ ◦ top | A |L; M; A0 ; X ⊢L A ≺: B ⇝ X ′L ⊢R A ≺: Nat ⇝ X[id | Nat | ]Left Focusing| A | , | A2 |L; M; A0 ; (λc.X[c ◦ π1 1]) ⊢L A1 ≺: Nat ⇝ X ′AL-nat[]; M; A0 ; X ⊢L Nat ≺: Nat ⇝ X

L; M; A0 ; X ⊢L A1 & A2 ≺: Nat ⇝ X ′| A | , | A2 |L; M; A0 ; (λc.X[c ◦ π2 1]) ⊢L A2 ≺: Nat ⇝ X ′L; M; A0 ; X ⊢L A1 & A2 ≺: Nat ⇝ X ′[] ⊢R B1 ≺: A1 ⇝ c 1

AL-and1

AL-and2

L; M, B1 ; A0 ; (λc.X[c 1 → c]) ⊢L A2 ≺: Nat ⇝ X ′B1, L; M; A0 ; X ⊢L A1 → A2 ≺: Nat ⇝ X ′AL-arrL; M; A0 ; X ′ ⊢L A2 ≺: Nat ⇝ X ′′[] ⊢R A0 ≺: (M →→ A1 ) ⇝ c2|
(A1 →A2 ) | , | A1 ||
(A1 →A2 ) | , | A1 |(c ◦(ππ2)),(A1 →A2 ), A1
X ′ = (λc.JMK& 1◦ ⟨X[id | A1 →A2 | ], c2 ⟩)L; M; A0 ; X ⊢L A1 → A2 ≺: Nat ⇝ X ′′AL-mp

Fig. 9. Algorithmic Subtyping

an algorithmic context X into a coercion by function application, denoted as X[c]. The role ofalgorithmic contexts is explained in Section 5.1.2 where we discuss the left-focusing rules.8
5.1.1 Right Focusing. As mentioned earlier, the first judgment (L ⊢R A ≺: B ⇝ c) structurally
analyzes B , until it is stripped down to a base type (Nat or ⊤). The accumulating parameter L
captures the domains of arrows encountered in B , such that the following holds:
Lemma 5.1 (Soundness of Right Focusing). If L ⊢R A ≺: B ⇝ c then A <: (L →→ B ) ⇝ c.
The first judgment is mostly borrowed from NeColus; we explain it only briefly here.
Subtyping. Ignoring coercion generation for now, the judgment works as follows: Rule AR-anddecomposes an intersection type, similar to its declarative counterpart (rule S-and). Rule AR-arr
deals with arrow types: the left sides of arrow types are inserted in the rear of type queue L
and removed again later, left-to-right, as arrows are encountered in A (see rule AL-arr below).
There are two base cases: either B = ⊤ or B = Nat. Rule AR-top handles the first case, where
8 In both our mechanization and implementation of the algorithm we use a defunctionalized [Reynolds 1972] representationof algorithmic contexts, which we then interpret as actual functions between coercions.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

AR-nat =⇒AL-nat =⇒L0 ; M0 ; A0 ; X0 ⊢L A0 ≺: Nat↓
L1 ; M1 ; A0 ; X1 ⊢L A1 ≺: Nat↓···↓
Ln ; Mn ; A0 ; Xn ⊢L An ≺: Nat

206:19

⇝
⇝

⇝

Xn
↑
Xn
↑
···
↑
Xn

(M0 = [], X0 = □)(An = Nat, Ln = [])Fig. 10. Visual Representation of the Execution of (L; M; A0 ; X ⊢L A ≺: B ⇝ X ′ )subtyping directly produces a coercion with the use of the meta-function JLK⊤ , discussed in
the next paragraph. If B = Nat, then we perform structural analysis on A, using judgment
L; M; A0 ; X ⊢L A ≺: B ⇝ X ′, which we elaborate on in Section 5.1.2.
Coercion Generation. The elaboration side is a bit more involved. Coercion generation can beunderstood via Lemma 5.1 and works as follows. Rule AR-and deals with intersection types. By
induction we have that
A <: (L →→ B1 ) ⇝ c1=⇒ A <: (L →→ B1 ) & (L →→ B2 ) ⇝ ⟨c1, c2 ⟩A <: (L →→ B2 ) ⇝ c2
1 , B2
We finish the transition to L →→ (B1 & B2 ) using meta-function JLKB
, whose meaning is given&
9by the following lemma:
1 , B2
Lemma 5.2. ∀L, B1, B2 , (L →→ B1 ) & (L →→ B2 ) <: L →→ (B1 & B2 ) ⇝ JLKB.
&Rule AR-top deals with the same problem that rule AR-and does: according to Lemma 5.1, thecoercion needs to witness A <: (L →→ ⊤), and not simply A <: ⊤. As (L →→ ⊤) is top-like [Alpuim
et al. 2017] we can always cast ⊤ to it, which is what JLK⊤ witnesses:9
Lemma 5.3. ∀L, ⊤ <: (L →→ ⊤) ⇝ JLK⊤ .

Rule AR-arr is straightforward. Finally, rule AR-nat handles the base case where B is Nat. In thiscase we resort to the auxiliary judgment L; M; A0 ; X ⊢L A ≺: B ⇝ X ′, which we discuss next.
5.1.2 Left Focusing. The intuition behind L; M; A0 ; X ⊢L A ≺: B ⇝ X ′ is that the (input) algorithmic context X witnesses the transition from A0 to (M →→ A), the component of A0 that weare currently focusing on. The (output) algorithmic context X ′ is meant to capture the complete
transition from A0 to (M →→ (L →→ B )). Essentially, starting with rule AR-nat as the entry point,
the judgment continuously decomposes A (via rules AL-and1, AL-and2, AL-arr, and AL-mp) until it
equals B (rule AL-nat); then the accumulated context X witnesses the complete transition from
A0 to (M →→ (L →→ B )) and the job is done. Figure 10 visualizes this process.
Subtyping. Ignoring coercion generation, the judgment works as follows: Rule AL-nat constitutes
the base case where subtyping holds trivially. Rules AL-and1 and AL-and2 non-deterministicallyfocus on the left or the right component of an intersection, similarly to their declarative counterparts(rules S-andl and S-andr, respectively). Rule AL-arr is the algorithmic version of rule S-arr: wedequeue B1 from L in a first-in-first-out manner, in order to match the order in which arrows areencountered in A. After we prove subtyping for the domains of the functions, we record that weare going under a binder of type B1 in the queue M and proceed recursively with the function
images. Queue M thus captures all the arrow domains in B that have been removed in lockstep
9 Its definition is straightforward and thus omitted; it can be found in Appendix D.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:20

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

with arrow domains in A using rule S-arr.10 This context becomes useful when we need to use
Modus Ponens under a binder, e.g. to prove
Nat → (Bool & (Bool → String)) <: Nat → String(or even ⊤ → (Bool & (Bool → String)) <: Nat → String). Lastly, rule AL-mp is the algorithmic
version of the S-mp rule. The first premise reveals the synergistic relationship between this ruleand rule AL-arr: when we need to synthesize an argument for Modus Ponens, we restart fromthe original type A0 —thus capturing the complete implicit context of A1 → A2 —and use thecontextualized version of A1 , (M →→ A1 ). For the above example, this amounts to proving
Nat → (Bool & (Bool → String)) <: Nat → BoolThe second premise is straightforward.
Note that rules AL-arr and AL-mp overlap and, to ensure completeness with respect to thedeclarative specification of subtyping, backtracking is required. However, it is never the case thatboth rules can apply for resolving a subtyping judgment. That is, backtracking will always fail in atleast one of the two choices.
Coercion Generation. The elaboration side, again, requires a bit more explanation. The complication arises in rule AL-mp, where the first premise restarts from the original type A0 . This is essential
for recovering the unfocused context needed for Modus Ponens, but it goes against the inductive,
top-down approach to coercion generation that we follow in the right-focusing rules. Coercions
produced by the recursive calls can no longer be directly combined. This is why the left focusing
rules use algorithmic contexts instead of coercions. The essence of the algorithmic contexts is
captured in the following invariant, which is preserved by each step of the left focusing algorithm:
Invariant 1. ∀c A′, Ai <: A′ ⇝ c =⇒ A0 <: (Mi →→ A′) ⇝ Xi [c]Metavariables Ai , A0 , Mi , and Xi refer to the corresponding parameters at the i-th step in
Figure 10. Informally, X captures the transition from A0 to Ai : Xi [c] witnesses the complete
transition from A0 to any type A′, if we have a way to perform the remaining transition from Ai
to A′. Hence, every rule of the judgment strips a layer off A and extends the “input” algorithmic
context accordingly, so that Invariant 1 is preserved.
Rule AL-mp is by far the most interesting rule. It commits to using the S-mp rule: the left premise
produces a coercion c2 that provides the argument (of type M →→ A1 ), while the appropriate
instantiation of the current context X gives us the function (of type M →→ (A1 → A2 )):A0 <: M →→ A1 ⇝ c2
A0 <: M →→ (A1 → A2 ) ⇝ X[id | A1 →A2 | ]Yet, the above coercions cannot be directly combined, due to the type queue M. We remedy thisusing meta-function JMKc&, B1 , B2 , whose meaning is given by the following lemma:11

Lemma 5.4. ∀L B1 B2 B c, B1 & B2 <: B ⇝ c =⇒ (L →→ B1 ) & (L →→ B2 ) <: L →→ B ⇝ JLKc&, B1 , B2 .

The general idea is that if (A0 <: M →→ A1 ⇝ c2 ) and (A0 <: M →→ (A1 → A2 ) ⇝ c1 ) then
| (A→B ) | , | A |(c ◦(π1A0 <: M →→ A2 ⇝ (λc.JMK&| (A→B ) | , | A | )),(A→B ), Aπ2

◦ ⟨c1, c2 ⟩) [id | A2 | ]Returning to rule AL-mp, the second premise uses the above algorithmic context (named X ′ forconvenience) to further focus on A2 .
i ++ Li = L0 , where ++ denotes list concatenation. At the end, we have Mn = L0 .
11 Its definition is straightforward and thus omitted; it can be found in Appendix D.
10 In Figure 10, it is easy to see that M

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

5.2

206:21

Algorithm Metatheory

Subsumption of NeColus’ Algorithmic Subtyping. First, we have proven that the subtyping algorithm of Figure 9 subsumes the subtyping algorithm of NeColus [Bi et al. 2018, Fig. 12]:
Theorem 5.5 (Subsumption of NeColus’ Algorithm). If [] ⊢ A ≪ B ⇝ c then A ≺: B ⇝ c.
where L ⊢ A ≪ B ⇝ c denotes the subtyping algorithm of NeColus.
Transivity and Modus Ponens. A major difference between algorithmic and declarative subtyping
is that the latter has an explicit transitivity rule while the former does not. Hence, transitivity ofalgorithmic subtyping requires a separate proof. Unfortunately, this proof is considerably more
involved than in NeColus. Instead of one inductive core lemma, it consists of 7 mutually recursive
lemmas. The well-foundedness of the induction used in the proofs of those 7 lemmas is no longer
a straightforward size-based induction that can be easily understood by Coq. To overcome thisproblem we have used a new approach, external to Coq, to establish well-foundedness. We haveencoded the proof—which is essentially an algorithm that transforms derivation trees—as a term
rewriting system. Then we have used the AProVE tool [Giesl et al. 2017] to verify its termination
automatically. AProVE reports success after 40 steps of transformation, decomposition and basic
termination arguments.
Theorem 5.6 (Transitivity of Algorithmic Subtyping). If A1 ≺: A2 ⇝ c1 and A2 ≺:A3 ⇝ c2 , then A1 ≺: A3 ⇝ c3 for some c3 .
The modus ponens property for algorithmic subtyping is closely tied to transitivity proof and isanother consequence of the 7 mutually recursive lemmas.
Corollary 5.7 (Modus Ponens of Algorithmic Subtyping). If A ≺: B1 → B2 ⇝ c1 andA ≺: B1 ⇝ c2 , then A ≺: B2 ⇝ c3 for some c3 .
Soundness and Completeness. We have proven that the subtyping algorithm (Figure 9) is soundand complete with respect to its declarative specification (Figure 4). The soundness of the overall
algorithm is a direct corollary of the soundness of right focusing (Lemma 5.1):
Theorem 5.8 (Soundness). If A ≺: B ⇝ c then A <: B ⇝ c.
The completeness proof largely follows the same strategy as for NeColus. The main challenge was
the new transitivity proof discussed above.
Theorem 5.9 (Completeness). If A <: B ⇝ c then there exists c ′ such that A ≺: B ⇝ c ′.
Termination. The final key property of the algorithm is termination. Actually, the algorithm
presented in Figure 9 is not terminating. Consider for example the trace of Nat → Nat ≺: Nat:
AR-natAL-mp

AR-natAL-mp([] ⊢R Nat → Nat ≺: Nat) −−−−−−−→ ([]; []; Nat → Nat ⊢L Nat → Nat ≺: Nat) −−−−−−→([] ⊢R Nat → Nat ≺: Nat) −−−−−−−→ ([]; []; Nat → Nat ⊢L Nat → Nat ≺: Nat) −−−−−−→ . . .
Such a subtyping judgment can result from an erroneous type annotation by the user. Nonetheless,the language does not statically detect annotations that may cause non-termination in the subtyping
algorithm. Another example, perhaps more plausible as a programming error, is an annotation that
leads to the judgment (Nat → Bool) & (Bool → Nat) ≺: Nat. One simple ingredient needs to be
added to the algorithm to make it terminating: a loop detection on the [] ⊢R A ≺: B call in rule
AL-mp. This loop detection should reject any calls that repeat one of their ancestor calls.
We can show that (1) any infinite derivation involves an infinite number of these nested calls
and that (2) detecting repeated calls is effective at stopping the non-termination.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:22

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

A priori there are multiple possible ways in which the algorithm can diverge. It might involvean infinite sequence of recursive calls within one of the two judgments. However, following the
focusing approach, the two judgments structurally decompose their focal argument. Hence, on
their own they are clearly terminating. Any divergence must thus involve an infinite number ofmutually recursive calls between the two judgments. There are two “gatekeepers” of the mutual
recursion, calling back from the left-focusing into the right-focusing judgment. These two are
the problematic one in rule AL-mp and the one in rule AL-arr. Yet, we can show that an infinite
number of recursion steps through rule AL-Arr is impossible and thus we can eliminate it fromconsideration. Indeed, the left-arrow depth || · || defined below decreases strictly in every AL-arr
loop step, and non-strictly in every other step. Moreover, a value of 0 inhibits rule AL-arr. Thus,
after a finite number of AL-arr steps, the rule can no longer be used.
||Nat||
||⊤||

=
=

0
0

||A → B || = max (||A|| + 1, ||B||)||A & B || = max (||A||, ||B||)||[] ⊢R A ≺: B|| = max (||A||, ||B||)

That leaves only the problematic mutually recursive call in rule AL-mp, which we have alreadydemonstrated to be a source of non-termination. Fortunately, we can show that the number ofdistinct nested calls is finite. Hence, on any infinite derivation path, a repeated call has to occur
after a finite number of steps. This makes the loop detection effective at curtailing divergence.
A more extensive account can be found in Appendix G.
Theorem 5.10 (Termination). The algorithm extended with loop detection terminates.
Decidability. In summary, if we take the soundness, completeness and termination of the subtyping together, we can conclude that the declarative subtyping is decidable.
Corollary 5.11 (Decidable Subtyping). In λiMP , A <: B is decidable for any two types A and
B.
6

COHERENCE

A desired property for calculi with a merge operator is coherence. This ensures that no semantic
ambiguity arises in programs, i.e. programs and their subparts always have a single, unambiguous
meaning. Recall that the semantics of λiMP is given indirectly, through an elaboration to λMP
andcits operational semantics. Hence, coherence for λiMP means that all possible elaborations of awell-typed source expression for a given type are contextually equivalent in the target language.
Two target expressions, that may be syntactically different, are contextually equivalent iff, whenused in the context of any program, there is no difference in that program’s behavior. In our purely
functional and strongly normalising setting, we can reduce a program’s behavior to the value it
returns. Moreover, as usual, we can restrict ourselves without loss of generality to programs oftype Nat to facilitate the comparison of the results.
Program contexts express the above notion of using an expression in the context of a programand are defined as follows:
Program contexts C F [·] | λx . C | C E | E C | C , , E | E , , C | C : A
Intuitively, a program context is an expression with a missing subexpression. This hole can be filledin with an appropriate term to form an actual expression. Which terms are eligible to be used ina program context is captured by the context typing judgment that consists of judgments of theform C : (Γ ⇒ A) 7→ (Γ ′ ⇐ B ) ⇝ D.12 Essentially, the judgment expresses that program context
12 There are also judgments for the three other combinations of the two typing directions that appear in the judgment. The

full specification can be found in Appendix C.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:23

C expects a term of type A under typing context Γ to form an expression of type B under context
Γ ′. Moreover, the source context C elaborates straightforwardly to a target context D. Indeed, forthe coherence of λiMP we do not account for all possible target contexts, but only for those that are
the image of a source context C. This restriction is important, as Bi et al. [2018] have demonstrated
that there are other target contexts that can distinguish between alternative elaborations.
We can now formally state coherence13 .
Theorem 6.1 (Coherence of λiMP ). For any C : (Γ ⇒ A) 7→ (• ⇒ Nat) ⇝ D,
if Γ ⊢ E ⇒ A ⇝ e1 and Γ ⊢ E ⇒ A ⇝ e2 , then there is a value • ⊢ v : Nat such that D{e1 } −→∗ v
and D{e2 } −→∗ v .
Here, D{e } denotes the term that results from filling in the hole of D with expression e.
The remainder of this section summarizes our proof approach for coherence and discusses theissues for our proof’s partiality. A more extensive account can be found in Appendix F.
6.1

A Context Dependent Logical Relation

We follow the general approach for showing coherence as NeColus. This approach is based on arather atypical heterogeneous binary logical relation, called canonicity, by Bi et al. [2019].
Canonicity. The canonicity relation is in fact two families of relations, one for values V andone for expressions E, indexed by types. Two values v1 and v2 of types τ1 and τ2 are related bycanonicity, written (v1, v2 ) ∈ V(τ1, τ2 ), iff any parts of the same type have the same meaning.
By parts we mean values v1′ and v2′ derivable from respectively v1 and v2 by means of subtyping
coercions. If two values have non-trivial (i.e., non-top-like) parts with the same type, we say thatthey overlap. For instance, values ⟨1, true⟩ and 1 overlap since both have a part of type Nat; because
their overlapping part is the same, namely 1, these values are related by canonicity. In contrast,⟨1, true⟩ and 2 are not related since their overlapping Nat parts are different.
While the λiMP canonicity relation follows the above principles just like that of NeColus, there
are considerable differences in the actual definition because of the addition of modus ponens.
Context Dependency. A major complicating factor in the design of the new logical relation is thatthe modus ponens subtyping rule introduces a form of context dependency. Indeed, when reasoning
about overlapping parts, the NeColus approach of decomposing terms and their types, and looking
at their syntactic components in isolation no longer works. Instead, in λiMP the components haveto be considered in the context of the whole value they appear in. For example, the target term
λx : Nat. true does not overlap with false, since one is an arrow type and the other a boolean. Yet,when λx : Nat. true is part of the larger term ⟨λx : Nat. true, 1⟩, a problematic overlap arises: via
modus ponens, the function applied to 1 to yields the boolean value true that differs from false.
To account for that dependency on the whole value, or contextual dependency for short, we
equip the canonicity relation of λiMP with two additional indices: the whole values and their types.
Thus, we write(v1, v2 ) ∈ V (v1 :τ1 ;v2 :τ2 ) Jτ1 ; τ2 K
′

′

′

′

to express that v1 and v2 are related values of types τ1 and τ2 that are components of respectively
the values v1′ of type τ1′ and v2′ of type τ2′ .
We refer to Appendix F for the full definition of this context-dependent canonicity relation V
for values and its companion E for expressions.
13 There is a second statement for the type checking direction of the two hypotheses.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:24

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

Properties. A key property of the canonicity relation is coercion compatibility. This states thatany coercions of related values are related as well.
Lemma 6.2 (Coercion Compatibility).
If (v1, v2 ) ∈ V (v1 :τ1 ;v2 :τ2 ) Jτ1 ; τ2 K, then for all coercions c1 , c2 and types τ1′ , τ2′ such that c1 ⊢ τ1 ▷ τ1′′′
and c2 ⊢ τ2 ▷ τ2′ it holds that (c1 v1, c2 v2 ) ∈ E (c1 v1 :τ1 ;c2 v2 :τ2 ) Jτ1′ ; τ2′ K.
The following lemma asserts another key property of the value relation, which establishes its
connection to disjointness. This follows from the design principle that any overlap in types should
concern indistinguishable values. If there is no overlap, then this is trivially satisfied.
Lemma 6.3 (Disjointly-Typed Values are Related). If • ⊢ v1 : |A1 | and • ⊢ v1 : |A2 | whereA1 ∗ A2 , then (v1, v2 ) ∈ V (v1 : | A1 | ;v2 : | A2 | ) J|A1 |; |A2 |K.
6.2

Coherence Proof

With the canonicity relation in place, we can turn to the actual coherence proof. This proof issplit in two parts by the canonicity relation. The first and hardest part is to show that any two
elaborations of the same source term are related by canonicity; this is the so-called fundamental
property, . The second part is to show that related programs of type Nat return the same value; itfollows almost trivially from the definition of the canonicity relation.
Logical Equivalence. To express the fundamental property, we need to introduce a notion oflogical equivalence for open expressions on top of the canonicity relations for closed values (V) andclosed terms (E). Open expressions are considered in some typing context ∆. A closing substitution
γ of a typing context ∆ maps variables to values of the type specified in ∆. Two open expressions
are related iff applying any two related closing substitutions to e1 and e2 , respectively, results in
E-related closed terms:∆1 ; ∆2 ⊢ e1 ≃log e2 : τ1 ; τ2 ≜ ∀ (γ 1 ; γ 2 ) ∈ GJ∆1 ; ∆2 K, (e1 [γ 1 ], e2 [γ 2 ]) ∈ V (e1 [γ1 ]:τ1 ;e2 [γ2 ]:τ2 ) Jτ1 ; τ2 K

Two closing substitutions γ 1 and γ 2 of ∆1 and ∆2 are related iff the two typing contexts differ
only in the types of the variables (otherwise, they contain the same variables and in the same order)
and the values that γ 1 and γ 2 contain for each variable are V-related.
Fundamental Property. Now we can state the fundamental property:14
Theorem 6.4 (Fundamental property). If Γ ⊢ E ⇒ A ⇝ e1 and Γ ⊢ E ⇒ A ⇝ e2 ,then |Γ|; |Γ| ⊢ e1 ≃log e2 : |A|; |A|.
Due to the complexity of the canonicity relation, we have proven this theorem under Conjectures 1
and 2. The proof proceeds by induction on the first hypothesis and calls coercion compatibility for
the T-sub case. The conjectures are used in the inductive cases of T-abs and T-merge.
Conjecture 1 (Compatibility of abstractions). If ∆, x : τ1′ ; ∆, x : τ2′ ⊢ e1 ≃log e2 : τ1 ; τ2 ,then ∆; ∆ ⊢ λx : τ1′ . e1 ≃log λx : τ2′ . e2 : τ1′ → τ1 ; τ2′ → τ2 .
Conjecture 2 (Compatibility of pairs). If ∆; ∆ ⊢ e1 ≃log e2 : τ1 ; τ2and ∆; ∆ ⊢ e1′ ≃log e2′ : τ1′ ; τ2′ and τ1 ∗τ2′ and τ2 ∗τ1′ , then ∆; ∆ ⊢ ⟨e1, e1′ ⟩ ≃log ⟨e2, e2′ ⟩ : τ1 ×τ1′ ; τ2 ×τ2′ .
Regarding compatibility of pairs, a tuple value can result either from an explicit merge or from a
coercion applied on some value. In the first case, the subcomponents of the tuple are disjoint witheach other and thus related (by Lemma 6.3). In the second case, given that the original expression
14 There is a second statement for the type checking direction of the two hypotheses.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:25is unambiguous and since coercions do not introduce ambiguity, the coercion application is also
unambiguous. However, because of the context dependency it is not easy to recover the original
expression and inspect it. For a similar reason, compatibility of abstraction is also hard to prove.
Logical Equivalence Entails Contextual Equivalence. Lastly, we need to show that any logicallyrelated target expressions are contextually equivalent. The proof is fairly straightforward.
Theorem 6.5 (Logical Eqivalence Entails Contextual Eqivalence).
If |Γ|; |Γ| ⊢ e1 ≃log e2 : |A|; |A|, then for any C : (Γ ⇒ A) 7→ (• ⇒ Nat) ⇝ D, there is a value• ⊢ v : Nat such that D{e1 } −→∗ v and D{e2 } −→∗ v .
Taken together, the (conditionally proven) fundamental property and the entailment of contextual
equivalence establish Theorem 6.1, the coherence of λiMP .
7

RELATED WORK

Resolution and Subtyping. The main contribution of our work is to unify resolution and subtyping into a single mechanism. Resolution is a common technique for automatically constructing
implicit values, such as Haskell’s type class dictionaries [Wadler and Blott 1989] or Scala’s implicits [Odersky 2010]. Subtyping is widely used in Object-Oriented programming and various
other type systems [Barendregt et al. 1983; Chen 2003; Gay and Hole 2005; Pierce and Sangiorgi
1996]. In our work we interpret resolution as a special case of coercive subtyping [Chen 2003],
where coercions are generated automatically in a type-directed fashion and then “inserted” into
the program. This fits well with the common type-directed elaboration style usually employed byresolution mechanisms, which work in a similar way.
As far as we are aware, the unification of subtyping and resolution is novel. Despite the fact that
languages like Scala integrate both mechanisms, only Jeffery [2019] combines both mechanisms
within his DIF calculus. Unfortunately—in contrast to λiMP —DIF’s subtyping is known to be undecidable. Furthermore, Jeffery does not study the coherence of DIF. Scala implicits [Odersky 2010] havemotivated other researchers to look into the foundations of the mechanism. However, all previous
work on implicit calculi, including the implicit calculus [Oliveira et al. 2012], Cochis [Schrijvers
et al. 2019] and the SI calculus [Odersky et al. 2017], do not account for subtyping. Instead, they all
focus on a System F [Reynolds 1974] based language (without subtyping), and model resolution
for such a language. One aspect that these implicit calculi preserve from Scala is a biased form of
resolution where innermost implicits are preferred. In contrast, our disjointness approach is morereminiscent of Haskell’s non-overlapping type class instances, which are unbiased.
The most common technique to algorithmically construct values by resolution, attributed
to Kowalski [1974], is commonly known as SLD resolution, or backwards chaining. Another technique, mostly used as a proof search method, is focusing [Andreoli 1992; Liang and Miller 2009;
Miller et al. 1989] and has been used to great effect in similar calculi (e.g. Cochis [Schrijvers et al.
2019] and Haskell with quantified class constraints [Bottu et al. 2017]) to create coherent resolution
mechanisms. Our subtyping algorithm of Section 5 closely resembles the focusing technique.
Coherence. Since Reynolds [1991] proved coherence for a calculus with intersection types, basedon denotational semantics, many researchers have studied it in a variety of typed calculi. Below wesummarize two commonly-found approaches in the literature: normal forms, and logical relations.
Breazu-Tannen et al. [1991] proved the coherence of a coercion translation from Fun [Cardelliand Wegner 1985] extended with recursive types to System F, by showing that any two typing
derivations of the same judgment are normalizable to the same form. Curien and Ghelli [1994]
presented a translation of System F ≤ into a calculus with explicit coercions and showed that any
derivations of the same judgment are translated to terms that are normalizable to a unique normal
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:26

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

form. Following the same approach, Schwinghammer [2009] proved the coherence of coercion
translation from Moggi’s computational lambda calculus [Moggi 1991] with subtyping.
Central to the first approach is to find a unique normal form for derivations. However, thisapproach cannot be directly applied to Curry-style calculi, i.e., where the lambda abstractions are
not type-annotated. Also, it does not work when the calculus has general recursion. Biernacki
and Polesiuk [2015] considered the coherence problem of coercion semantics. Their criterion for
coherence of the translation is contextual equivalence in the target calculus. They used a logicalrelation for establishing coherence for coercion semantics, applicable in a variety of calculi, including
delimited continuations and control-effect subtyping.
As far as we know, the first work to use logical relations to show the coherence for intersection
types and the merge operator was that of Bi et al. [2018] for NeColus, and later for Fi+ [Bi et al.
2019]. The BCD subtyping in both calculi (as well as our own) poses a non-trivial complication over
Bernacki and Polesiuk’s simple structural subtyping. In their system any two coercions between
given types are behaviorally equivalent in the target language, so their coherence reasoning can all
take place in the target language. In NeColus, Fi+ , and λiMP this is not the case; coercions can be
distinguished by arbitrary target programs but not those that are elaborations of source programs.
Hence, reasoning is restricted to the latter class, which is reflected in a more complicated notion ofcontextual equivalence and the logical relation’s non-trivial treatment of pairs. In addition to thesecomplications, our logical relation (and consequently the coherence proof) is significantly more
convoluted than that of NeColus and Fi+ , due to the non-compositionality of Modus Ponens.
Intersection Types and the Merge Operator. Forsythe [Reynolds 1988] is one of the first languages
with intersection types and a merge-like operator. However, merges in Forsythe cannot contain morethan one function; this restriction ensures that the language is coherent. Similarly, Castagna et al.’s
λ& calculus [Castagna et al. 1992] includes a special merge operator that works on functions only.
More recently, Dunfield [2012] showed significant expressiveness of type systems with intersection
types and a merge operator, at the cost of coherence. The limitation was addressed by Oliveira et al.
[2016], who introduced disjointness to ensure coherence. The combination of intersection types, amerge operator and parametric polymorphism—while achieving coherence—was first studied in
the Fi calculus [Alpuim et al. 2017]. Its successor, Fi+ [Bi et al. 2019] additionally incorporates BCD
subtyping [Barendregt et al. 1983], while remaining coherent. NeColus [Bi et al. 2018] has been thestarting point for our design of λiMP and incorporates intersection types, a merge operator, andBCD-style distributivity. Though neither NeColus nor λiMP accounts for parametric polymorphism,
this is a direction we would like to explore in the future.
BCD Type System and Decidability. The BCD type system was first introduced by Barendregt
et al. [1983]. It is derived from a filter lambda model in order to characterize exactly the strongly
normalizing terms. The BCD type system features a powerful subtyping relation, which serves as abase for ours. Bessai et al. [2014] showed how to type classes and mixins in a BCD-style record
calculus with the merge operator of Bracha and Cook [1990]. Their merge only operates on records,
and they only study a type assignment system. The decidability of BCD subtyping has been shownin several works [Kurata and Takahashi 1995; Pierce 1989; Rehof and Urzyczyn 2011; Statman 2014].
Laurent [2012] has formalized the relation in Coq in order to eliminate transitivity cuts from it, but
he does not deliver an algorithm. Based on the work of Statman [2014], Bessai et al. [2016] show aformally verified subtyping algorithm in Coq. Our algorithm follows the decision procedure of Bi
et al. [2018] and Pierce [1989]. However the addition of modus ponens requires significant changes
to the algorithm, and complicates the metatheory.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:27

Coq Type Classes. Coq employs a flexible type class system [Sozeau and Oury 2008b] that permits
overlapping instances and provides the user with the means to control resolution: Coq instances
are named and can be explicitly passed as arguments. The system poses no restrictions over the
implicit environment, like non-overlapping instances in Haskell or disjointness in λiMP . Therefore,
coherence becomes a choice and responsibility of the user.
In contrast, λiMP employs a stricter system that provides less control over subtyping. First, implicit
environments are not possible if not internally disjoint. Second, going against the intuition which
relates classes to types and instances to appropriately typed terms, expressions in λiMP can be rather
viewed as typed implicit environments, which can be composed with the use of the merge operator.
Passing a value to a function in λiMP can be seen as bringing an implicit environment in scope
within the body of the function. The function, then, can use that environment to infer values fromit, but it does not have access to the names of the instances contained in it. This is conceptuallydifferent from the named instances of Coq that can be optionally passed explicitly by the user. Last,
Coq uses a global environment to which instances are inserted at their point of declaration.
8

CONCLUSION AND FUTURE WORKThis paper has shown that, with a small extension, subtyping with intersection types can be used
to model resolution. We have materialized our ideas in the design of λiMP , a type-safe extension of
NeColus with the logical rule for Modus Ponens. This small extension significantly increases theexpressive power of λiMP ’s predecessor, allowing us to model features such as type class resolution
and first-class environments.
Future Work. A natural avenue for future work is the extension of λiMP with parametric polymorphism. When done naively, it can make the algorithm diverge and, like in Haskell, additional
conditions will have to be imposed to recover termination. Moreover, we believe that there arevarious applications for our work that we wish to explore in the future.
In a Haskell-like setting, our design would enable multiple implicit environments, instead of asingle global one. Such environments could be first-class, could be explicitly passed as arguments orreturned as a result, or could be composed to form larger implicit environments. The programmer
would then be able to choose which of the implicit environments to use for resolution.
In a Scala-like setting, where subtyping is present, our design helps clarify the interaction between
resolution and subtyping. This is important, from the practical point of view, since the interaction
between the two mechanisms has been a continuous source of compiler bugs15 . Furthermore, ourwork could also be interesting to offer a unified view of subtyping and resolution, which could
significantly reduce the implementation effort for the two mechanisms.
Finally, languages like TypeScript can support a merge operator for intersection types via an
encoding [Alpuim et al. 2017]. Since Typescript has subtyping, intersection types and the merge
operator (via an encoding), it would be quite interesting to explore the potential to extend thecurrent formulation of intersection types in TypeScript with the ideas of our work.
ACKNOWLEDGMENTS
We are grateful to anonymous reviewers that helped improving the presentation of our work. This
work has been sponsored by Hong Kong Research Grant Council projects number 17210617 and
17209519, Flemish Fund for Scientific Research project number G073816N and KU Leuven project
number C14/20/079.

15 See for example https://github.com/scala/bug/issues/2509 or https://github.com/scala/bug/issues/9764.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:28

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

REFERENCES
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In ESOP (Lecture Notes in Computer
Science, Vol. 10201). Springer, 1–28.
Nada Amin, Karl Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object
Types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th
Birthday (2016), 249–272. http://infoscience.epfl.ch/record/215280
Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent Object Types. (2012). http://infoscience.epfl.ch/record/
183030Jean-marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2(1992), 297–347.
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completenessof Type Assignment. J. Symb. Log. 48, 4 (1983), 931–940.
Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003. CDuce: An XML-Centric General-Purpose Language.
SIGPLAN Not. 38, 9 (Aug. 2003), 51–63. https://doi.org/10.1145/944746.944711
Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de’Liguoro. 2014. Typing Classes and Mixins with
Intersection Types. In ITRS (EPTCS, Vol. 177). 79–93.
Jan Bessai, Andrej Dudenhefner, Boris Düdder, and Jakob Rehof. 2016. Extracting a Formally Verified Subtyping Algorithm
for Intersection Types from Ideals and Filters (TYPES).
Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018. The Essence of Nested Composition. In ECOOP (LIPIcs, Vol. 109).
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 22:1–22:33.
Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019. Distributive Disjoint Polymorphism for Compositional Programming. In Programming Languages and Systems, Luís Caires (Ed.). Springer International Publishing, Cham,
381–409.
Dariusz Biernacki and Piotr Polesiuk. 2015. Logical Relations for Coherence of Effect Subtyping. In TLCA (LIPIcs, Vol. 38).
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 107–122.
Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017. Quantified Class
Constraints. SIGPLAN Not. 52, 10 (Sept. 2017), 148–161.
Gilad Bracha and William R. Cook. 1990. Mixin-based Inheritance. In OOPSLA/ECOOP. ACM, 303–311.
Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. 1991. Inheritance As Implicit Coercion. Inf.
Comput. 93, 1 (July 1991), 172–221.
Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv.
17, 4 (Dec. 1985), 471–523.
Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. 1992. A Calculus for Overloaded Functions with Subtyping.
SIGPLAN Lisp Pointers V, 1 (Jan. 1992), 182–192.
Gang Chen. 2003. Coercive subtyping for the Calculus of Constructions.. In POPL. 150–159.
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. 1981. Functional Characters of Solvable Terms. Math. Log. Q. 27 (1981),
45–58.
Pierre-Louis Curien and Giorgio Ghelli. 1994. Theoretical Aspects of Object-oriented Programming. MIT Press, Cambridge,
MA, USA, Chapter Coherence of Subsumption, Minimum Typing and Type-checking in F&Le;, 247–292.
Rowan Davies and Frank Pfenning. 2000. Intersection Types and Computational Effects. SIGPLAN Not. 35, 9 (Sept. 2000),
198–208. https://doi.org/10.1145/357766.351259
Dominique Devriese and Frank Piessens. 2011. On the bright side of type classes: instance arguments in Agda. In ICFP ’11:
Proceedings of the 16th ACM SIGPLAN international conference on Functional programming. ACM, 143–155.
Joshua Dunfield. 2007. Refined Typechecking with Stardust. In Proceedings of the 2007 Workshop on Programming Languages
Meets Program Verification (Freiburg, Germany) (PLPV ’07). Association for Computing Machinery, New York, NY, USA,
21–32. https://doi.org/10.1145/1292597.1292602
Jana Dunfield. 2012. Elaborating Intersection and Union Types. SIGPLAN Not. 47, 9 (Sept. 2012), 17–28.
Joshua Dunfield. 2015. Elaborating Evaluation-Order Polymorphism. SIGPLAN Not. 50, 9 (Aug. 2015), 256–268. https://doi.org/10.1145/2858949.2784744
Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 conference on
Programming language design and implementation. 268–277.
Simon J. Gay and Malcolm J. Hole. 2005. Subtyping for Session Types in the Pi Calculus. Acta Informatica 42, 2/3 (2005),
191–225.
J. Giesl, C. Aschermann, M. Brockschmidt, et al. 2017. Analyzing Program Termination and Complexity Automatically with
AProVE. J Autom Reasoning 58 (2017), 3–31.
Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. 1996. Type classes in Haskell. ACM
Transactions on Programming Languages and Systems 18, 2 (1996), 109–138.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

Resolution as Intersection Subtyping via Modus Ponens

206:29Alex Jeffery. 2019. Dependent Object Types with Implicit Functions. In Proceedings of the Tenth ACM SIGPLAN Symposium
on Scala (Scala ’19). Association for Computing Machinery, New York, NY, USA, 1–11.
Robert A. Kowalski. 1974. Predicate Logic as Programming Language. In IFIP Congress. North-Holland, 569–574.
Toshihiko Kurata and Masako Takahashi. 1995. Decidable Properties of Intersection Type Systems. In Proceedings of theSecond International Conference on Typed Lambda Calculi and Applications (TLCA ’95). Springer-Verlag, Berlin, Heidelberg,
297–311.
Olivier Laurent. 2012. Intersection Types with Subtyping by Means of Cut Elimination. Fundam. Inf. 121, 1-4 (Jan. 2012),
203–226.
Chuck Liang and Dale Miller. 2009. Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. Theor. Comput.
Sci. 410, 46 (2009), 4747–4768.
Zhaohui Luo. 1999. Coercive subtyping. Journal of Logic and Computation 9, 1 (1999), 105–130.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. 1989. Uniform Proofs As a Foundation for Logic
Programming. Technical Report.
Eugenio Moggi. 1991. Notions of Computation and Monads. Inf. Comput. 93, 1 (July 1991), 55–92.
Martin Odersky. 2010. The Scala language specification, version 2.8.
Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. 2017. Simplicitly:
Foundations and Applications of Implicit Function Types. Proc. ACM Program. Lang. 2, POPL (2017).
Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. 2010. Type Classes As Objects and Implicits. In Proceedings of
the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA ’10).
ACM, 341–360.
Bruno C.d.S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, and Kwangkeun Yi. 2012. The Implicit Calculus: A New
Foundation for Generic Programming. 47, 6 (2012).
Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016. Disjoint Intersection Types. SIGPLAN Not. 51, 9 (Sept. 2016),
364–377.
Benjamin C. Pierce. 1989. A Decision Procedure for the Subtype Relation on Intersection Types with Bounded Variables. Technical
Report. Carnegie Mellon University.
Benjamin C. Pierce. 1991. Programming with Intersection Types and Bounded Polymorphism. Ph.D. Dissertation. Carnegie
Mellon University. Available as School of Computer Science technical report CMU-CS-91-205.
Benjamin C. Pierce. 1997. Intersection types and bounded polymorphism. Mathematical Structures in Computer Science 7, 2
(1997), 129–193. https://doi.org/10.1017/S096012959600223X
B. C. Pierce and D. Sangiorgi. 1996. Typing and Subtyping for Mobile Processes. Math. Structures in Comput. Sci. 6, 5 (1996),
409–453.
Garrel Pottinger. 1980. A type assignment for the strongly normalizable λ-terms. To HB Curry: essays on combinatory logic,
lambda calculus and formalism (1980), 561–577.
Jef Raskin. 1974. FLOW: a teaching language for computer programming in the humanities. Computers and the Humanities
8, 4 (1974), 231–237.
Jakob Rehof and PawełUrzyczyn. 2011. Finite Combinatory Logic with Intersection Types. In Proceedings of the 10th
International Conference on Typed Lambda Calculi and Applications (Novi Sad, Serbia) (TLCA’11). Springer-Verlag, Berlin,
Heidelberg, 169–183.
John C. Reynolds. 1972. Definitional Interpreters for Higher-order Programming Languages. In Proceedings of the ACM
Annual Conference - Volume 2 (Boston, Massachusetts, USA) (ACM ’72). ACM, New York, NY, USA, 717–740.
John C. Reynolds. 1974. Towards a Theory of Type Structure. Lecture Notes in Computer Science, Vol. 19. 408–425.
John C. Reynolds. 1988. Preliminary Design of the Programming Language Forsythe. Technical Report. Carnegie Mellon
University.
John C. Reynolds. 1991. The Coherence of Languages with Intersection Types. In Proceedings of the International Conferenceon Theoretical Aspects of Computer Software (TACS ’91). Springer-Verlag, Berlin, Heidelberg, 675–700.
Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler, and Koar Marntirosian. 2019. COCHIS: Stable and coherent implicits.
Journal of Functional Programming 29 (2019), e3.
Jan Schwinghammer. 2009. Coherence of Subsumption for Monadic Types. J. Funct. Program. 19, 2 (March 2009), 157–172.
Matthieu Sozeau and Nicolas Oury. 2008a. First-Class Type Classes. In TPHOLs ’08: Proceedings of the 21st International
Conference on Theorem Proving in Higher Order Logics.
M. Sozeau and N. Oury. 2008b. First-Class Type Classes. In TPHOLs.
Rick Statman. 2014. A Finite Model Property for Intersection Types. In ITRS (EPTCS, Vol. 177). 1–9.
Philip Wadler. 2015. Propositions as Types. Commun. ACM 58, 12 (Nov. 2015), 75–84.
P. Wadler and S. Blott. 1989. How to Make Ad-hoc Polymorphism Less Ad Hoc. In Proceedings of the 16th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (Austin, Texas, USA) (POPL ’89). ACM, New York, NY, USA,
60–76.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.

206:30

Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias

Leo White, Frédéric Bour, and Jeremy Yallop. 2015. Modular implicits. Electronic Proceedings in Theoretical Computer Science
198 (12 2015).
Thomas Winant and Dominique Devriese. 2018. Coherent Explicit Dictionary Application for Haskell. In Proceedings of the
11th ACM SIGPLAN International Symposium on Haskell (St. Louis, MO, USA) (Haskell 2018). Association for Computing
Machinery, New York, NY, USA, 81–93.

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 206. Publication date: November 2020.