# Resolution as Intersection Subtyping via Modus Ponens

Koar Marntirosian<EMAIL_ADDRESS>,  Tom Schrijvers  KU
LeuvenLeuvenBelgium ,  Bruno C. d. S. Oliveira<EMAIL_ADDRESS>The University
of Hong KongHong Kong and  Georgios Karachalias<EMAIL_ADDRESS>TweagParisFrance

(2020)

###### Abstract.

Resolution and subtyping are two common mechanisms in programming languages.
Resolution is used by features 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 another
compatible 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 of resolution into subtyping enables _first-class
(implicit) environments_. The extension that recovers the power of resolution
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 _decidability_ of
algorithmic subtyping, and _coherence_. To materialize these ideas we develop
$\lambda_{i}^{\mathsf{MP}}$, a calculus that extends a previous calculus with
disjoint intersection types, and develop its metatheory in the Coq theorem
prover.

resolution, nested composition, family polymorphism, intersection types,
coherence, modus ponens

††copyright: rightsretained††journal: PACMPL††journalyear:
2020††journalvolume: 4††journalnumber: OOPSLA††article: 206††publicationmonth:
11††doi: 10.1145/3428274††ccs: Software and its engineering Functional
languages††ccs: Software and its engineering Object oriented languages††ccs:
Software and its engineering Semantics

##  1\. Introduction

_Subtyping_ is a well-known programming language feature. It is most notably
employed in object-oriented languages, but there are many other uses of
subtyping in the literature (Pierce and Sangiorgi, 1996; Barendregt et al.,
1983; Chen, 2003; Gay and Hole, 2005). Subtyping automatically converts 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 with intersection
types, it is possible to build overloaded functions such as:

      f : (Int -> Int) & (Char -> Char) = succ ,, toUpper

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 the type of the input, which triggers
an upcast induced by the subtyping relation. For instance, in the case 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 Blott, 1989) employ resolution to automatically _search_ for and
_compose_ instances of type classes. Resolution is also used by Scala’s
implicits (Oliveira et al., 2010). Many other programming languages have
mechanisms similar to type classes and implicits (Devriese and Piessens, 2011;
White et al., 2015; Sozeau and Oury, 2008a), 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 -> a
      instance 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, the Haskell 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 about type class instances. When class methods are used,
resolution searches the implicit environment to find 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 not allowed by
resolution mechanisms documented in the literature (Hall et al., 1996;
Schrijvers et al., 2019; Odersky et al., 2017; Wadler and Blott, 1989;
Oliveira et al., 2012). On the other hand, a key feature of resolution is its
ability to compose instances (or implicits). For instance, suppose that we
want 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 fact subsume forms of resolution. The extension that is necessary
to recover the power of resolution via subtyping is essentially the logical
rule for _modus ponens_ :

$\displaystyle\displaystyle{\hbox{\hskip
41.8163pt\vbox{\hbox{\hskip-41.81628pt\hbox{\hbox{$\displaystyle\displaystyle
A\vdash B\to C\qquad A\vdash B$}}}\vbox{}}}\over\hbox{\hskip
12.16313pt\vbox{\vbox{}\hbox{\hskip-12.16312pt\hbox{\hbox{$\displaystyle\displaystyle
A\vdash C$}}}}}}$ Modus Ponens

Modus ponens states that if from $A$ one can conclude both $B\to 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 power (and the essential
power of resolution). To accomplish this, we simply reinterpret entailment
($A\vdash 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 to be taken to retain desirable properties, such as
transitivity and decidability of subtyping. Our work builds and extends upon
the NeColus calculus (Bi et al., 2018)—or $\lambda_{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, comes with 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.111For example, GHC issue ticket 17295 is
a closely related problem, caused by an unexpected interaction between
resolution and overlapping “intersections”. Indeed, various foundational
calculi related to Scala formalize either subtyping (Amin et al., 2012; Amin
et al., 2016) or implicits (Oliveira et al., 2012; Schrijvers et al., 2019;
Odersky et al., 2017), 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, the integration
of resolution into subtyping enables _first-class (implicit) environments_.
That is, we can create (implicit) environments (encoded as intersection
types), use them as arguments, or return them 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 $\lambda_{i}^{\mathsf{MP}}$: a calculus
that extends the NeColus calculus (a calculus 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 $\lambda_{i}^{\mathsf{MP}}$ 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
$\lambda_{\mathit{c}}^{\mathsf{MP}}$, a simply typed lambda calculus extended
with coercions.

  * •

Algorithmic subtyping for $\lambda_{i}^{\mathsf{MP}}$: 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 $\lambda_{i}^{\mathsf{MP}}$ 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 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 $\lambda_{i}^{\mathsf{MP}}$: Establishing coherence
of $\lambda_{i}^{\mathsf{MP}}$ is also a challenging technical goal. The
addition of modus ponens makes it a lot harder due to the ability to compose
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). It is available online at
https://zenodo.org/record/4043646#.X4gBAHVfhjs.

##  2\. Background

This section introduces background on resolution, coercive subtyping,
intersection types and their use 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 logical inference they use are compatible. In this paper we
show how to extend this compatibility to the language design level and how to
ensure properties that, while typically of no concern for logical inference,
are key for programming languages, like coherence and decidable type checking.

In the sequent notation, the judgment $A\vdash B$ asserts that proposition $B$
can be inferred from proposition $A$. An inference rule provides a way to
construct a valid (or true) judgment. For instance, the inference rule

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
13.33328pt\vbox{\vbox{}\hbox{\hskip-13.33328pt\hbox{\hbox{$\displaystyle\displaystyle
A\vdash A$}}}}}}$

states that the judgment $A\vdash A$ (from $A$ follows $A$) is valid for any
proposition $A$.

The $A\vdash 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\vdash B$ then means that there exists a computable function that 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 been used to establish that judgment. For
instance, the evidence for the trivial $A\vdash A$ judgment above is the
identity function $\lambda x.x$. A more advanced inference rule is that for
transitivity

$\displaystyle\displaystyle{\hbox{\hskip
37.43462pt\vbox{\hbox{\hskip-37.4346pt\hbox{\hbox{$\displaystyle\displaystyle
A\vdash B$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle B\vdash
C$}}}}\vbox{}}}\over\hbox{\hskip
13.51453pt\vbox{\vbox{}\hbox{\hskip-13.51451pt\hbox{\hbox{$\displaystyle\displaystyle
A\vdash C$}}}}}}$

which allows to conclude $C$ from $A$ provided that $B$ can be concluded from
$A$ and $C$ from $B$. Given evidence $f$ for $B\vdash C$ and evidence $g$ for
$A\vdash B$, the evidence for $A\vdash C$ is $\lambda x.g\,(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\vdash B$ and
call $A$ and $B$ subtype and supertype respectively, rather than premise and
conclusion. Also we call the associated evidence of the 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 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
can therefore 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 $f$ that 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 then transforms 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 can take implicit parameters
which the type system fills in by searching values of the appropriate type in
the implicit environment. Elaboration turns those implicit parameters into
explicit ones. This behavior 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
$\lambda x.(f\,x)\,(g\,x)$ where $f$ is the evidence for $A\vdash B\to C$ and
$g$ for $A\vdash B$. The modus ponens rule can be applied recursively, e.g. to
establish $B$ from $A$ by modus ponens via $D\to 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

$\displaystyle P\to Q,Q\to U,P\vdash 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.

      object Test {
        class P                                        // proposition P
        class Q                                        // proposition Q
        class U                                        // proposition U

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

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

Figure 1. Encoding of the judgment $P\to Q,Q\to U,P\vdash U$ as a Scala
program.

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\to Q$, the definition of `g` encodes $Q\to U$ and the definition of
`p` 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
eventually by the synthesized expression `g(f(p))`.

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 and facts 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, and the conjunction of propositions in the environment as
intersections. Thus, the above judgment corresponds to:

$\displaystyle(P\to Q)\&(Q\to U)\&P<:U$

using 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 other types 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 $\lambda$-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 TypeScript222https://www.typescriptlang.org/,
Flow (Raskin, 1974), Ceylon333https://ceylon-lang.org/ 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 (Freeman and Pfenning, 1991; Davies and Pfenning, 2000; Dunfield,
2007). 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 to the 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 the construction 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:

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
22.9322pt\vbox{\vbox{}\hbox{\hskip-22.93219pt\hbox{\hbox{$\displaystyle\displaystyle
A\land B\vdash A$}}}}}}$ $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
23.2256pt\vbox{\vbox{}\hbox{\hskip-23.22559pt\hbox{\hbox{$\displaystyle\displaystyle
A\land B\vdash B$}}}}}}$

Here, we write $A\&B$, instead of $A\wedge B$, to denote an intersection type.
The runtime representation of values of type $A\&B$ is a tuple $(v,w)$ where
$v$ has type $A$ and $w$ has type $B$. The coercions associated with the two
inference rules are respectively $\pi_{1}$ and $\pi_{2}$, the projection on
respectively the first and second 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 this issue by
introducing a notion of disjoint intersection types.

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 top of 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\. Overview

This 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 on type classes and/or implicits and disjoint
intersection types. Then we explain the key idea of our work 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 for this 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 type class. 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 in the 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 must use 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, or Char 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.
have no common values), so their intersection is empty. With the merge
operator, however, it is possible to build values that inhabit such an
intersection type. For example:

      v : Int & Char = 1 ,, ’c’

In the definition of v, the merge operator (`,,`), is used to build a value of
type Int&Char from an integer and a character. In calculi with a merge
operator, intersection types are similar to conventional 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
while for 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 is easy 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) depending on what integer gets selected from the merge.

Disjoint intersection types (Oliveira et al., 2016) were proposed to solve
ambiguity problems in calculi 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, for previous 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 well-formed 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 distinct444 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., which is subsumed by a
disjointness check for merges.

##### Type class instances as merges

The fact that disjointness checking relates/subsumes to non-overlapping
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 the type ((Int -> Int) -> [Int] -> [Int]). Here, the merge
creates an overloaded function and checks 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 class
instances 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]

would not type check because `[Int] -> [Int]`, which is the type that `f`
needs to have, _is not_ a supertype 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 arguments or
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.555Though recent work by Winant and Devriese (2018) aims to rectify this.

To illustrate the use of first-class environments, consider a program that
processes data from a sensor measuring temperatures. The temperatures are
collected at fixed time intervals, and the sensor may fail to read
temperatures (for example due to temperatures being too high, low or to some
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 where
         read :: String -> a

to 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 syntax666The 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.. The read method provided by Read [Either String Int]
would require the string:

      "[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 not possible to use alternative instances for Either a b and
[a]. There are various workarounds for this issue, but none of these is ideal.

##### A solution using first-class environments

An alternative approach to solve this problem is to use merges to encode
first-class environments for instances of Read. We present such a solution
using the $\lambda_{i}^{\mathsf{MP}}$ calculus (assuming a few convenience
source language features). For the purposes of illustration and readability we
assume the following definition of Read:

      type Read a = String -> a

and 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:

      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 instances that 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 where application 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 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., 2012; Amin et al., 2016). Similarly, works that formalize
resolution typically do not account for subtyping (Oliveira et al., 2012;
Schrijvers et al., 2019; Odersky et al., 2017).

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 -> Bool

work 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
$\lambda_{i}^{\mathsf{MP}}$ 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 the fact 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 no longer possible in
$\lambda_{i}^{\mathsf{MP}}$ because one component may interact with another
through modus ponens.

This affects coherence: the NeColus disjointness constraint is insufficient
for $\lambda_{i}^{\mathsf{MP}}$ and needs to be tightened. Also the coherence
proof requires a considerably more complex canonicity relation that features a
form of context dependency to capture the possible interaction between type
components.

Algorithmic subtyping is also affected by this. The algorithm no longer
terminates naturally and requires 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 $\lambda_{i}^{\mathsf{MP}}$ and explain these
aspects in detail.

##  4\. The $\lambda_{i}^{\mathsf{MP}}$ Calculus

##### Syntax

Types | $\mathit{A},\mathit{B},C$ | $\Coloneqq$ | $\mathsf{Nat}\mid\top\mid\mathit{A}\rightarrow\mathit{B}\mid\mathit{A}\,\&\,\mathit{B}$
---|---|---|---
Terms | $E$ | $\Coloneqq$ | $\mathit{x}\mid\top\mid\mathit{i}\mid\lambda\mathit{x}.\,E\mid E_{{\mathrm{1}}}\,E_{{\mathrm{2}}}\mid E_{{\mathrm{1}}}\,,,\,E_{{\mathrm{2}}}\mid E:\mathit{A}$
Typing Contexts | $\Gamma$ | $\Coloneqq$ | $\bullet\mid\Gamma,\mathit{x}:\mathit{A}$
Figure 2. $\lambda_{i}^{\mathsf{MP}}$ Syntax

Figure 2 shows the syntax of $\lambda_{i}^{\mathsf{MP}}$. It is the same as
that of NeColus, but—for the sake of conciseness—without records. Types
$\mathit{A},\mathit{B},C$ include naturals $\mathsf{Nat}$, the top type
$\top$, function types $\mathit{A}\rightarrow\mathit{B}$ and intersection
types $\mathit{A}\,\&\,\mathit{B}$. Terms $E$ include variables $\mathit{x}$,
natural numbers $\mathit{i}$, the top value $\top$, function abstractions
$\lambda\mathit{x}.\,E$, function applications
$E_{{\mathrm{1}}}\,E_{{\mathrm{2}}}$, merges
$E_{{\mathrm{1}}}\,,,\,E_{{\mathrm{2}}}$ and (type-)annotated terms
$E:\mathit{A}$.

$\Gamma\vdash
E\Rightarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{e}$\/}$ Type
Synthesis

$\displaystyle\displaystyle{\hbox{\hskip
8.06252pt\vbox{\hbox{\hskip-8.0625pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
28.95145pt\vbox{\vbox{}\hbox{\hskip-28.95143pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\top\Rightarrow\top\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\langle\rangle$\/}$}}}}}}$
T-top $\displaystyle\displaystyle{\hbox{\hskip
8.06252pt\vbox{\hbox{\hskip-8.0625pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
27.93755pt\vbox{\vbox{}\hbox{\hskip-27.93753pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{i}\Rightarrow\mathsf{Nat}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{i}$\/}$}}}}}}$
T-nat $\displaystyle\displaystyle{\hbox{\hskip
31.37506pt\vbox{\hbox{\hskip-31.37505pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}:\mathit{A}\,{\in}\,\Gamma$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma$}}}}\vbox{}}}\over\hbox{\hskip
26.18755pt\vbox{\vbox{}\hbox{\hskip-26.18755pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{x}\Rightarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{x}$\/}$}}}}}}$
T-var $\displaystyle\displaystyle{\hbox{\hskip
79.9826pt\vbox{\hbox{\hskip-79.98259pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E_{{\mathrm{1}}}\Rightarrow\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e_{{\mathrm{1}}}}$\/}\qquad\Gamma\vdash
E_{{\mathrm{2}}}\Leftarrow\mathit{A_{{\mathrm{1}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e_{{\mathrm{2}}}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
41.65004pt\vbox{\vbox{}\hbox{\hskip-41.65002pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E_{{\mathrm{1}}}\,E_{{\mathrm{2}}}\Rightarrow\mathit{A_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e_{{\mathrm{1}}}}\,\mathit{e_{{\mathrm{2}}}}$\/}$}}}}}}$
T-app $\displaystyle\displaystyle{\hbox{\hskip
29.51878pt\vbox{\hbox{\hskip-29.51877pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E\Leftarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e}$\/}$}}}\vbox{}}}\over\hbox{\hskip
34.14378pt\vbox{\vbox{}\hbox{\hskip-34.14378pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E:\mathit{A}\Rightarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e}$\/}$}}}}}}$
T-anno $\displaystyle\displaystyle{\hbox{\hskip
102.06815pt\vbox{\hbox{\hskip-102.06815pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E_{{\mathrm{1}}}\Rightarrow\mathit{A_{{\mathrm{1}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e_{{\mathrm{1}}}}$\/}\qquad\Gamma\vdash
E_{{\mathrm{2}}}\Rightarrow\mathit{A_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e_{{\mathrm{2}}}}$\/}\qquad\vdash_{d}\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
60.81285pt\vbox{\vbox{}\hbox{\hskip-60.81284pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E_{{\mathrm{1}}}\,,,\,E_{{\mathrm{2}}}\Rightarrow\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\langle\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}\rangle$\/}$}}}}}}$
T-merge

$\Gamma\vdash
E\Leftarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{e}$\/}$ Type
Checking

$\displaystyle\displaystyle{\hbox{\hskip
35.8313pt\vbox{\hbox{\hskip-35.83128pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\mathit{x}:\mathit{A}\vdash
E\Leftarrow\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e}$\/}$}}}\vbox{}}}\over\hbox{\hskip
60.33133pt\vbox{\vbox{}\hbox{\hskip-60.33133pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\lambda\mathit{x}.\,E\Leftarrow\mathit{A}\rightarrow\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\lambda\mathit{x}:\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$}.\,\mathit{e}$\/}$}}}}}}$
T-abs $\displaystyle\displaystyle{\hbox{\hskip
58.39383pt\vbox{\hbox{\hskip-58.39381pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E\Rightarrow\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{e}$\/}\qquad\mathit{B}<:\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c}$\/}$}}}\vbox{}}}\over\hbox{\hskip
32.26878pt\vbox{\vbox{}\hbox{\hskip-32.26877pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
E\Leftarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c}\,\mathit{e}$\/}$}}}}}}$
T-sub

Figure 3. Bidirectional Typing

##### Bidirectional Typing

The type system of $\lambda_{i}^{\mathsf{MP}}$, shown in Figure 3, is
bidirectional and thus has two modes: the _synthesis_ mode ($\Rightarrow$) and
the _checking_ mode ($\Leftarrow$). The synthesis judgment $\Gamma\vdash
E\Rightarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{e}$\/}$ means
that we can synthesize type $\mathit{A}$ from expression $E$ in context
$\Gamma$, while the checking judgment $\Gamma\vdash
E\Leftarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{e}$\/}$ checks
whether $E$ has given type $\mathit{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 $\mathit{A_{{\mathrm{1}}}}$ and
$\mathit{A_{{\mathrm{2}}}}$ of the two subterms to be disjoint,
$\mathit{A_{{\mathrm{1}}}}*\mathit{A_{{\mathrm{2}}}}$, but also requires them
to be _internally_ disjoint, $\vdash_{d}\mathit{A_{{\mathrm{1}}}}$ and
$\vdash_{d}\mathit{A_{{\mathrm{2}}}}$, all summarised in the internal
disjointness premise
$\vdash_{d}\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}$ of the
rule. The two disjointness conditions are discussed in Section 4.4.

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

###  4.1. Declarative Subtyping

$\mathit{A}<:\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{c}$\/}$
Subtyping

S-refl $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
26.61005pt\vbox{\vbox{}\hbox{\hskip-26.61003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathsf{id}_{\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$}}$\/}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
57.06009pt\vbox{\hbox{\hskip-57.06009pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}<:\mathit{A_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{1}}}}$\/}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{2}}}}<:\mathit{A_{{\mathrm{3}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/}$}}}}\vbox{}}}\over\hbox{\hskip
29.54005pt\vbox{\vbox{}\hbox{\hskip-29.54004pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}<:\mathit{A_{{\mathrm{3}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{2}}}}\circ\mathit{c_{{\mathrm{1}}}}$\/}$}}}}}}$
S-trans S-top $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
29.48505pt\vbox{\vbox{}\hbox{\hskip-29.48505pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\top\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathsf{top}_{\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$}}$\/}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
56.68509pt\vbox{\hbox{\hskip-56.68509pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B_{{\mathrm{1}}}}<:\mathit{A_{{\mathrm{1}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{1}}}}$\/}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{2}}}}<:\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/}$}}}}\vbox{}}}\over\hbox{\hskip
42.93509pt\vbox{\vbox{}\hbox{\hskip-42.93507pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}<:\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{1}}}}\rightarrow\mathit{c_{{\mathrm{2}}}}$\/}$}}}}}}$
S-arr S-topArr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
33.01007pt\vbox{\vbox{}\hbox{\hskip-33.01006pt\hbox{\hbox{$\displaystyle\displaystyle\top<:\top\rightarrow\top\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathsf{top}_{\rightarrow}$\/}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
54.16508pt\vbox{\hbox{\hskip-54.16508pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{B_{{\mathrm{1}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{1}}}}$\/}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/}$}}}}\vbox{}}}\over\hbox{\hskip
40.81786pt\vbox{\vbox{}\hbox{\hskip-40.81784pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle$\/}$}}}}}}$
S-and S-andl $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
31.90157pt\vbox{\vbox{}\hbox{\hskip-31.90155pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}\,\&\,\mathit{B}<:\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{1}^{\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{B}\mbox{$\displaystyle\mid$}}$\/}$}}}}}}$
S-andr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
31.71407pt\vbox{\vbox{}\hbox{\hskip-31.71405pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}\,\&\,\mathit{B}<:\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{2}^{\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{B}\mbox{$\displaystyle\mid$}}$\/}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
73.72792pt\vbox{\vbox{}\hbox{\hskip-73.7279pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A}\rightarrow\mathit{B_{{\mathrm{1}}}})\,\&\,(\mathit{A}\rightarrow\mathit{B_{{\mathrm{2}}}})<:\mathit{A}\rightarrow\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathsf{dist}_{\rightarrow}^{\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{B_{{\mathrm{1}}}}\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{B_{{\mathrm{2}}}}\mbox{$\displaystyle\mid$}}$\/}$}}}}}}$
S-distArr $\displaystyle\displaystyle{\hbox{\hskip
60.86261pt\vbox{\hbox{\hskip-60.8626pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{B_{{\mathrm{1}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{1}}}}$\/}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/}$}}}}\vbox{}}}\over\hbox{\hskip
33.76157pt\vbox{\vbox{}\hbox{\hskip-33.76157pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}<:\mathit{B_{{\mathrm{2}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\mathit{c_{{\mathrm{2}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{1}}}}$\/}$}}}}}}$
S-mp

Figure 4. Declarative Specification of Subtyping

Figure 4 declaratively specifies the subtyping relation of
$\lambda_{i}^{\mathsf{MP}}$. The judgment
$\mathit{A}<:\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{c}$\/}$ states
that $\mathit{A}$ is a subtype of $\mathit{B}$ and produces coercion
$\mathit{c}$. Intuitively, $\mathit{c}$ captures the way to convert values of
type $\mathit{A}$ into values of type $\mathit{B}$.

##### BCD-Style Subtyping

All but the last subtyping rule are the same as those of NeColus and originate
from the BCD type system (Barendregt et al., 1983). Rules S-refl, S-trans and
S-top ensure that subtyping is a partial order with $\top$ 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_ (Bi et al., 2018), while the latter provides a more
unified treatment of top-like types in the meta-theory of the language:
without that rule, we cannot have
$\mathit{A}\rightarrow\mathit{B}<:\top\rightarrow\top$, if $\mathit{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 $\mathit{A}$ is a subtype of both
$\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}$ and of
$\mathit{B_{{\mathrm{1}}}}$, then it is also a subtype of
$\mathit{B_{{\mathrm{2}}}}$. While this extension of subtyping is conceptually
small, it has far-reaching consequences for the meta-theory of the language.

###  4.2. Elaboration Semantics

Following NeColus we assign a semantics to $\lambda_{i}^{\mathsf{MP}}$ by
means of an elaboration. The target of the elaboration is
$\lambda_{\mathit{c}}^{\mathsf{MP}}$, 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 the
implicit use of subtyping in $\lambda_{i}^{\mathsf{MP}}$ (rule T-sub).

Types | $\tau$ | $\Coloneqq$ | $\mathsf{Nat}\mid\langle\rangle\mid\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}\mid\tau_{{\mathrm{1}}}\times\tau_{{\mathrm{2}}}$
---|---|---|---
Terms | $\mathit{e}$ | $\Coloneqq$ | $\mathit{x}\mid\langle\rangle\mid\mathit{i}\mid\lambda\mathit{x}:\tau.\,\mathit{e}\mid\mathit{e_{{\mathrm{1}}}}\,\mathit{e_{{\mathrm{2}}}}\mid\langle\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}\rangle\mid\mathit{c}\,\mathit{e}$
Coercions | $\mathit{c}$ | $\Coloneqq$ | $\mathsf{id}_{\tau}\mid\mathit{c_{{\mathrm{1}}}}\circ\mathit{c_{{\mathrm{2}}}}\mid\mathsf{top}_{\tau}\mid\mathit{c_{{\mathrm{1}}}}\rightarrow\mathit{c_{{\mathrm{2}}}}\mid\pi_{1}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\mid\pi_{2}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\mid\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle\mid\mathsf{top}_{\rightarrow}\mid\mathsf{dist}_{\rightarrow}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}},\tau_{{\mathrm{3}}}}\mid$
|  |  | $\mathit{c_{{\mathrm{1}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color \leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{\ignorespaces}}{{\ignorespaces}{}}{{}}{} {\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{ }\ignorespaces {\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{ }\ignorespaces \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{2}}}}$
Typing contexts | $\Delta$ | $\Coloneqq$ | $\bullet\mid\Delta,\mathit{x}:\tau$
Values | $\mathit{v}$ | $\Coloneqq$ | $\langle\rangle\mid\mathit{i}\mid\lambda\mathit{x}:\tau.\,\mathit{e}\mid\langle\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\rangle\mid(\mathit{c_{{\mathrm{1}}}}\rightarrow\mathit{c_{{\mathrm{2}}}})\,\mathit{v}\mid\mathsf{top}_{\rightarrow}\,\mathit{v}\mid(\mathsf{dist}_{\rightarrow}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}},\tau_{{\mathrm{3}}}})\,\mathit{v}$
Figure 5. $\lambda_{\mathit{c}}^{\mathsf{MP}}$ Syntax

##### The $\lambda_{\mathit{c}}^{\mathsf{MP}}$ Calculus

Figure 5 shows the syntax of $\lambda_{\mathit{c}}^{\mathsf{MP}}$. This syntax
is nearly identical to that of NeColus’ target language. There are only two
differences, both situated in the coercions $\mathit{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 regular function terms—is that it facilitates the coherence
proof. Each coercion form corresponds to a particular 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 $\lambda_{i}^{\mathsf{MP}}$,
there is also a new corresponding coercion form
$\mathit{c_{{\mathrm{1}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{2}}}}$
in $\lambda_{\mathit{c}}^{\mathsf{MP}}$ to witness it. The second and minor
difference is that we have annotated 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 semantics of $\lambda_{\mathit{c}}^{\mathsf{MP}}$ to support the
new coercion form. The full definitions of these relations can be found in
Appendix A. The coercion typing rule CT-mp essentially replicates the
subtyping rule S-mp of Figure 4, but now with
$\lambda_{\mathit{c}}^{\mathsf{MP}}$ types. The new small-step rule, step-mp,
splits up an application of a modus ponens coercion
$\mathit{c_{{\mathrm{2}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{1}}}}$
to value $\mathit{v}$ into separate coercion applications
$\mathit{c_{{\mathrm{2}}}}\,\mathit{v}$ and
$\mathit{c_{{\mathrm{1}}}}\,\mathit{v}$ where the former should yield a
function that is applied to the latter.

$\mathit{c}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{2}}}$
Coercion Typing

$\displaystyle\displaystyle{\hbox{\hskip
58.15602pt\vbox{\hbox{\hskip-58.15602pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c_{{\mathrm{1}}}}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{2}}}\qquad\mathit{c_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,(\tau_{{\mathrm{2}}}\rightarrow\tau_{{\mathrm{3}}})$}}}\vbox{}}}\over\hbox{\hskip
30.64343pt\vbox{\vbox{}\hbox{\hskip-30.64343pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c_{{\mathrm{2}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{1}}}}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{3}}}$}}}}}}$
CT-mp

$\mathit{e_{{\mathrm{1}}}}\longrightarrow\mathit{e_{{\mathrm{2}}}}\vphantom{\mathit{c}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{2}}}}$
Small-Step Operational Semantics

$\displaystyle\displaystyle{\hbox{\hskip
44.95906pt\vbox{\hbox{\hskip-44.95906pt\hbox{\hbox{$\displaystyle\displaystyle\vphantom{(\mathit{c_{{\mathrm{2}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{1}}}})\,\mathit{v}\longrightarrow(\mathit{c_{{\mathrm{2}}}}\,\mathit{v})\,(\mathit{c_{{\mathrm{1}}}}\,\mathit{v})}$}}}\vbox{}}}\over\hbox{\hskip
46.20906pt\vbox{\vbox{}\hbox{\hskip-46.20906pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{c_{{\mathrm{2}}}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\mathit{c_{{\mathrm{1}}}})\,\mathit{v}\longrightarrow(\mathit{c_{{\mathrm{2}}}}\,\mathit{v})\,(\mathit{c_{{\mathrm{1}}}}\,\mathit{v})$}}}}}}$
step-mp

Figure 6. $\lambda_{\mathit{c}}^{\mathsf{MP}}$ Coercion Typing and Operational
Semantics (new rules)

How the features of $\lambda_{i}^{\mathsf{MP}}$ are mapped to
$\lambda_{\mathit{c}}^{\mathsf{MP}}$ is given in the grey parts of Figures 4
and 3. In those figures the meta-function $|\cdot|$ transforms
$\lambda_{i}^{\mathsf{MP}}$ types to $\lambda_{\mathit{c}}^{\mathsf{MP}}$
types, and extends naturally to typing contexts. Its definition is in Appendix
B.

###  4.3. Target and Elaboration Metatheory

We have formally investigated the metatheory of our calculus,
$\lambda_{i}^{\mathsf{MP}}$, and of its target language,
$\lambda_{\mathit{c}}^{\mathsf{MP}}$, and mechanised it in Coq.

##### Target Language

Firstly, we have proven that the key metatheoretical properties of
$\lambda_{\mathit{c}}^{\mathsf{MP}}$ are not invalidated by the new coercion
form. Indeed, $\lambda_{\mathit{c}}^{\mathsf{MP}}$ is type safe:

###### Theorem 4.1 (Preservation).

If $\bullet\vdash\mathit{e}:\tau$ and
$\mathit{e}\longrightarrow\mathit{e^{\prime}}$, then
$\bullet\vdash\mathit{e^{\prime}}:\tau$.

###### Theorem 4.2 (Progress).

If $\bullet\vdash\mathit{e}:\tau$, then either $\mathit{e}$ is a value or
there is an $\mathit{e^{\prime}}$ such that
$\mathit{e}\longrightarrow\mathit{e^{\prime}}$.

Moreover, every well-typed $\lambda_{\mathit{c}}^{\mathsf{MP}}$ term is
normalising.

###### Theorem 4.3 (Normalisation).

If $\bullet\vdash\mathit{e}:\tau$ then there exists a value $\mathit{v}$ such
that $\mathit{e}\longrightarrow^{*}\mathit{v}$.

Here $\longrightarrow^{*}$, is the reflexive transitive closure of
$\longrightarrow$.

##### Elaboration

Also, the elaboration of $\lambda_{i}^{\mathsf{MP}}$ to
$\lambda_{\mathit{c}}^{\mathsf{MP}}$ preserves well-typing.

###### Theorem 4.4 (Coercions Preserve Types).

If
$\mathit{A}<:\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{c}$\/}$, then
$\mathit{c}\vdash\mbox{$\mid$}\mathit{A}\mbox{$\mid$}\,\triangleright\,\mbox{$\mid$}\mathit{B}\mbox{$\mid$}$.

###### Theorem 4.5 (Elaboration Preserves Types).

  * •

If $\Gamma\vdash
E\Rightarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{e}$\/}$, then
$\mbox{$\mid$}\Gamma\mbox{$\mid$}\vdash\mathit{e}:\mbox{$\mid$}\mathit{A}\mbox{$\mid$}$.

  * •

If $\Gamma\vdash
E\Leftarrow\mathit{A}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{e}$\/}$, then
$\mbox{$\mid$}\Gamma\mbox{$\mid$}\vdash\mathit{e}:\mbox{$\mid$}\mathit{A}\mbox{$\mid$}$.

The meta-function $\mbox{$\mid$}\Gamma\mbox{$\mid$}$ translates a source
typing context $\Gamma$ to a target one. The full definition can be found in
Appendix B.

###  4.4. Disjointness Conditions

$\mathit{A}*\mathit{B}$ Disjointness

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
10.12503pt\vbox{\vbox{}\hbox{\hskip-10.12502pt\hbox{\hbox{$\displaystyle\displaystyle\top*\mathit{A}$}}}}}}$
D-topL $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
9.12503pt\vbox{\vbox{}\hbox{\hskip-9.12502pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}*\top$}}}}}}$
D-topR $\displaystyle\displaystyle{\hbox{\hskip
29.14507pt\vbox{\hbox{\hskip-29.14507pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}*\mathit{B}\qquad\mathit{A_{{\mathrm{2}}}}*\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
20.09644pt\vbox{\vbox{}\hbox{\hskip-20.09644pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}*\mathit{B}$}}}}}}$
D-andL $\displaystyle\displaystyle{\hbox{\hskip
29.14507pt\vbox{\hbox{\hskip-29.14507pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}*\mathit{B_{{\mathrm{1}}}}\qquad\mathit{A}*\mathit{B_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
19.90894pt\vbox{\vbox{}\hbox{\hskip-19.90894pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}*\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}$}}}}}}$
D-andR $\displaystyle\displaystyle{\hbox{\hskip
10.07253pt\vbox{\hbox{\hskip-10.07253pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A_{{\mathrm{2}}}}*\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
21.45755pt\vbox{\vbox{}\hbox{\hskip-21.45753pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}})*\mathit{B}$}}}}}}$
D-mpL $\displaystyle\displaystyle{\hbox{\hskip
10.07253pt\vbox{\hbox{\hskip-10.07253pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}*\mathit{B_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
21.27005pt\vbox{\vbox{}\hbox{\hskip-21.27003pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}*(\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}})$}}}}}}$
D-mpR

$\vdash_{d}\mathit{A}$ Internal Disjointness

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
12.68665pt\vbox{\vbox{}\hbox{\hskip-12.68665pt\hbox{\hbox{$\displaystyle\displaystyle\vdash_{d}\mathsf{Nat}$}}}}}}$
ID-nat $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
8.81165pt\vbox{\vbox{}\hbox{\hskip-8.81163pt\hbox{\hbox{$\displaystyle\displaystyle\vdash_{d}\top$}}}}}}$
ID-top $\displaystyle\displaystyle{\hbox{\hskip
8.49915pt\vbox{\hbox{\hskip-8.49913pt\hbox{\hbox{$\displaystyle\displaystyle\vdash_{d}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
14.12416pt\vbox{\vbox{}\hbox{\hskip-14.12415pt\hbox{\hbox{$\displaystyle\displaystyle\vdash_{d}\mathit{A}\rightarrow\mathit{B}$}}}}}}$
ID-arr $\displaystyle\displaystyle{\hbox{\hskip
43.99834pt\vbox{\hbox{\hskip-43.99832pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{A}*\mathit{B}\qquad\vdash_{d}\mathit{A}\qquad\vdash_{d}\mathit{B}$}}}\vbox{}}}\over\hbox{\hskip
17.26305pt\vbox{\vbox{}\hbox{\hskip-17.26305pt\hbox{\hbox{$\displaystyle\displaystyle\vdash_{d}\mathit{A}\,\&\,\mathit{B}$}}}}}}$
ID-and

Figure 7. 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 $\mathit{A}*\mathit{B}$ conservatively captures the
notion that the common supertypes of $\mathit{A}$ and $\mathit{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 rule777This rule states
that two arrow types are disjoint if their codomains are disjoint.,

$\displaystyle\displaystyle{\hbox{\hskip
11.14503pt\vbox{\hbox{\hskip-11.14502pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{B_{{\mathrm{1}}}}*\mathit{B_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
33.91507pt\vbox{\vbox{}\hbox{\hskip-33.91505pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{1}}}})*(\mathit{A_{{\mathrm{2}}}}\rightarrow\mathit{B_{{\mathrm{2}}}})$}}}}}}$
D-arr

they cannot be used to recover the NeColus axioms
$\mathsf{Nat}*(\mathit{A}\rightarrow\mathit{B})$ and
$(\mathit{A}\rightarrow\mathit{B})*\mathsf{Nat}$. On the contrary,
$\lambda_{i}^{\mathsf{MP}}$ does not consider the types $\mathsf{Nat}$ and
$\mathsf{Bool}\rightarrow\mathsf{Nat}$ to be disjoint. For the sake of
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
$((\mathsf{true}\,,,\,(\lambda\mathit{x}.\,1):\mathsf{Bool}\rightarrow\mathsf{Nat})\,,,\,2):\mathsf{Nat}$.
The elaborated form of the merge expression on the left of the outer type
annotation is the tuple
$\langle\langle\mathsf{true},\lambda\mathit{x}:\mathsf{Bool}.\,1\rangle,2\rangle$.
The outer type annotation will trigger the subtyping mechanism, first via rule
T-anno and then through rule T-sub, in order to produce a value of type
$\mathsf{Nat}$. This example is ambiguous, because it can produce—through
subtyping—two different values of this type: $2$ by projecting on the right
component of the outer tuple, and $1$ by projecting on the left component of
the outer tuple and using modus ponens to apply
$(\lambda\mathit{x}:\mathsf{Bool}.\,1)$ to $\mathsf{true}$. The respective
subtyping derivations and the coercions they generate are shown in Figure 8.

Example (a)

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
53.10298pt\vbox{\vbox{}\hbox{\hskip-53.10298pt\hbox{\hbox{$\displaystyle\displaystyle(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))\,\&\,\mathsf{N}<:\mathsf{N}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{2}^{\mathsf{B}\times(\mathsf{B}\rightarrow\mathsf{N}),\mathsf{N}}$\/}$}}}}}}$
S-andr

Example (b)

$\displaystyle\displaystyle{\hbox{\hskip
166.54507pt\vbox{\hbox{\hskip-166.54507pt\hbox{\hbox{$\displaystyle\displaystyle\raise
10.59721pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
70.61691pt\vbox{\vbox{}\hbox{\hskip-70.6169pt\hbox{\hbox{$\displaystyle\displaystyle(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))\,\&\,\mathsf{N}<:\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{1}^{\mathsf{B}\times(\mathsf{B}\rightarrow\mathsf{N}),\mathsf{N}}$\/}$}}}}}}$}}\hbox{}$
}$}\hskip 5.0pt\hbox{\hbox{$\displaystyle\displaystyle\raise
16.59721pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\vbox{\hbox{\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})<:\mathsf{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{1}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}}$\/}}$}\hskip
5.0pt\hbox{\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})<:\mathsf{B}\rightarrow\mathsf{N}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{2}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}}$\/}}$}}}}}\hrule
height=0.0pt,depth=2.0pt,width=0.0pt\vbox{\hbox{\hbox{\hbox{$\displaystyle\displaystyle{\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})<:\mathsf{B}\rightarrow\mathsf{N}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{2}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}}$\/}}$}}}\hrule
height=0.0pt,depth=2.0pt,width=0.0pt\vbox{}}}}\over\hbox{\vbox{\vbox{}\hrule
height=0.0pt,depth=2.0pt,width=0.0pt\hbox{\hbox{\hbox{$\displaystyle\displaystyle\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})<:\mathsf{N}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow\pi_{2}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\pi_{1}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}}$\/}$}}}}}}$}}\hbox{\hbox{\hbox{}\hbox
to0.0pt{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
S-mp}}}}}$\hss}}\hskip-3.0pt}$ }$}}}}\vbox{}}}\over\hbox{\hskip
76.42226pt\vbox{\vbox{}\hbox{\hskip-76.42226pt\hbox{\hbox{$\displaystyle\displaystyle(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))\,\&\,\mathsf{N}<:\mathsf{N}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow(\pi_{2}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\pi_{1}^{\mathsf{B},\mathsf{B}\rightarrow\mathsf{N}})\circ\pi_{1}^{\mathsf{B}\times(\mathsf{B}\rightarrow\mathsf{N}),\mathsf{N}}$\/}$}}}}}}$
S-trans

Figure 8. Example subtyping derivations. Types $\mathsf{Bool}$ and
$\mathsf{Nat}$ are abbreviated here as $\mathsf{B}$ and $\mathsf{N}$,
respectively.

For similar reasons, expressions
$(\lambda\mathit{x}.\,1):\mathsf{Bool}\rightarrow\mathsf{Nat}\,,,\,(2\,,,\,\mathsf{true})$
and
$(2\,,,\,(\lambda\mathit{x}.\,1):\mathsf{Bool}\rightarrow\mathsf{Nat})\,,,\,\mathsf{true}$
are also ambiguous. In all three cases, the component types of a merge will
not be disjoint.

The two new rules D-mpL and D-mpR bring the notion of disjointness between two
types closer to the notion of no-overlaps between two (or more) instances.
Types $\mathit{B}$ and $\mathit{A}\rightarrow\mathit{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\,,,\,(\lambda\mathit{x}.\,1):\mathsf{Bool}\rightarrow\mathsf{Nat}$ of type
$\mathsf{Nat}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{Nat})$, the types
$\mathsf{Nat}$ and $\mathsf{Bool}\rightarrow\mathsf{Nat}$ overlap, but there
is only one applicable way to resolve a value of type $\mathsf{Nat}$, because
there is no $\mathsf{Bool}$ value to feed to the function
$(\lambda\mathit{x}.\,1):\mathsf{Bool}\rightarrow\mathsf{Nat}$. Secondly,
expressions of an overlapping type are harmless when all possible resolution
paths for a wanted type result in the same 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:\mathsf{Nat}\,\&\,\mathsf{Nat}$, which is accepted and semantically same.
Its full typing derivation is in Appendix E.

##### Internal Disjointness

The internal disjointness predicate, $\vdash_{d}\mathit{A}$, requires that the
two components of any intersection type that appear in $\mathit{A}$ are
disjoint. Intuitively, $\vdash_{d}\mathit{A}$ ensures that if
$\mathit{A}<:\mathit{B}$, then $\mathit{B}$ 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 that involves nested merges interleaved with
subtyping. Here is a minimal ambiguous example to illustrate the problem:

$\displaystyle((\mathsf{true}\,,,\,\mathsf{b2n}):\mathsf{Nat}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{Nat})\,,,\,\mathsf{false}):\mathsf{Nat}$

This example features $\mathsf{b2n}$, which we assume to be a built-in
function of type $\mathsf{Bool}\rightarrow\mathsf{Nat}$ that maps
$\mathsf{true}$ to $1$ and $\mathsf{false}$ to $0$. The inner merge has type
$\mathsf{Bool}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{Nat})$, but is converted
to type $\mathsf{Nat}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{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) the
subterm $\mathsf{true}\,,,\,\mathsf{b2n}$. The corresponding value is
$1\,,,\,\mathsf{b2n}$, which could not be written explicitly because
$\mathsf{Nat}$ and $\mathsf{Bool}\rightarrow\mathsf{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\,,,\,\mathsf{b2n}$ potentially
produces two different values of type $\mathsf{Nat}$, one of those requires a
$\mathsf{Bool}$, which is not available at this point.

However, the outer merge with $\mathsf{false}$ provides the missing
$\mathsf{Bool}$ value, making the outer $\mathsf{Nat}$ type annotation
ambiguously yield both $0$ and $1$ as possible results. The disjointness check
rejects none of 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\,,,\,\mathsf{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 $\mathit{A}\rightarrow\mathit{B}$ that potentially is
a supertype of some internally disjoint type, say $\mathit{A^{\prime}}$
(formally, $\mathit{A^{\prime}}<:\mathit{A}\rightarrow\mathit{B}$). If
$\mathit{A^{\prime}}$ is not a subtype of $\mathit{A}$ (thus,
$\mathit{A^{\prime}}<:\mathit{A}$ does not hold), then rule S-mp does not
apply. In fact, it becomes impossible to implicitly produce $\mathit{B}$ from
$\mathit{A^{\prime}}$ and, therefore, unnecessary to demand internal
disjointness of $\mathit{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 function of type
$\mathit{A}\rightarrow\mathit{B}$ is unambiguous if it outputs unambiguous
values of type $\mathit{B}$, given unambiguous input values of type
$\mathit{A}$. This implies the requirement that $\mathit{A}$ is also
internally disjoint. However, at this point, only values produced implicitly
from $\mathit{A^{\prime}}$ are considered, and these can only contain harmless
ambiguity. Indeed, explicit values can be added only through the merge
operator, thus falling under rule ID-and. Thus, unambiguity is ensured for
$\mathit{A}$.

##  5\. Algorithmic Subtyping

In 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 ($\mathit{A_{{\mathrm{2}}}}$ in the
former, and $\mathit{B_{{\mathrm{1}}}}$ 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
$\mathit{A}<:\mathit{B}$ is to structurally analyze (focus on) $\mathit{B}$,
and when it is stripped down to a base type do the same for $\mathit{A}$. This
task is performed by two mutually-recursive judgments, the first focusing on
the _right_ type $\mathit{B}$, and the second focusing on the _left_ type
$\mathit{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 the additional 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
come up 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

${A}\prec:{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{c}$\/}$ Algorithmic
Subtyping

$\displaystyle\displaystyle{\hbox{\hskip
27.16753pt\vbox{\hbox{\hskip-27.16753pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathit{c}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
20.06253pt\vbox{\vbox{}\hbox{\hskip-20.06253pt\hbox{\hbox{$\displaystyle\displaystyle{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathit{c}}$\/}$}}}}}}$
A-main

${\mathcal{L}}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathit{c}}$\/}$ Right
Focusing

$\displaystyle\displaystyle{\hbox{\hskip
69.00009pt\vbox{\hbox{\hskip-69.00009pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\mathit{B_{{\mathrm{1}}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathit{c_{{\mathrm{1}}}}}$\/}\qquad{\mathcal{L}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\mathit{B_{{\mathrm{2}}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathit{c_{{\mathrm{2}}}}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
63.159pt\vbox{\vbox{}\hbox{\hskip-63.15898pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\llbracket{\mathcal{L}}\rrbracket_{\&}^{{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}\circ\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle}$\/}$}}}}}}$
AR-and $\displaystyle\displaystyle{\hbox{\hskip
34.38495pt\vbox{\hbox{\hskip-34.38495pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L},\mathit{B_{{\mathrm{1}}}}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\mathit{B_{{\mathrm{2}}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{c}$\/}$}}}\vbox{}}}\over\hbox{\hskip
35.38496pt\vbox{\vbox{}\hbox{\hskip-35.38495pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\mathit{B_{{\mathrm{1}}}}\rightarrow\mathit{B_{{\mathrm{2}}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{c}$\/}$}}}}}}$
AR-arr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
50.67508pt\vbox{\vbox{}\hbox{\hskip-50.67506pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\top}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\llbracket{\mathcal{L}}\rrbracket_{\top}\circ\mathsf{top}_{\mbox{$\displaystyle\mid$}\mathit{A}\mbox{$\displaystyle\mid$}}}$\/}$}}}}}}$
AR-top $\displaystyle\displaystyle{\hbox{\hskip
55.40738pt\vbox{\hbox{\hskip-55.40736pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}};{[]};{A};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{(\lambda
c.c)}$\/}\vdash_{\text{L}}{A}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
46.14256pt\vbox{\vbox{}\hbox{\hskip-46.14255pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}}\mathrel{\vdash_{\text{R}}}{A}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}[\mathsf{id}_{\mbox{$\displaystyle\mid$}\mathsf{Nat}\mbox{$\displaystyle\mid$}}]}$\/}$}}}}}}$
AR-nat

${\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}${\mathcal{X}}$\/}\vdash_{\text{L}}{A}\prec:{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$
Left Focusing

AL-nat $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
53.33508pt\vbox{\vbox{}\hbox{\hskip-53.33507pt\hbox{\hbox{$\displaystyle\displaystyle{[]};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{\mathcal{X}}$\/}\vdash_{\text{L}}{\mathsf{Nat}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}}$\/}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
72.49811pt\vbox{\hbox{\hskip-72.49811pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{(\lambda
c.\mathcal{X}[\hbox{}\mathit{c}\circ\pi_{1}^{\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{2}}}}\mbox{$\displaystyle\mid$}}\hbox{}])}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{1}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
61.62448pt\vbox{\vbox{}\hbox{\hskip-61.62448pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{\mathcal{X}}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$}}}}}}$
AL-and1 $\displaystyle\displaystyle{\hbox{\hskip
72.49811pt\vbox{\hbox{\hskip-72.49811pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{(\lambda
c.\mathcal{X}[\hbox{}\mathit{c}\circ\pi_{2}^{\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{2}}}}\mbox{$\displaystyle\mid$}}\hbox{}])}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
61.62448pt\vbox{\vbox{}\hbox{\hskip-61.62448pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{\mathcal{X}}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{1}}}}\,\&\,\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$}}}}}}$
AL-and2 $\displaystyle\displaystyle{\hbox{\hskip
117.67026pt\vbox{\hbox{\hskip-117.67026pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\mathit{B_{{\mathrm{1}}}}}\prec:{\mathit{A_{{\mathrm{1}}}}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{c_{1}}$\/}\qquad{\mathcal{L}};{\mathcal{M},\mathit{B_{{\mathrm{1}}}}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{(\lambda
c.\mathcal{X}[c_{1}\to
c])}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$}}}\vbox{}}}\over\hbox{\hskip
64.1831pt\vbox{\vbox{}\hbox{\hskip-64.18309pt\hbox{\hbox{$\displaystyle\displaystyle{\mathit{B_{{\mathrm{1}}}},\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{\mathcal{X}}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$}}}}}}$
AL-arr $\displaystyle\displaystyle{\hbox{\hskip
177.59712pt\vbox{\hbox{\hskip-177.59712pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\mathit{A_{{\mathrm{0}}}}}\prec:{(\mathcal{M}\to\to\mathit{A_{{\mathrm{1}}}})}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathit{c_{{\mathrm{2}}}}}$\/}\qquad{\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{\mathcal{X}^{\prime}}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime\prime}}$\/}$}\hskip
18.00003pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\mathcal{X}^{\prime}=(\lambda
c.\llbracket{\mathcal{M}}\rrbracket_{\&}^{{(\mathit{c}\circ(\pi_{1}^{\mbox{$\displaystyle\mid$}(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}})\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\displaystyle\mid$}}\,\vbox{\hbox{\leavevmode\hbox{\set@color
\leavevmode\hbox to9.5pt{\vbox to4.95pt{\pgfpicture\makeatletter\hbox{\hskip
0.2pt\lower 0.36905pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\ignorespaces\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{\ignorespaces}}{{\ignorespaces}{}}{{}}{}
{\ignorespaces}{}{}\pgfsys@moveto{0.0pt}{2.84523pt}\pgfsys@lineto{9.10474pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces
{\ignorespaces}{{}}{}{{{}}{\ignorespaces}{}{\ignorespaces}{}{}{}{}{}}{}\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@moveto{6.82855pt}{2.84523pt}\pgfsys@curveto{6.82855pt}{4.10234pt}{5.80948pt}{5.12141pt}{4.55237pt}{5.12141pt}\pgfsys@curveto{3.29526pt}{5.12141pt}{2.27618pt}{4.10234pt}{2.27618pt}{2.84523pt}\pgfsys@curveto{2.27618pt}{1.58812pt}{3.29526pt}{0.56905pt}{4.55237pt}{0.56905pt}\pgfsys@curveto{5.80948pt}{0.56905pt}{6.82855pt}{1.58812pt}{6.82855pt}{2.84523pt}\pgfsys@closepath\pgfsys@moveto{4.55237pt}{2.84523pt}\pgfsys@stroke\pgfsys@invoke{
}\ignorespaces \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{\ignorespaces}{\ignorespaces}{\ignorespaces}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}\,\pi_{2}^{\mbox{$\displaystyle\mid$}(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}})\mbox{$\displaystyle\mid$},\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\displaystyle\mid$}}))},{(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}})},{\mathit{A_{{\mathrm{1}}}}}}\circ\langle\mathcal{X}[\mathsf{id}_{\mbox{$\displaystyle\mid$}\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\mbox{$\displaystyle\mid$}}],\mathit{c_{{\mathrm{2}}}}\rangle)$\/}$}}}}\vbox{}}}\over\hbox{\hskip
59.17859pt\vbox{\vbox{}\hbox{\hskip-59.17857pt\hbox{\hbox{$\displaystyle\displaystyle{\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle{\mathcal{X}}$\/}\vdash_{\text{L}}{\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}}\prec:{\mathsf{Nat}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\displaystyle\rightsquigarrow{\mathcal{X}^{\prime\prime}}$\/}$}}}}}}$
AL-mp

Figure 9. Algorithmic Subtyping

In Figure 9, we present the algorithmic subtyping judgment
${\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathit{c}}$\/}$; the
algorithmic counterpart of the declarative judgment
$\mathit{A}<:\mathit{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{c}$\/}$ of
Section 4.1. The main judgment is defined in terms of two auxiliary, mutually-
recursive judgments
${\mathcal{L}}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathit{c}}$\/}$ and
${\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}${\mathcal{X}}$\/}\vdash_{\text{L}}{A}\prec:{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$,
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 $\mathcal{L}$ and $\mathcal{M}$ stand for queues of types. The
algorithm uses them to capture the left-hand sides of arrow types. Operation
$\mathcal{L}\to\to\mathit{B}$ converts a queue $\mathcal{L}$ back into a type,
given the right-hand side type $\mathit{B}$. It is inductively defined as
follows:

$\displaystyle\small[]\to\to\mathit{B}=\mathit{B}\qquad\qquad(\mathit{A},\mathcal{L})\to\to\mathit{B}=\mathit{A}\rightarrow(\mathcal{L}\to\to\mathit{B})$

Meta-variable $\mathcal{X}$ denotes _algorithmic contexts_. An algorithmic
context is merely the Cayley representation of a coercion: a function from
coercions to coercions. Given a coercion $\mathit{c}$, we can convert an
algorithmic context $\mathcal{X}$ into a coercion by function application,
denoted as $\mathcal{X}[\mathit{c}]$. The role of algorithmic contexts is
explained in Section 5.1.2 where we discuss the left-focusing rules.888In both
our mechanization and implementation of the algorithm we use a
defunctionalized (Reynolds, 1972) representation of algorithmic contexts,
which we then interpret as actual functions between coercions.

####  5.1.1. Right Focusing

As mentioned earlier, the first judgment
(${\mathcal{L}}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathit{c}}$\/}$)
structurally analyzes $\mathit{B}$, until it is stripped down to a base type
($\mathsf{Nat}$ or $\top$). The accumulating parameter $\mathcal{L}$ captures
the domains of arrows encountered in $\mathit{B}$, such that the following
holds:

###### Lemma 5.1 (Soundness of Right Focusing).

If
${\mathcal{L}}\mathrel{\vdash_{\text{R}}}{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathit{c}}$\/}$ then
$\mathit{A}<:(\mathcal{L}\to\to\mathit{B})\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{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-
and decomposes 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 $\mathcal{L}$ and removed again
later, left-to-right, as arrows are encountered in $\mathit{A}$ (see rule AL-
arr below). There are two base cases: either $\mathit{B}=\top$ or
$\mathit{B}=\mathsf{Nat}$. Rule AR-top handles the first case, where subtyping
directly produces a coercion with the use of the meta-function
$\llbracket{\mathcal{L}}\rrbracket_{\top}$, discussed in the next paragraph.
If $\mathit{B}=\mathsf{Nat}$, then we perform structural analysis on
$\mathit{A}$, using judgment
${\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}${\mathcal{X}}$\/}\vdash_{\text{L}}{\mathit{A}}\prec:{\mathit{B}}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$,
which we elaborate on in Section 5.1.2.

##### Coercion Generation

The elaboration side is a bit more involved. Coercion generation can be
understood via Lemma 5.1 and works as follows. Rule AR-and deals with
intersection types. By induction we have that

$\left.\begin{array}[]{l}\mathit{A}<:(\mathcal{L}\to\to\mathit{B_{{\mathrm{1}}}})\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{c_{{\mathrm{1}}}}$\/}\\\
\mathit{A}<:(\mathcal{L}\to\to\mathit{B_{{\mathrm{2}}}})\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/}\\\
\end{array}\right\\}\implies\mathit{A}<:(\mathcal{L}\to\to\mathit{B_{{\mathrm{1}}}})\,\&\,(\mathcal{L}\to\to\mathit{B_{{\mathrm{2}}}})\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle$\/}$

We finish the transition to
$\mathcal{L}\to\to(\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}})$
using meta-function
$\llbracket{\mathcal{L}}\rrbracket_{\&}^{{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}$,
whose meaning is given by the following lemma:999Its definition is
straightforward and thus omitted; it can be found in Appendix D.

###### Lemma 5.2.

$\forall\mathcal{L},\mathit{B_{{\mathrm{1}}}},\mathit{B_{{\mathrm{2}}}}$,
$(\mathcal{L}\to\to\mathit{B_{{\mathrm{1}}}})\,\&\,(\mathcal{L}\to\to\mathit{B_{{\mathrm{2}}}})<:\mathcal{L}\to\to(\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}})\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\llbracket{\mathcal{L}}\rrbracket_{\&}^{{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}$\/}$.

Rule AR-top deals with the same problem that rule AR-and does: according to
Lemma 5.1, the coercion needs to witness
$\mathit{A}<:(\mathcal{L}\to\to\top)$, and not simply $\mathit{A}<:\top$. As
$(\mathcal{L}\to\to\top)$ is top-like (Alpuim et al., 2017) we can always cast
$\top$ to it, which is what $\llbracket{\mathcal{L}}\rrbracket_{\top}$
witnesses:${}^{\ref{foot:metafunctions}}$

###### Lemma 5.3.

$\forall\mathcal{L},\top<:(\mathcal{L}\to\to\top)\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow\llbracket{\mathcal{L}}\rrbracket_{\top}$\/}$.

Rule AR-arr is straightforward. Finally, rule AR-nat handles the base case
where $\mathit{B}$ is $\mathsf{Nat}$. In this case we resort to the auxiliary
judgment
${\mathcal{L}};{\mathcal{M}};{\mathit{A_{{\mathrm{0}}}}};\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}${\mathcal{X}}$\/}\vdash_{\text{L}}{A}\prec:{B}\hbox{\pagecolor{gray!20}{\color[rgb]{0.9,0.9,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@stroke{0.9}\pgfsys@color<EMAIL_ADDRESS>width=2.0pt,height=0.0pt,depth=0.0pt}$\rightsquigarrow{\mathcal{X}^{\prime}}$\/}$,
which we discuss next.

####  5.1.2. Left Focusing

$\displaystyle\begin{array}[]{r@{\qquad}ccc@{\qquad}l}{\small\mbox{{\tt\sc AR-
nat}}}\Longrightarrow&\mathcal{L}_{0};\mathcal{M}_{0};\mathit{A_{{\mathrm{0}}}};\mathcal{X}_{0}\vdash_{L}\mathit{A_{{\mathrm{0}}}}\prec:\mathsf{Nat}&\rightsquigarrow&\mathcal{X}_{n}&(\mathcal{M}_{0}=[],\mathcal{X}_{0}=\Box)\\\
&\downarrow&&\uparrow&\\\
&\mathcal{L}_{1};\mathcal{M}_{1};\mathit{A_{{\mathrm{0}}}};\mathcal{X}_{1}\vdash_{L}\mathit{A}_{1}\prec:\mathsf{Nat}&\rightsquigarrow&\mathcal{X}_{n}&\\\
&\downarrow&&\uparrow\\\ &\cdots&&\cdots&\\\ &\downarrow&&\uparrow&\\\
{\small\mbox{{\tt\sc AL-
nat}}}\Longrightarrow&\mathcal{L}_{n};\mathcal{M}_{n};\mathit{A_{{\mathrm{0}}}};\mathcal{X}_{n}\vdash_{L}\mathit{A}_{n}\prec:\mathsf{Nat}&\rightsquigarrow&\mathcal{X}_{n}&(\mathit{A}_{n}=\mathsf{Nat},\mathcal{L}_{n}=[])\\\
\end{array}$

Figure 10. Visual Representation of the Execution of