(${\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}}$\/}$)

The intuition behind
${\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}}$\/}$
is that the (input) algorithmic context $\mathcal{X}$ witnesses the transition
from $\mathit{A_{{\mathrm{0}}}}$ to $(\mathcal{M}\to\to\mathit{A})$, the
component of $\mathit{A_{{\mathrm{0}}}}$ that we are currently focusing on.
The (output) algorithmic context $\mathcal{X}^{\prime}$ is meant to capture
the complete transition from $\mathit{A_{{\mathrm{0}}}}$ to
$(\mathcal{M}\to\to(\mathcal{L}\to\to\mathit{B}))$. Essentially, starting with
rule AR-nat as the entry point, the judgment continuously decomposes
$\mathit{A}$ (via rules AL-and1, AL-and2, AL-arr, and AL-mp) until it equals
$\mathit{B}$ (rule AL-nat); then the accumulated context $\mathcal{X}$
witnesses the complete transition from $\mathit{A_{{\mathrm{0}}}}$ to
$(\mathcal{M}\to\to(\mathcal{L}\to\to\mathit{B}))$ and the job is done. Figure
10 visualizes this process.

##### Subtyping

Ignoring coercion generation, the judgment works as follows: Rule AL-nat
constitutes the base case where subtyping holds trivially. Rules AL-and1 and
AL-and2 non-deterministically focus on the left or the right component of an
intersection, similarly to their declarative counterparts (rules S-andl and
S-andr, respectively). Rule AL-arr is the algorithmic version of rule S-arr:
we dequeue $\mathit{B_{{\mathrm{1}}}}$ from $\mathcal{L}$ in a first-in-first-
out manner, in order to match the order in which arrows are encountered in
$\mathit{A}$. After we prove subtyping for the domains of the functions, we
record that we are going under a binder of type $\mathit{B_{{\mathrm{1}}}}$ in
the queue $\mathcal{M}$ and proceed recursively with the function images.
Queue $\mathcal{M}$ thus captures all the arrow domains in $\mathit{B}$ that
have been removed in lockstep with arrow domains in $\mathit{A}$ using rule
S-arr.101010In Figure 10, it is easy to see that
$\mathcal{M}_{i}\,\mathtt{++}\,\mathcal{L}_{i}=\mathcal{L}_{0}$, where
$\mathtt{++}$ denotes list concatenation. At the end, we have
$\mathcal{M}_{n}=\mathcal{L}_{0}$. This context becomes useful when we need to
use Modus Ponens under a binder, e.g. to prove

$\mathsf{Nat}\rightarrow(\mathsf{Bool}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{String}))<:\mathsf{Nat}\rightarrow\mathsf{String}$

(or even
$\top\rightarrow(\mathsf{Bool}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{String}))<:\mathsf{Nat}\rightarrow\mathsf{String}$).
Lastly, rule AL-mp is the algorithmic version of the S-mp rule. The first
premise reveals the synergistic relationship between this rule and rule AL-
arr: when we need to synthesize an argument for Modus Ponens, we restart from
the original type $\mathit{A_{{\mathrm{0}}}}$—thus capturing the complete
implicit context of
$\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}$—and use the
contextualized version of $\mathit{A_{{\mathrm{1}}}}$,
($\mathcal{M}\to\to\mathit{A_{{\mathrm{1}}}}$). For the above example, this
amounts to proving

$\mathsf{Nat}\rightarrow(\mathsf{Bool}\,\&\,(\mathsf{Bool}\rightarrow\mathsf{String}))<:\mathsf{Nat}\rightarrow\mathsf{Bool}$

The second premise is straightforward.

Note that rules AL-arr and AL-mp overlap and, to ensure completeness with
respect to the declarative specification of subtyping, backtracking is
required. However, it is never the case that both rules can apply for
resolving a subtyping judgment. That is, backtracking will always fail in at
least one of the two choices.

##### Coercion Generation

The elaboration side, again, requires a bit more explanation. The complication
arises in rule AL-mp, where the first premise restarts from the original type
$\mathit{A_{{\mathrm{0}}}}$. This is essential for recovering the unfocused
context needed for Modus Ponens, but it goes against the inductive, top-down
approach to coercion generation that we follow in the right-focusing rules.
Coercions produced by the recursive calls can no longer be directly combined.
This is why the left focusing rules use algorithmic contexts instead of
coercions. The essence of the algorithmic contexts is captured in the
following invariant, which is preserved by each step of the left focusing
algorithm:

###### Invariant 1.

$\forall\mathit{c}~{}\mathit{A^{\prime}},\mathit{A}_{i}<:\mathit{A}^{\prime}\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}$\/}\implies\mathit{A_{{\mathrm{0}}}}<:(\mathcal{M}_{i}\to\to\mathit{A}^{\prime})\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}_{i}[c]$\/}$

Metavariables $\mathit{A}_{i}$, $\mathit{A_{{\mathrm{0}}}}$,
$\mathcal{M}_{i}$, and $\mathcal{X}_{i}$ refer to the corresponding parameters
at the $i$-th step in Figure 10. Informally, $\mathcal{X}$ captures the
transition from $\mathit{A_{{\mathrm{0}}}}$ to $\mathit{A}_{i}$:
$\mathcal{X}_{i}[c]$ witnesses the complete transition from
$\mathit{A_{{\mathrm{0}}}}$ to any type $\mathit{A}^{\prime}$, if we have a
way to perform the remaining transition from $\mathit{A}_{i}$ to
$\mathit{A}^{\prime}$. Hence, every rule of the judgment strips a layer off
$\mathit{A}$ and extends the “input” algorithmic context accordingly, so that
Invariant 1 is preserved.

Rule AL-mp is by far the most interesting rule. It commits to using the S-mp
rule: the left premise produces a coercion $\mathit{c_{{\mathrm{2}}}}$ that
provides the argument (of type $\mathcal{M}\to\to\mathit{A_{{\mathrm{1}}}}$),
while the appropriate instantiation of the current context $\mathcal{X}$ gives
us the function (of type
$\mathcal{M}\to\to(\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}})$):

$\begin{array}[]{l}\mathit{A_{{\mathrm{0}}}}<:\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}$\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/}\\\
\mathit{A_{{\mathrm{0}}}}<:\mathcal{M}\to\to(\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}$\rightsquigarrow\mathcal{X}[\mathsf{id}_{\mbox{$\mid$}\mathit{A_{{\mathrm{1}}}}\rightarrow\mathit{A_{{\mathrm{2}}}}\mbox{$\mid$}}]$\/}\\\
\end{array}$

Yet, the above coercions cannot be directly combined, due to the type queue
$\mathcal{M}$. We remedy this using meta-function
$\llbracket{\mathcal{M}}\rrbracket_{\&}^{{\mathit{c}},{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}$,
whose meaning is given by the following lemma:111111Its definition is
straightforward and thus omitted; it can be found in Appendix D.

###### Lemma 5.4.

$\forall\mathcal{L}\,\mathit{B_{{\mathrm{1}}}}\,\mathit{B_{{\mathrm{2}}}}\,\mathit{B}\,\mathit{c},\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}<:\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}$\/}\implies(\mathcal{L}\to\to\mathit{B_{{\mathrm{1}}}})\,\&\,(\mathcal{L}\to\to\mathit{B_{{\mathrm{2}}}})<:\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\llbracket{\mathcal{L}}\rrbracket_{\&}^{{\mathit{c}},{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}$\/}$.

The general idea is that if
$(\mathit{A_{{\mathrm{0}}}}<:\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}$\rightsquigarrow\mathit{c_{{\mathrm{2}}}}$\/})$
and
$(\mathit{A_{{\mathrm{0}}}}<:\mathcal{M}\to\to(\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}$\rightsquigarrow\mathit{c_{{\mathrm{1}}}}$\/})$
then

$\mathit{A_{{\mathrm{0}}}}<:\mathcal{M}\to\to\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}$\rightsquigarrow(\lambda
c.\llbracket{\mathcal{M}}\rrbracket_{\&}^{{(\mathit{c}\circ(\pi_{1}^{\mbox{$\mid$}(\mathit{A}\rightarrow\mathit{B})\mbox{$\mid$},\mbox{$\mid$}\mathit{A}\mbox{$\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{$\mid$}(\mathit{A}\rightarrow\mathit{B})\mbox{$\mid$},\mbox{$\mid$}\mathit{A}\mbox{$\mid$}}))},{(\mathit{A}\rightarrow\mathit{B})},{\mathit{A}}}\circ\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle)~{}[\hbox{}{}\mathsf{id}_{\mbox{$\mid$}\mathit{A_{{\mathrm{2}}}}\mbox{$\mid$}}\hbox{}]$\/}$

Returning to rule AL-mp, the second premise uses the above algorithmic context
(named $\mathcal{X}^{\prime}$ for convenience) to further focus on
$\mathit{A_{{\mathrm{2}}}}$.

###  5.2. Algorithm Metatheory

##### Subsumption of NeColus’ Algorithmic Subtyping

First, we have proven that the subtyping algorithm of Figure 9 subsumes the
subtyping algorithm of NeColus (Bi et al., 2018, Fig. 12):

###### Theorem 5.5 (Subsumption of NeColus’ Algorithm).

If
${[]}\vdash{\mathit{A}}\ll{\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}}\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}}$\/}$.

where
${\mathcal{L}}\vdash{\mathit{A}}\ll{\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}}$\/}$
denotes the subtyping algorithm of NeColus.

##### Transivity and Modus Ponens

A major difference between algorithmic and declarative subtyping is that the
latter has an explicit transitivity rule while the former does not. Hence,
transitivity of algorithmic subtyping requires a separate proof.
Unfortunately, this proof is considerably more involved than in NeColus.
Instead of one inductive core lemma, it consists of 7 mutually recursive
lemmas. The well-foundedness of the induction used in the proofs of those 7
lemmas is no longer a straightforward size-based induction that can be easily
understood by Coq. To overcome this problem we have used a new approach,
external to Coq, to establish well-foundedness. We have encoded the
proof—which is essentially an algorithm that transforms derivation trees—as a
term rewriting system. Then we have used the AProVE tool (Giesl et al., 2017)
to verify its termination automatically. AProVE reports success after 40 steps
of transformation, decomposition and basic termination arguments.

###### Theorem 5.6 (Transitivity of Algorithmic Subtyping).

If
${\mathit{A_{{\mathrm{1}}}}}\prec:{\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}$\rightsquigarrow{\mathit{c_{{\mathrm{1}}}}}$\/}$
and
${\mathit{A_{{\mathrm{2}}}}}\prec:{\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}$\rightsquigarrow{\mathit{c_{{\mathrm{2}}}}}$\/}$,
then
${\mathit{A_{{\mathrm{1}}}}}\prec:{\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}$\rightsquigarrow{\mathit{c_{{\mathrm{3}}}}}$\/}$
for some $\mathit{c_{{\mathrm{3}}}}$.

The modus ponens property for algorithmic subtyping is closely tied to
transitivity proof and is another consequence of the 7 mutually recursive
lemmas.

###### Corollary 5.7 (Modus Ponens of Algorithmic Subtyping).

If
${\mathit{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}$\rightsquigarrow{\mathit{c_{{\mathrm{1}}}}}$\/}$
and
${\mathit{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}$\rightsquigarrow{\mathit{c_{{\mathrm{2}}}}}$\/}$,
then
${\mathit{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}$\rightsquigarrow{\mathit{c_{{\mathrm{3}}}}}$\/}$
for some $\mathit{c_{{\mathrm{3}}}}$.

##### Soundness and Completeness

We have proven that the subtyping algorithm (Figure 9) is sound and complete
with respect to its declarative specification (Figure 4). The soundness of the
overall algorithm is a direct corollary of the soundness of right focusing
(Lemma 5.1):

###### Theorem 5.8 (Soundness).

If
${\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}<:\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 completeness proof largely follows the same strategy as for NeColus. The
main challenge was the new transitivity proof discussed above.

###### Theorem 5.9 (Completeness).

If
$\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
there exists $\mathit{c^{\prime}}$ such that
${\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^{\prime}}}$\/}$.

##### Termination

The final key property of the algorithm is termination. Actually, the
algorithm presented in Figure 9 is not terminating. Consider for example the
trace of ${\mathsf{Nat}\rightarrow\mathsf{Nat}}\prec:{\mathsf{Nat}}$:

$\begin{array}[]{l}({[]}\mathrel{\vdash_{\text{R}}}{\mathsf{Nat}\rightarrow\mathsf{Nat}}\prec:{\mathsf{Nat}})\xrightarrow{{\small\mbox{{\tt\sc
AR-
nat}}}}({[]};{[]};{\mathsf{Nat}\rightarrow\mathsf{Nat}}\vdash_{\text{L}}{\mathsf{Nat}\rightarrow\mathsf{Nat}}\prec:{\mathsf{Nat}})\xrightarrow{{\small\mbox{{\tt\sc
AL-mp}}}}\\\
({[]}\mathrel{\vdash_{\text{R}}}{\mathsf{Nat}\rightarrow\mathsf{Nat}}\prec:{\mathsf{Nat}})\xrightarrow{{\small\mbox{{\tt\sc
AR-
nat}}}}({[]};{[]};{\mathsf{Nat}\rightarrow\mathsf{Nat}}\vdash_{\text{L}}{\mathsf{Nat}\rightarrow\mathsf{Nat}}\prec:{\mathsf{Nat}})\xrightarrow{{\small\mbox{{\tt\sc
AL-mp}}}}\dots\\\ \end{array}$

Such a subtyping judgment can result from an erroneous type annotation by the
user. Nonetheless, the language does not statically detect annotations that
may cause non-termination in the subtyping algorithm. Another example, perhaps
more plausible as a programming error, is an annotation that leads to the
judgment
${(\mathsf{Nat}\rightarrow\mathsf{Bool})\,\&\,(\mathsf{Bool}\rightarrow\mathsf{Nat})}\prec:{\mathsf{Nat}}$.
One simple ingredient needs to be added to the algorithm to make it
terminating: a loop detection on the
${[]}\mathrel{\vdash_{\text{R}}}{A}\prec:{B}$ call in rule AL-mp. This loop
detection should reject any calls that repeat one of their ancestor calls.

We can show that (1) any infinite derivation involves an infinite number of
these nested calls and that (2) detecting repeated calls is effective at
stopping the non-termination.

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

$\begin{array}[]{rcl@{\hspace{2cm}}rcl}||\mathsf{Nat}||&=&0\hfil\hskip
56.9055pt&||\mathit{A}\rightarrow\mathit{B}||&=&\max{(||A||+1,||B||)}\\\
||\top||&=&0\hfil\hskip
56.9055pt&||\mathit{A}\,\&\,\mathit{B}||&=&\max{(||A||,||B||)}\\\
\lx@intercol\hfil||{[]}\mathrel{\vdash_{\text{R}}}{A}\prec:{B}||=\max{(||A||,||B||)}\hfil\lx@intercol\end{array}$

That leaves only the problematic mutually recursive call in rule AL-mp, which
we have already demonstrated to be a source of non-termination. Fortunately,
we can show that the number of distinct nested calls is finite. Hence, on any
infinite derivation path, a repeated call has to occur after a finite number
of steps. This makes the loop detection effective at curtailing divergence.

A more extensive account can be found in Appendix G.

###### Theorem 5.10 (Termination).

The algorithm extended with loop detection terminates.

##### Decidability

In summary, if we take the soundness, completeness and termination of the
subtyping together, we can conclude that the declarative subtyping is
decidable.

###### Corollary 5.11 (Decidable Subtyping).

In $\lambda_{i}^{\mathsf{MP}}$, $\mathit{A}<:\mathit{B}$ is decidable for any
types $\mathit{A}$ and $\mathit{B}$.

##  6\. Coherence

A desired property for calculi with a merge operator is _coherence_. This
ensures that no semantic ambiguity arises in programs, i.e. programs and their
subparts always have a single, unambiguous meaning. Recall that the semantics
of $\lambda_{i}^{\mathsf{MP}}$ is given indirectly, through an elaboration to
$\lambda_{\mathit{c}}^{\mathsf{MP}}$ and its operational semantics. Hence,
coherence for $\lambda_{i}^{\mathsf{MP}}$ means that all possible elaborations
of a well-typed source expression for a given type are contextually equivalent
in the target language.

Two target expressions, that may be syntactically different, are _contextually
equivalent_ iff, when used in the context of any program, there is no
difference in that program’s behavior. In our purely functional and strongly
normalising setting, we can reduce a program’s behavior to the value it
returns. Moreover, as usual, we can restrict ourselves without loss of
generality to programs of type $\mathsf{Nat}$ to facilitate the comparison of
the results.

_Program contexts_ express the above notion of using an expression in the
context of a program and are defined as follows:

Program contexts | $\mathcal{C}$ | $\Coloneqq$ | $[\cdot]\mid\lambda\mathit{x}.\,\mathcal{C}\mid\mathcal{C}\,E\mid E\,\mathcal{C}\mid\mathcal{C}\,,,\,E\mid E\,,,\,\mathcal{C}\mid\mathcal{C}:\mathit{A}$
---|---|---|---

Intuitively, a program context is an expression with a missing subexpression.
This hole can be filled in with an appropriate term to form an actual
expression. Which terms are eligible to be used in a program context is
captured by the context typing judgment that consists of judgments of the form
$\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}$\rightsquigarrow\mathcal{D}$\/}$.121212
There are also judgments for the three other combinations of the two typing
directions that appear in the judgment. The full specification can be found in
Appendix C.  Essentially, the judgment expresses that program context
$\mathcal{C}$ expects a term of type $\mathit{A}$ under typing context
$\Gamma$ to form an expression of type $\mathit{B}$ under context
$\Gamma^{\prime}$. Moreover, the source context $\mathcal{C}$ elaborates
straightforwardly to a target context $\mathcal{D}$. Indeed, for the coherence
of $\lambda_{i}^{\mathsf{MP}}$ we do not account for all possible target
contexts, but only for those that are the image of a source context
$\mathcal{C}$. This restriction is important, as Bi et al. (2018) have
demonstrated that there are other target contexts that can distinguish between
alternative elaborations.

We can now formally state coherence131313There is a second statement for the
type checking direction of the two hypotheses. .

###### Theorem 6.1 (Coherence of $\lambda_{i}^{\mathsf{MP}}$).

For any
$\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\bullet\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}$\rightsquigarrow\mathcal{D}$\/}$,
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_{{\mathrm{1}}}}$\/}$
and $\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_{{\mathrm{2}}}}$\/}$,
then there is a value $\bullet\vdash\mathit{v}:\mathsf{Nat}$ such that
$\mathcal{D}\\{\mathit{e_{{\mathrm{1}}}}\\}\longrightarrow^{*}\mathit{v}$ and
$\mathcal{D}\\{\mathit{e_{{\mathrm{2}}}}\\}\longrightarrow^{*}\mathit{v}$.

Here, $\mathcal{D}\\{\mathit{e}\\}$ denotes the term that results from filling
in the hole of $\mathcal{D}$ with expression $\mathit{e}$.

The remainder of this section summarizes our proof approach for coherence and
discusses the issues for our proof’s partiality. A more extensive account can
be found in Appendix F.

###  6.1. A Context Dependent Logical Relation

We follow the general approach for showing coherence as NeColus. This approach
is based on a rather atypical heterogeneous binary logical relation, called
_canonicity_ , by Bi et al. (2019).

##### Canonicity

The canonicity relation is in fact two families of relations, one for values
$\mathcal{V}$ and one for expressions $\mathcal{E}$, indexed by types. Two
values $\mathit{v_{{\mathrm{1}}}}$ and $\mathit{v_{{\mathrm{2}}}}$ of types
$\tau_{{\mathrm{1}}}$ and $\tau_{{\mathrm{2}}}$ are related by canonicity,
written
$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}(\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}})$,
iff any parts of the same type have the same meaning. By parts we mean values
$\mathit{v^{\prime}_{{\mathrm{1}}}}$ and $\mathit{v^{\prime}_{{\mathrm{2}}}}$
derivable from respectively $\mathit{v_{{\mathrm{1}}}}$ and
$\mathit{v_{{\mathrm{2}}}}$ by means of subtyping coercions. If two values
have non-trivial (i.e., non-top-like) parts with the same type, we say that
they overlap. For instance, values $\langle 1,\mathsf{true}\rangle$ and $1$
overlap since both have a part of type $\mathsf{Nat}$; because their
overlapping part is the same, namely $1$, these values are related by
canonicity. In contrast, $\langle 1,\mathsf{true}\rangle$ and $2$ are not
related since their overlapping $\mathsf{Nat}$ parts are different.

While the $\lambda_{i}^{\mathsf{MP}}$ canonicity relation follows the above
principles just like that of NeColus, there are considerable differences in
the actual definition because of the addition of modus ponens.

##### Context Dependency

A major complicating factor in the design of the new logical relation is that
the modus ponens subtyping rule introduces a form of context dependency.
Indeed, when reasoning about overlapping parts, the NeColus approach of
decomposing terms and their types, and looking at their syntactic components
in isolation no longer works. Instead, in $\lambda_{i}^{\mathsf{MP}}$ the
components have to be considered in the context of the whole value they appear
in. For example, the target term
$\lambda\mathit{x}:\mathsf{Nat}.\,\mathsf{true}$ does not overlap with
$\mathsf{false}$, since one is an arrow type and the other a boolean. Yet,
when $\lambda\mathit{x}:\mathsf{Nat}.\,\mathsf{true}$ is part of the larger
term $\langle\lambda\mathit{x}:\mathsf{Nat}.\,\mathsf{true},1\rangle$, a
problematic overlap arises: via modus ponens, the function applied to $1$ to
yields the boolean value $\mathsf{true}$ that differs from $\mathsf{false}$.

To account for that dependency on the whole value, or contextual dependency
for short, we equip the canonicity relation of $\lambda_{i}^{\mathsf{MP}}$
with two additional indices: the whole values and their types. Thus, we write

$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket$

to express that $\mathit{v_{{\mathrm{1}}}}$ and $\mathit{v_{{\mathrm{2}}}}$
are related values of types $\tau_{{\mathrm{1}}}$ and $\tau_{{\mathrm{2}}}$
that are components of respectively the values
$\mathit{v^{\prime}_{{\mathrm{1}}}}$ of type $\tau^{\prime}_{{\mathrm{1}}}$
and $\mathit{v^{\prime}_{{\mathrm{2}}}}$ of type
$\tau^{\prime}_{{\mathrm{2}}}$.

We refer to Appendix F for the full definition of this context-dependent
canonicity relation $\mathcal{V}$ for values and its companion $\mathcal{E}$
for expressions.

##### Properties

A key property of the canonicity relation is _coercion compatibility_. This
states that any coercions of related values are related as well.

###### Lemma 6.2 (Coercion Compatibility).

If
$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v_{{\mathrm{1}}}}:\tau_{{\mathrm{1}}};\mathit{v_{{\mathrm{2}}}}:\tau_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket$,
then for all coercions $\mathit{c_{{\mathrm{1}}}}$,
$\mathit{c_{{\mathrm{2}}}}$ and types $\tau^{\prime}_{{\mathrm{1}}}$,
$\tau^{\prime}_{{\mathrm{2}}}$ such that
$\mathit{c_{{\mathrm{1}}}}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau^{\prime}_{{\mathrm{1}}}$
and
$\mathit{c_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{2}}}\,\triangleright\,\tau^{\prime}_{{\mathrm{2}}}$
it holds that
$(\mathit{c_{{\mathrm{1}}}}\,\mathit{v_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\,\mathit{v_{{\mathrm{2}}}})\in\mathcal{E}^{(\mathit{c_{{\mathrm{1}}}}\,\mathit{v_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{c_{{\mathrm{2}}}}\,\mathit{v_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau^{\prime}_{{\mathrm{1}}};\tau^{\prime}_{{\mathrm{2}}}\rrbracket$.

The following lemma asserts another key property of the value relation, which
establishes its connection to disjointness. This follows from the design
principle that any overlap in types should concern indistinguishable values.
If there is no overlap, then this is trivially satisfied.

###### Lemma 6.3 (Disjointly-Typed Values are Related).

If
$\bullet\vdash\mathit{v_{{\mathrm{1}}}}:\mbox{$\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\mid$}$
and
$\bullet\vdash\mathit{v_{{\mathrm{1}}}}:\mbox{$\mid$}\mathit{A_{{\mathrm{2}}}}\mbox{$\mid$}$
where $\mathit{A_{{\mathrm{1}}}}*\mathit{A_{{\mathrm{2}}}}$, then
$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v_{{\mathrm{1}}}}:\mbox{$\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\mid$};\mathit{v_{{\mathrm{2}}}}:\mbox{$\mid$}\mathit{A_{{\mathrm{2}}}}\mbox{$\mid$})}\llbracket\mbox{$\mid$}\mathit{A_{{\mathrm{1}}}}\mbox{$\mid$};\mbox{$\mid$}\mathit{A_{{\mathrm{2}}}}\mbox{$\mid$}\rrbracket$.

###  6.2. Coherence Proof

With the canonicity relation in place, we can turn to the actual coherence
proof. This proof is split in two parts by the canonicity relation. The first
and hardest part is to show that any two elaborations of the same source term
are related by canonicity; this is the so-called _fundamental property_ , .
The second part is to show that related programs of type $\mathsf{Nat}$ return
the same value; it follows almost trivially from the definition of the
canonicity relation.

##### Logical Equivalence

To express the fundamental property, we need to introduce a notion of logical
equivalence for open expressions on top of the canonicity relations for closed
values ($\mathcal{V}$) and closed terms ($\mathcal{E}$). Open expressions are
considered in some typing context $\Delta$. A _closing substitution_ $\gamma$
of a typing context $\Delta$ maps variables to values of the type specified in
$\Delta$. Two open expressions are related iff applying any two related
closing substitutions to $\mathit{e_{{\mathrm{1}}}}$ and
$\mathit{e_{{\mathrm{2}}}}$, respectively, results in $\mathcal{E}$-related
closed terms:

$\Delta_{{\mathrm{1}}};\Delta_{{\mathrm{2}}}\vdash\mathit{e_{{\mathrm{1}}}}\simeq_{\text{log}}\mathit{e_{{\mathrm{2}}}}:\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}~{}\triangleq~{}\forall~{}(\gamma_{{\mathrm{1}}};\gamma_{{\mathrm{2}}})\in\mathcal{G}\llbracket\Delta_{{\mathrm{1}}};\Delta_{{\mathrm{2}}}\rrbracket,~{}~{}(\mathit{e_{{\mathrm{1}}}}[\gamma_{{\mathrm{1}}}],\mathit{e_{{\mathrm{2}}}}[\gamma_{{\mathrm{2}}}])\in\mathcal{V}^{(\mathit{e_{{\mathrm{1}}}}[\gamma_{{\mathrm{1}}}]:\tau_{{\mathrm{1}}};\mathit{e_{{\mathrm{2}}}}[\gamma_{{\mathrm{2}}}]:\tau_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket$

Two closing substitutions $\gamma_{{\mathrm{1}}}$ and $\gamma_{{\mathrm{2}}}$
of $\Delta_{{\mathrm{1}}}$ and $\Delta_{{\mathrm{2}}}$ are related iff the two
typing contexts differ only in the types of the variables (otherwise, they
contain the same variables and in the same order) and the values that
$\gamma_{{\mathrm{1}}}$ and $\gamma_{{\mathrm{2}}}$ contain for each variable
are $\mathcal{V}$-related.

##### Fundamental Property

Now we can state the fundamental property:141414There is a second statement
for the type checking direction of the two hypotheses.

###### Theorem 6.4 (Fundamental property).

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_{{\mathrm{1}}}}$\/}$
and $\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_{{\mathrm{2}}}}$\/}$,
then
$\mbox{$\mid$}\Gamma\mbox{$\mid$};\mbox{$\mid$}\Gamma\mbox{$\mid$}\vdash\mathit{e_{{\mathrm{1}}}}\simeq_{\text{log}}\mathit{e_{{\mathrm{2}}}}:\mbox{$\mid$}\mathit{A}\mbox{$\mid$};\mbox{$\mid$}\mathit{A}\mbox{$\mid$}$.

Due to the complexity of the canonicity relation, we have proven this theorem
under Conjectures 6.5 and 6.6. The proof proceeds by induction on the first
hypothesis and calls coercion compatibility for the T-sub case. The
conjectures are used in the inductive cases of T-abs and T-merge.

###### Conjecture 0 (Compatibility of abstractions).

If
$\Delta,\mathit{x}:\tau^{\prime}_{{\mathrm{1}}};\Delta,\mathit{x}:\tau^{\prime}_{{\mathrm{2}}}\vdash\mathit{e_{{\mathrm{1}}}}\simeq_{\text{log}}\mathit{e_{{\mathrm{2}}}}:\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}$,
then
$\Delta;\Delta\vdash\lambda\mathit{x}:\tau^{\prime}_{{\mathrm{1}}}.\,\mathit{e_{{\mathrm{1}}}}\simeq_{\text{log}}\lambda\mathit{x}:\tau^{\prime}_{{\mathrm{2}}}.\,\mathit{e_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{1}}};\tau^{\prime}_{{\mathrm{2}}}\rightarrow\tau_{{\mathrm{2}}}$.

###### Conjecture 0 (Compatibility of pairs).

If
$\Delta;\Delta\vdash\mathit{e_{{\mathrm{1}}}}\simeq_{\text{log}}\mathit{e_{{\mathrm{2}}}}:\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}$
and
$\Delta;\Delta\vdash\mathit{e^{\prime}_{{\mathrm{1}}}}\simeq_{\text{log}}\mathit{e^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{1}}};\tau^{\prime}_{{\mathrm{2}}}$
and $\tau_{{\mathrm{1}}}*\tau^{\prime}_{{\mathrm{2}}}$ and
$\tau_{{\mathrm{2}}}*\tau^{\prime}_{{\mathrm{1}}}$, then
$\Delta;\Delta\vdash\langle\mathit{e_{{\mathrm{1}}}},\mathit{e^{\prime}_{{\mathrm{1}}}}\rangle\simeq_{\text{log}}\langle\mathit{e_{{\mathrm{2}}}},\mathit{e^{\prime}_{{\mathrm{2}}}}\rangle:\tau_{{\mathrm{1}}}\times\tau^{\prime}_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\times\tau^{\prime}_{{\mathrm{2}}}$.

Regarding compatibility of pairs, a tuple value can result either from an
explicit merge or from a coercion applied on some value. In the first case,
the subcomponents of the tuple are disjoint with each other and thus related
(by Lemma 6.3). In the second case, given that the original expression is
unambiguous and since coercions do not introduce ambiguity, the coercion
application is also unambiguous. However, because of the context dependency it
is not easy to recover the original expression and inspect it. For a similar
reason, compatibility of abstraction is also hard to prove.

##### Logical Equivalence Entails Contextual Equivalence

Lastly, we need to show that any logically related target expressions are
contextually equivalent. The proof is fairly straightforward.

###### Theorem 6.7 (Logical Equivalence Entails Contextual Equivalence).

If
$\mbox{$\mid$}\Gamma\mbox{$\mid$};\mbox{$\mid$}\Gamma\mbox{$\mid$}\vdash\mathit{e_{{\mathrm{1}}}}\simeq_{\text{log}}\mathit{e_{{\mathrm{2}}}}:\mbox{$\mid$}\mathit{A}\mbox{$\mid$};\mbox{$\mid$}\mathit{A}\mbox{$\mid$}$,
then for any
$\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\bullet\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}$\rightsquigarrow\mathcal{D}$\/}$, there
is a value $\bullet\vdash\mathit{v}:\mathsf{Nat}$ such that
$\mathcal{D}\\{\mathit{e_{{\mathrm{1}}}}\\}\longrightarrow^{*}\mathit{v}$ and
$\mathcal{D}\\{\mathit{e_{{\mathrm{2}}}}\\}\longrightarrow^{*}\mathit{v}$.

Taken together, the (conditionally proven) fundamental property and the
entailment of contextual equivalence establish Theorem 6.1, the coherence of
$\lambda_{i}^{\mathsf{MP}}$.

##  7\. Related Work

##### Resolution and Subtyping

The main contribution of our work is to unify resolution and subtyping into a
single mechanism. Resolution is a common technique for automatically
constructing implicit values, such as Haskell’s type class dictionaries
(Wadler and Blott, 1989) or Scala’s implicits (Odersky, 2010). Subtyping is
widely used in Object-Oriented programming and various other type systems
(Pierce and Sangiorgi, 1996; Barendregt et al., 1983; Chen, 2003; Gay and
Hole, 2005). In our work we interpret resolution as a special case of coercive
subtyping (Chen, 2003), where coercions are generated automatically in a type-
directed fashion and then “inserted” into the program. This fits well with the
common type-directed elaboration style usually employed by resolution
mechanisms, which work in a similar way.

As far as we are aware, the unification of subtyping and resolution is novel.
Despite the fact that languages like Scala integrate both mechanisms, only
Jeffery (2019) combines both mechanisms within his DIF calculus.
Unfortunately—in contrast to $\lambda_{i}^{\mathsf{MP}}$—DIF’s subtyping is
known to be undecidable. Furthermore, Jeffery does not study the coherence of
DIF. Scala implicits (Odersky, 2010) have motivated other researchers to look
into the foundations of the mechanism. However, all previous work on implicit
calculi, including the _implicit calculus_ (Oliveira et al., 2012), _Cochis_
(Schrijvers et al., 2019) and the _SI calculus_ (Odersky et al., 2017), do not
account for subtyping. Instead, they all focus on a System F (Reynolds, 1974)
based language (without subtyping), and model resolution for such a language.
One aspect that these implicit calculi preserve from Scala is a biased form of
resolution where innermost implicits are preferred. In contrast, our
disjointness approach is more reminiscent of Haskell’s non-overlapping type
class instances, which are unbiased.

The most common technique to algorithmically construct values by resolution,
attributed to Kowalski (1974), is commonly known as SLD resolution, or
backwards chaining. Another technique, mostly used as a proof search method,
is focusing (Andreoli, 1992; Liang and Miller, 2009; Miller et al., 1989) and
has been used to great effect in similar calculi (e.g. Cochis (Schrijvers et
al., 2019) and Haskell with quantified class constraints (Bottu et al., 2017))
to create coherent resolution mechanisms. Our subtyping algorithm of Section 5
closely resembles the focusing technique.

##### Coherence

Since Reynolds (1991) proved coherence for a calculus with intersection types,
based on denotational semantics, many researchers have studied it in a variety
of typed calculi. Below we summarize two commonly-found approaches in the
literature: normal forms, and logical relations.

Breazu-Tannen et al. (1991) proved the coherence of a coercion translation
from Fun (Cardelli and Wegner, 1985) extended with recursive types to System
F, by showing that any two typing derivations of the same judgment are
normalizable to the same form. Curien and Ghelli (1994) presented a
translation of System $F_{\leq}$ into a calculus with explicit coercions and
showed that any derivations of the same judgment are translated to terms that
are normalizable to a unique normal form. Following the same approach,
Schwinghammer (2009) proved the coherence of coercion translation from Moggi’s
computational lambda calculus (Moggi, 1991) with subtyping.

Central to the first approach is to find a unique normal form for derivations.
However, this approach cannot be directly applied to Curry-style calculi,
i.e., where the lambda abstractions are not type-annotated. Also, it does not
work when the calculus has general recursion. Biernacki and Polesiuk (2015)
considered the coherence problem of coercion semantics. Their criterion for
coherence of the translation is contextual equivalence in the target calculus.
They used a logical relation for establishing coherence for coercion
semantics, applicable in a variety of calculi, including delimited
continuations and control-effect subtyping.

As far as we know, the first work to use logical relations to show the
coherence for intersection types and the merge operator was that of Bi et al.
(2018) for NeColus, and later for $F_{i}^{+}$ (Bi et al., 2019). The BCD
subtyping in both calculi (as well as our own) poses a non-trivial
complication over Bernacki and Polesiuk’s simple structural subtyping. In
their system any two coercions between given types are behaviorally equivalent
in the target language, so their coherence reasoning can all take place in the
target language. In NeColus, $F_{i}^{+}$, and $\lambda_{i}^{\mathsf{MP}}$ this
is not the case; coercions can be distinguished by arbitrary target programs
but not those that are elaborations of source programs. Hence, reasoning is
restricted to the latter class, which is reflected in a more complicated
notion of contextual equivalence and the logical relation’s non-trivial
treatment of pairs. In addition to these complications, our logical relation
(and consequently the coherence proof) is significantly more convoluted than
that of NeColus and $F_{i}^{+}$, due to the non-compositionality of Modus
Ponens.

##### Intersection Types and the Merge Operator

Forsythe (Reynolds, 1988) is one of the first languages with intersection
types and a merge-like operator. However, merges in Forsythe cannot contain
more than one function; this restriction ensures that the language is
coherent. Similarly, Castagna et al.’s $\lambda\&$ calculus (Castagna et al.,
1992) includes a special merge operator that works on functions only. More
recently, Dunfield (2012) showed significant expressiveness of type systems
with intersection types and a merge operator, at the cost of coherence. The
limitation was addressed by Oliveira et al. (2016), who introduced
disjointness to ensure coherence. The combination of intersection types, a
merge operator and parametric polymorphism—while achieving coherence—was first
studied in the $F_{i}$ calculus (Alpuim et al., 2017). Its successor,
$F_{i}^{+}$ (Bi et al., 2019) additionally incorporates BCD subtyping
(Barendregt et al., 1983), while remaining coherent. NeColus (Bi et al., 2018)
has been the starting point for our design of $\lambda_{i}^{\mathsf{MP}}$ and
incorporates intersection types, a merge operator, and BCD-style
distributivity. Though neither NeColus nor $\lambda_{i}^{\mathsf{MP}}$
accounts for parametric polymorphism, this is a direction we would like to
explore in the future.

##### BCD Type System and Decidability

The BCD type system was first introduced by Barendregt et al. (1983). It is
derived from a filter lambda model in order to characterize exactly the
strongly normalizing terms. The BCD type system features a powerful subtyping
relation, which serves as a base for ours. Bessai et al. (2014) showed how to
type classes and mixins in a BCD-style record calculus with the merge operator
of Bracha and Cook (1990). Their merge only operates on records, and they only
study a type assignment system. The decidability of BCD subtyping has been
shown in several works (Pierce, 1989; Kurata and Takahashi, 1995; Rehof and
Urzyczyn, 2011; Statman, 2014). Laurent (2012) has formalized the relation in
Coq in order to eliminate transitivity cuts from it, but he does not deliver
an algorithm. Based on the work of Statman (2014), Bessai et al. (2016) show a
formally verified subtyping algorithm in Coq. Our algorithm follows the
decision procedure of Bi et al. (2018) and Pierce (1989). However the addition
of modus ponens requires significant changes to the algorithm, and complicates
the metatheory.

##### Coq Type Classes

Coq employs a flexible type class system (Sozeau and Oury, 2008b) that permits
overlapping instances and provides the user with the means to control
resolution: Coq instances are named and can be explicitly passed as arguments.
The system poses no restrictions over the implicit environment, like non-
overlapping instances in Haskell or disjointness in
$\lambda_{i}^{\mathsf{MP}}$. Therefore, coherence becomes a choice and
responsibility of the user.

In contrast, $\lambda_{i}^{\mathsf{MP}}$ employs a stricter system that
provides less control over subtyping. First, implicit environments are not
possible if not internally disjoint. Second, going against the intuition which
relates classes to types and instances to appropriately typed terms,
expressions in $\lambda_{i}^{\mathsf{MP}}$ can be rather viewed as typed
implicit environments, which can be composed with the use of the merge
operator. Passing a value to a function in $\lambda_{i}^{\mathsf{MP}}$ can be
seen as bringing an implicit environment in scope within the body of the
function. The function, then, can use that environment to infer values from
it, but it does not have access to the names of the instances contained in it.
This is conceptually different from the named instances of Coq that can be
optionally passed explicitly by the user. Last, Coq uses a global environment
to which instances are inserted at their point of declaration.

##  8\. Conclusion and Future Work

This paper has shown that, with a small extension, subtyping with intersection
types can be used to model resolution. We have materialized our ideas in the
design of $\lambda_{i}^{\mathsf{MP}}$, a type-safe extension of NeColus with
the logical rule for Modus Ponens. This small extension significantly
increases the expressive power of $\lambda_{i}^{\mathsf{MP}}$’s predecessor,
allowing us to model features such as type class resolution and first-class
environments.

##### Future Work

A natural avenue for future work is the extension of
$\lambda_{i}^{\mathsf{MP}}$ with parametric polymorphism. When done naively,
it can make the algorithm diverge and, like in Haskell, additional conditions
will have to be imposed to recover termination. Moreover, we believe that
there are various applications for our work that we wish to explore in the
future.

In a Haskell-like setting, our design would enable multiple implicit
environments, instead of a single global one. Such environments could be
first-class, could be explicitly passed as arguments or returned as a result,
or could be composed to form larger implicit environments. The programmer
would then be able to choose which of the implicit environments to use for
resolution.

In a Scala-like setting, where subtyping is present, our design helps clarify
the interaction between resolution and subtyping. This is important, from the
practical point of view, since the interaction between the two mechanisms has
been a continuous source of compiler bugs151515 See for example
https://github.com/scala/bug/issues/2509 or
https://github.com/scala/bug/issues/9764.. Furthermore, our work could also be
interesting to offer a unified view of subtyping and resolution, which could
significantly reduce the implementation effort for the two mechanisms.

Finally, languages like TypeScript can support a merge operator for
intersection types via an encoding (Alpuim et al., 2017). Since Typescript has
subtyping, intersection types and the merge operator (via an encoding), it
would be quite interesting to explore the potential to extend the current
formulation of intersection types in TypeScript with the ideas of our work.

###### Acknowledgements.

We are grateful to anonymous reviewers that helped improving the presentation
of our work. This work has been sponsored by Hong Kong Research Grant Council
projects number 17210617 and 17209519, Flemish Fund for Scientific Research
project number G073816N and KU Leuven project number C14/20/079.

## References

  * (1)
  * Alpuim et al. (2017) João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017.  Disjoint Polymorphism. In _ESOP_ _(Lecture Notes in Computer Science, Vol. 10201)_. Springer, 1–28.
  * Amin et al. (2016) Nada Amin, Karl Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016.  The Essence of Dependent Object Types.  _A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday_ (2016), 249–272.  http://infoscience.epfl.ch/record/215280
  * Amin et al. (2012) Nada Amin, Adriaan Moors, and Martin Odersky. 2012.  Dependent Object Types.  (2012).  http://infoscience.epfl.ch/record/183030
  * Andreoli (1992) Jean-marc Andreoli. 1992\.  Logic Programming with Focusing Proofs in Linear Logic.  _Journal of Logic and Computation_ 2 (1992), 297–347.
  * Barendregt et al. (1983) Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983\.  A Filter Lambda Model and the Completeness of Type Assignment.  _J. Symb. Log._ 48, 4 (1983), 931–940.
  * Benzaken et al. (2003) Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003\.  CDuce: An XML-Centric General-Purpose Language.  _SIGPLAN Not._ 38, 9 (Aug. 2003), 51–63.  https://doi.org/10.1145/944746.944711
  * Bessai et al. (2014) Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen, and Ugo de’Liguoro. 2014\.  Typing Classes and Mixins with Intersection Types. In _ITRS_ _(EPTCS, Vol. 177)_. 79–93.
  * Bessai et al. (2016) Jan Bessai, Andrej Dudenhefner, Boris Düdder, and Jakob Rehof. 2016.  Extracting a Formally Verified Subtyping Algorithm for Intersection Types from Ideals and Filters _(TYPES)_.
  * Bi et al. (2018) Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2018\.  The Essence of Nested Composition. In _ECOOP_ _(LIPIcs, Vol. 109)_. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 22:1–22:33.
  * Bi et al. (2019) Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2019.  Distributive Disjoint Polymorphism for Compositional Programming. In _Programming Languages and Systems_ , Luís Caires (Ed.). Springer International Publishing, Cham, 381–409.
  * Biernacki and Polesiuk (2015) Dariusz Biernacki and Piotr Polesiuk. 2015.  Logical Relations for Coherence of Effect Subtyping. In _TLCA_ _(LIPIcs, Vol. 38)_. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 107–122.
  * Bottu et al. (2017) Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, and Philip Wadler. 2017\.  Quantified Class Constraints.  _SIGPLAN Not._ 52, 10 (Sept. 2017), 148–161.
  * Bracha and Cook (1990) Gilad Bracha and William R. Cook. 1990.  Mixin-based Inheritance. In _OOPSLA/ECOOP_. ACM, 303–311.
  * Breazu-Tannen et al. (1991) Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. 1991.  Inheritance As Implicit Coercion.  _Inf. Comput._ 93, 1 (July 1991), 172–221.
  * Cardelli and Wegner (1985) Luca Cardelli and Peter Wegner. 1985.  On Understanding Types, Data Abstraction, and Polymorphism.  _ACM Comput. Surv._ 17, 4 (Dec. 1985), 471–523.
  * Castagna et al. (1992) Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. 1992\.  A Calculus for Overloaded Functions with Subtyping.  _SIGPLAN Lisp Pointers_ V, 1 (Jan. 1992), 182–192.
  * Chen (2003) Gang Chen. 2003\.  Coercive subtyping for the Calculus of Constructions.. In _POPL_. 150–159.
  * Coppo et al. (1981) M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. 1981\.  Functional Characters of Solvable Terms.  _Math. Log. Q._ 27 (1981), 45–58.
  * Curien and Ghelli (1994) Pierre-Louis Curien and Giorgio Ghelli. 1994.  Theoretical Aspects of Object-oriented Programming.  MIT Press, Cambridge, MA, USA, Chapter Coherence of Subsumption, Minimum Typing and Type-checking in F&Le;, 247–292.
  * Davies and Pfenning (2000) Rowan Davies and Frank Pfenning. 2000.  Intersection Types and Computational Effects.  _SIGPLAN Not._ 35, 9 (Sept. 2000), 198–208.  https://doi.org/10.1145/357766.351259
  * Devriese and Piessens (2011) Dominique Devriese and Frank Piessens. 2011.  On the bright side of type classes: instance arguments in Agda. In _ICFP ’11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming_. ACM, 143–155.
  * Dunfield (2007) Joshua Dunfield. 2007\.  Refined Typechecking with Stardust. In _Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification_ (Freiburg, Germany) _(PLPV ’07)_. Association for Computing Machinery, New York, NY, USA, 21–32.  https://doi.org/10.1145/1292597.1292602
  * Dunfield (2012) Jana Dunfield. 2012\.  Elaborating Intersection and Union Types.  _SIGPLAN Not._ 47, 9 (Sept. 2012), 17–28.
  * Dunfield (2015) Joshua Dunfield. 2015\.  Elaborating Evaluation-Order Polymorphism.  _SIGPLAN Not._ 50, 9 (Aug. 2015), 256–268.  https://doi.org/10.1145/2858949.2784744
  * Freeman and Pfenning (1991) Tim Freeman and Frank Pfenning. 1991.  Refinement types for ML. In _Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation_. 268–277.
  * Gay and Hole (2005) Simon J. Gay and Malcolm J. Hole. 2005.  Subtyping for Session Types in the Pi Calculus.  _Acta Informatica_ 42, 2/3 (2005), 191–225.
  * Giesl et al. (2017) J. Giesl, C. Aschermann, M. Brockschmidt, et al. 2017\.  Analyzing Program Termination and Complexity Automatically with AProVE.  _J Autom Reasoning_ 58 (2017), 3–31.
  * Hall et al. (1996) Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. 1996.  Type classes in Haskell.  _ACM Transactions on Programming Languages and Systems_ 18, 2 (1996), 109–138.
  * Jeffery (2019) Alex Jeffery. 2019\.  Dependent Object Types with Implicit Functions. In _Proceedings of the Tenth ACM SIGPLAN Symposium on Scala_ _(Scala ’19)_. Association for Computing Machinery, New York, NY, USA, 1–11.
  * Kowalski (1974) Robert A. Kowalski. 1974\.  Predicate Logic as Programming Language. In _IFIP Congress_. North-Holland, 569–574.
  * Kurata and Takahashi (1995) Toshihiko Kurata and Masako Takahashi. 1995.  Decidable Properties of Intersection Type Systems. In _Proceedings of the Second International Conference on Typed Lambda Calculi and Applications_ _(TLCA ’95)_. Springer-Verlag, Berlin, Heidelberg, 297–311.
  * Laurent (2012) Olivier Laurent. 2012\.  Intersection Types with Subtyping by Means of Cut Elimination.  _Fundam. Inf._ 121, 1-4 (Jan. 2012), 203–226.
  * Liang and Miller (2009) Chuck Liang and Dale Miller. 2009.  Focusing and Polarization in Linear, Intuitionistic, and Classical Logics.  _Theor. Comput. Sci._ 410, 46 (2009), 4747–4768.
  * Luo (1999) Zhaohui Luo. 1999\.  Coercive subtyping.  _Journal of Logic and Computation_ 9, 1 (1999), 105–130.
  * Miller et al. (1989) Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. 1989.  _Uniform Proofs As a Foundation for Logic Programming_.  Technical Report.
  * Moggi (1991) Eugenio Moggi. 1991\.  Notions of Computation and Monads.  _Inf. Comput._ 93, 1 (July 1991), 55–92.
  * Odersky (2010) Martin Odersky. 2010\.  The Scala language specification, version 2.8.
  * Odersky et al. (2017) Martin Odersky, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. 2017.  Simplicitly: Foundations and Applications of Implicit Function Types.  _Proc. ACM Program. Lang._ 2, POPL (2017).
  * Oliveira et al. (2010) Bruno C.d.S. Oliveira, Adriaan Moors, and Martin Odersky. 2010\.  Type Classes As Objects and Implicits. In _Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications_ _(OOPSLA ’10)_. ACM, 341–360.
  * Oliveira et al. (2012) Bruno C.d.S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee, and Kwangkeun Yi. 2012.  The Implicit Calculus: A New Foundation for Generic Programming.  47, 6 (2012).
  * Oliveira et al. (2016) Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016\.  Disjoint Intersection Types.  _SIGPLAN Not._ 51, 9 (Sept. 2016), 364–377.
  * Pierce (1989) Benjamin C. Pierce. 1989\.  _A Decision Procedure for the Subtype Relation on Intersection Types with Bounded Variables_.  Technical Report. Carnegie Mellon University.
  * Pierce (1991) Benjamin C. Pierce. 1991\.  _Programming with Intersection Types and Bounded Polymorphism_.  Ph.D. Dissertation. Carnegie Mellon University.  Available as School of Computer Science technical report CMU-CS-91-205.
  * Pierce (1997) Benjamin C. Pierce. 1997\.  Intersection types and bounded polymorphism.  _Mathematical Structures in Computer Science_ 7, 2 (1997), 129–193.  https://doi.org/10.1017/S096012959600223X
  * Pierce and Sangiorgi (1996) B. C. Pierce and D. Sangiorgi. 1996.  Typing and Subtyping for Mobile Processes.  _Math. Structures in Comput. Sci._ 6, 5 (1996), 409–453.
  * Pottinger (1980) Garrel Pottinger. 1980\.  A type assignment for the strongly normalizable $\lambda$-terms.  _To HB Curry: essays on combinatory logic, lambda calculus and formalism_ (1980), 561–577.
  * Raskin (1974) Jef Raskin. 1974\.  FLOW: a teaching language for computer programming in the humanities.  _Computers and the Humanities_ 8, 4 (1974), 231–237.
  * Rehof and Urzyczyn (2011) Jakob Rehof and PawełUrzyczyn. 2011.  Finite Combinatory Logic with Intersection Types. In _Proceedings of the 10th International Conference on Typed Lambda Calculi and Applications_ (Novi Sad, Serbia) _(TLCA’11)_. Springer-Verlag, Berlin, Heidelberg, 169–183.
  * Reynolds (1972) John C. Reynolds. 1972\.  Definitional Interpreters for Higher-order Programming Languages. In _Proceedings of the ACM Annual Conference - Volume 2_ (Boston, Massachusetts, USA) _(ACM ’72)_. ACM, New York, NY, USA, 717–740.
  * Reynolds (1974) John C. Reynolds. 1974\.  Towards a Theory of Type Structure.  Lecture Notes in Computer Science, Vol. 19. 408–425.
  * Reynolds (1988) John C. Reynolds. 1988\.  _Preliminary Design of the Programming Language Forsythe_.  Technical Report. Carnegie Mellon University.
  * Reynolds (1991) John C. Reynolds. 1991\.  The Coherence of Languages with Intersection Types. In _Proceedings of the International Conference on Theoretical Aspects of Computer Software_ _(TACS ’91)_. Springer-Verlag, Berlin, Heidelberg, 675–700.
  * Schrijvers et al. (2019) Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler, and Koar Marntirosian. 2019.  COCHIS: Stable and coherent implicits.  _Journal of Functional Programming_ 29 (2019), e3.
  * Schwinghammer (2009) Jan Schwinghammer. 2009\.  Coherence of Subsumption for Monadic Types.  _J. Funct. Program._ 19, 2 (March 2009), 157–172.
  * Sozeau and Oury (2008a) Matthieu Sozeau and Nicolas Oury. 2008a.  First-Class Type Classes. In _TPHOLs ’08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics_.
  * Sozeau and Oury (2008b) M. Sozeau and N. Oury. 2008b.  First-Class Type Classes. In _TPHOLs_.
  * Statman (2014) Rick Statman. 2014\.  A Finite Model Property for Intersection Types. In _ITRS_ _(EPTCS, Vol. 177)_. 1–9.
  * Wadler (2015) Philip Wadler. 2015\.  Propositions as Types.  _Commun. ACM_ 58, 12 (Nov. 2015), 75–84.
  * Wadler and Blott (1989) P. Wadler and S. Blott. 1989.  How to Make Ad-hoc Polymorphism Less Ad Hoc. In _Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Austin, Texas, USA) _(POPL ’89)_. ACM, New York, NY, USA, 60–76.
  * White et al. (2015) Leo White, Frédéric Bour, and Jeremy Yallop. 2015\.  Modular implicits.  _Electronic Proceedings in Theoretical Computer Science_ 198 (12 2015).
  * Winant and Devriese (2018) Thomas Winant and Dominique Devriese. 2018.  Coherent Explicit Dictionary Application for Haskell. In _Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell_ (St. Louis, MO, USA) _(Haskell 2018)_. Association for Computing Machinery, New York, NY, USA, 81–93.

##  Appendix A Complete Specification of $\lambda_{\mathit{c}}^{\mathsf{MP}}$

$\Delta\vdash\mathit{e}:\tau$ Term Typing

$\displaystyle\displaystyle{\hbox{\hskip
19.54678pt\vbox{\hbox{\hskip-19.54677pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{x}:\tau\,\in\,\Delta$}}}\vbox{}}}\over\hbox{\hskip
16.21352pt\vbox{\vbox{}\hbox{\hskip-16.2135pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{x}:\tau$}}}}}}$
typ-var $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
17.77779pt\vbox{\vbox{}\hbox{\hskip-17.77779pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\langle\rangle:\langle\rangle$}}}}}}$
typ-unit $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
19.58334pt\vbox{\vbox{}\hbox{\hskip-19.58334pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{i}:\mathsf{Nat}$}}}}}}$
typ-lit $\displaystyle\displaystyle{\hbox{\hskip
26.1993pt\vbox{\hbox{\hskip-26.19928pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,\mathit{x}:\tau_{{\mathrm{1}}}\vdash\mathit{e}:\tau_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
41.03494pt\vbox{\vbox{}\hbox{\hskip-41.03493pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\lambda\mathit{x}:\tau_{{\mathrm{1}}}.\,\mathit{e}:\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}$}}}}}}$
typ-abs $\displaystyle\displaystyle{\hbox{\hskip
54.66832pt\vbox{\hbox{\hskip-54.6683pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{e_{{\mathrm{1}}}}:\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}\qquad\Delta\vdash\mathit{e_{{\mathrm{2}}}}:\tau_{{\mathrm{1}}}$}}}\vbox{}}}\over\hbox{\hskip
23.05237pt\vbox{\vbox{}\hbox{\hskip-23.05237pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{e_{{\mathrm{1}}}}\,\mathit{e_{{\mathrm{2}}}}:\tau_{{\mathrm{2}}}$}}}}}}$
typ-app $\displaystyle\displaystyle{\hbox{\hskip
47.19368pt\vbox{\hbox{\hskip-47.19368pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{e_{{\mathrm{1}}}}:\tau_{{\mathrm{1}}}\qquad\Delta\vdash\mathit{e_{{\mathrm{2}}}}:\tau_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
36.08261pt\vbox{\vbox{}\hbox{\hskip-36.0826pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\langle\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}\rangle:\tau_{{\mathrm{1}}}\times\tau_{{\mathrm{2}}}$}}}}}}$
typ-pair $\displaystyle\displaystyle{\hbox{\hskip
43.99382pt\vbox{\hbox{\hskip-43.9938pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{e}:\tau\qquad\mathit{c}\vdash\tau\,\triangleright\,\tau^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
19.62236pt\vbox{\vbox{}\hbox{\hskip-19.62236pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathit{c}\,\mathit{e}:\tau^{\prime}$}}}}}}$
typ-capp

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

CT-refl $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
20.59546pt\vbox{\vbox{}\hbox{\hskip-20.59546pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{id}_{\tau}\vdash\tau\,\triangleright\,\tau$}}}}}}$
CT-trans $\displaystyle\displaystyle{\hbox{\hskip
53.25397pt\vbox{\hbox{\hskip-53.25397pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{3}}}\qquad\mathit{c_{{\mathrm{1}}}}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
27.7492pt\vbox{\vbox{}\hbox{\hskip-27.7492pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c_{{\mathrm{2}}}}\circ\mathit{c_{{\mathrm{1}}}}\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{3}}}$}}}}}}$
CT-top $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
25.35416pt\vbox{\vbox{}\hbox{\hskip-25.35416pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{top}_{\tau}\vdash\tau\,\triangleright\,\langle\rangle$}}}}}}$
CT-topArr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
32.23332pt\vbox{\vbox{}\hbox{\hskip-32.2333pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{top}_{\rightarrow}\vdash\langle\rangle\,\triangleright\,\langle\rangle\rightarrow\langle\rangle$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
64.61751pt\vbox{\hbox{\hskip-64.6175pt\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
33.33485pt\vbox{\vbox{}\hbox{\hskip-33.33485pt\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 $\displaystyle\displaystyle{\hbox{\hskip
51.99396pt\vbox{\hbox{\hskip-51.99396pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c_{{\mathrm{1}}}}\vdash\tau^{\prime}_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{1}}}\qquad\mathit{c_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{2}}}\,\triangleright\,\tau^{\prime}_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
41.43846pt\vbox{\vbox{}\hbox{\hskip-41.43846pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c_{{\mathrm{1}}}}\rightarrow\mathit{c_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}\,\triangleright\,\tau^{\prime}_{{\mathrm{1}}}\rightarrow\tau^{\prime}_{{\mathrm{2}}}$}}}}}}$
CT-arr CT-pair $\displaystyle\displaystyle{\hbox{\hskip
53.25397pt\vbox{\hbox{\hskip-53.25397pt\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{3}}}$}}}\vbox{}}}\over\hbox{\hskip
39.11275pt\vbox{\vbox{}\hbox{\hskip-39.11275pt\hbox{\hbox{$\displaystyle\displaystyle\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle\vdash\tau_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{3}}}$}}}}}}$
CT-projL $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
30.84065pt\vbox{\vbox{}\hbox{\hskip-30.84064pt\hbox{\hbox{$\displaystyle\displaystyle\pi_{1}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{1}}}\times\tau_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{1}}}$}}}}}}$
CT-projR $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
30.84065pt\vbox{\vbox{}\hbox{\hskip-30.84064pt\hbox{\hbox{$\displaystyle\displaystyle\pi_{2}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\vdash\tau_{{\mathrm{1}}}\times\tau_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{2}}}$}}}}}}$
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
75.9724pt\vbox{\vbox{}\hbox{\hskip-75.9724pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{dist}_{\rightarrow}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}},\tau_{{\mathrm{3}}}}\vdash(\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}})\times(\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{3}}})\,\triangleright\,\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{3}}}$}}}}}}$
CT-distArr

$\mathit{e}\longrightarrow\mathit{e^{\prime}}$ Operational Semantics

step-id $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
19.14073pt\vbox{\vbox{}\hbox{\hskip-19.14072pt\hbox{\hbox{$\displaystyle\displaystyle(\mathsf{id}_{\tau})\,\mathit{v}\longrightarrow\mathit{v}$}}}}}}$
step-trans $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
36.29445pt\vbox{\vbox{}\hbox{\hskip-36.29443pt\hbox{\hbox{$\displaystyle\displaystyle(\mathit{c_{{\mathrm{1}}}}\circ\mathit{c_{{\mathrm{2}}}})\,\mathit{v}\longrightarrow\mathit{c_{{\mathrm{1}}}}\,(\mathit{c_{{\mathrm{2}}}}\,\mathit{v})$}}}}}}$
step-mp $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
50.63007pt\vbox{\vbox{}\hbox{\hskip-50.63005pt\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-top $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
19.55739pt\vbox{\vbox{}\hbox{\hskip-19.55739pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{top}_{\tau}\,\mathit{v}\longrightarrow\langle\rangle$}}}}}}$
step-topArr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
29.59448pt\vbox{\vbox{}\hbox{\hskip-29.59447pt\hbox{\hbox{$\displaystyle\displaystyle(\mathsf{top}_{\rightarrow}\,\langle\rangle)\,\langle\rangle\longrightarrow\langle\rangle$}}}}}}$
step-arr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
56.61668pt\vbox{\vbox{}\hbox{\hskip-56.61667pt\hbox{\hbox{$\displaystyle\displaystyle((\mathit{c_{{\mathrm{1}}}}\rightarrow\mathit{c_{{\mathrm{2}}}})\,\mathit{v_{{\mathrm{1}}}})\,\mathit{v_{{\mathrm{2}}}}\longrightarrow\mathit{c_{{\mathrm{2}}}}\,(\mathit{v_{{\mathrm{1}}}}\,(\mathit{c_{{\mathrm{1}}}}\,\mathit{v_{{\mathrm{2}}}}))$}}}}}}$
step-pair $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
39.21112pt\vbox{\vbox{}\hbox{\hskip-39.21112pt\hbox{\hbox{$\displaystyle\displaystyle\langle\mathit{c_{{\mathrm{1}}}},\mathit{c_{{\mathrm{2}}}}\rangle\,\mathit{v}\longrightarrow\langle\mathit{c_{{\mathrm{1}}}}\,\mathit{v},\mathit{c_{{\mathrm{2}}}}\,\mathit{v}\rangle$}}}}}}$
step-distArr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
59.28342pt\vbox{\vbox{}\hbox{\hskip-59.2834pt\hbox{\hbox{$\displaystyle\displaystyle(\mathsf{dist}_{\rightarrow}^{\tau,\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\,\langle\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\rangle)\,\mathit{v_{{\mathrm{3}}}}\longrightarrow\langle\mathit{v_{{\mathrm{1}}}}\,\mathit{v_{{\mathrm{3}}}},\mathit{v_{{\mathrm{2}}}}\,\mathit{v_{{\mathrm{3}}}}\rangle$}}}}}}$
step-projl $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
26.22795pt\vbox{\vbox{}\hbox{\hskip-26.22795pt\hbox{\hbox{$\displaystyle\displaystyle\pi_{1}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\,\langle\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\rangle\longrightarrow\mathit{v_{{\mathrm{1}}}}$}}}}}}$
step-projr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
26.22795pt\vbox{\vbox{}\hbox{\hskip-26.22795pt\hbox{\hbox{$\displaystyle\displaystyle\pi_{2}^{\tau_{{\mathrm{1}}},\tau_{{\mathrm{2}}}}\,\langle\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\rangle\longrightarrow\mathit{v_{{\mathrm{2}}}}$}}}}}}$
step-beta $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
39.40799pt\vbox{\vbox{}\hbox{\hskip-39.40799pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda\mathit{x}:\tau.\,\mathit{e})\,\mathit{v}\longrightarrow{[}\mathit{v}/\mathit{x}{]}\mathit{e}$}}}}}}$
step-app1 $\displaystyle\displaystyle{\hbox{\hskip
10.36444pt\vbox{\hbox{\hskip-10.36444pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{e_{{\mathrm{1}}}}\longrightarrow\mathit{e^{\prime}_{{\mathrm{1}}}}$}}}\vbox{}}}\over\hbox{\hskip
19.27551pt\vbox{\vbox{}\hbox{\hskip-19.27551pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{e_{{\mathrm{1}}}}\,\mathit{e_{{\mathrm{2}}}}\longrightarrow\mathit{e^{\prime}_{{\mathrm{1}}}}\,\mathit{e_{{\mathrm{2}}}}$}}}}}}$
step-app2 $\displaystyle\displaystyle{\hbox{\hskip
10.36444pt\vbox{\hbox{\hskip-10.36444pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{e_{{\mathrm{2}}}}\longrightarrow\mathit{e^{\prime}_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
20.10887pt\vbox{\vbox{}\hbox{\hskip-20.10887pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{v_{{\mathrm{1}}}}\,\mathit{e_{{\mathrm{2}}}}\longrightarrow\mathit{v_{{\mathrm{1}}}}\,\mathit{e^{\prime}_{{\mathrm{2}}}}$}}}}}}$
step-pair1 $\displaystyle\displaystyle{\hbox{\hskip
10.36444pt\vbox{\hbox{\hskip-10.36444pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{e_{{\mathrm{1}}}}\longrightarrow\mathit{e^{\prime}_{{\mathrm{1}}}}$}}}\vbox{}}}\over\hbox{\hskip
28.16447pt\vbox{\vbox{}\hbox{\hskip-28.16447pt\hbox{\hbox{$\displaystyle\displaystyle\langle\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}\rangle\longrightarrow\langle\mathit{e^{\prime}_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}\rangle$}}}}}}$
step-pair2 $\displaystyle\displaystyle{\hbox{\hskip
10.36444pt\vbox{\hbox{\hskip-10.36444pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{e_{{\mathrm{2}}}}\longrightarrow\mathit{e^{\prime}_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
28.99783pt\vbox{\vbox{}\hbox{\hskip-28.99783pt\hbox{\hbox{$\displaystyle\displaystyle\langle\mathit{v_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}}\rangle\longrightarrow\langle\mathit{v_{{\mathrm{1}}}},\mathit{e^{\prime}_{{\mathrm{2}}}}\rangle$}}}}}}$
step-capp $\displaystyle\displaystyle{\hbox{\hskip
8.96445pt\vbox{\hbox{\hskip-8.96443pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{e}\longrightarrow\mathit{e^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
15.07552pt\vbox{\vbox{}\hbox{\hskip-15.0755pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{c}\,\mathit{e}\longrightarrow\mathit{c}\,\mathit{e^{\prime}}$}}}}}}$

##  Appendix B Additional Definitions

###### Definition B.1 (Type Translation).

$\begin{array}[]{@{\hspace{0mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{\hspace{0mm}}}\mbox{$\mid$}\mathit{A}\mbox{$\mid$}\hfil\hskip
5.69054pt&=\hfil\hskip 5.69054pt&\mathsf{Nat}\\\
\mbox{$\mid$}\top\mbox{$\mid$}\hfil\hskip 5.69054pt&=\hfil\hskip
5.69054pt&\langle\rangle\\\
\mbox{$\mid$}\mathit{A}\rightarrow\mathit{B}\mbox{$\mid$}\hfil\hskip
5.69054pt&=\hfil\hskip
5.69054pt&\mbox{$\mid$}\mathit{A}\mbox{$\mid$}\rightarrow\mbox{$\mid$}\mathit{B}\mbox{$\mid$}\\\
\mbox{$\mid$}\mathit{A}\,\&\,\mathit{B}\mbox{$\mid$}\hfil\hskip
5.69054pt&=\hfil\hskip
5.69054pt&\mbox{$\mid$}\mathit{A}\mbox{$\mid$}\times\mbox{$\mid$}\mathit{B}\mbox{$\mid$}\\\
\end{array}$

###### Definition B.2 (Typing Context Translation).

$\begin{array}[]{@{\hspace{0mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{\hspace{0mm}}}\mbox{$\mid$}\bullet\mbox{$\mid$}\hfil\hskip
5.69054pt&=\hfil\hskip 5.69054pt&\bullet\\\
\mbox{$\mid$}\Gamma,\mathit{x}:\mathit{A}\mbox{$\mid$}\hfil\hskip
5.69054pt&=\hfil\hskip
5.69054pt&\mbox{$\mid$}\Gamma\mbox{$\mid$},\mathit{x}:\mbox{$\mid$}\mathit{A}\mbox{$\mid$}\end{array}$

###### Definition B.3.

$\vdash\Gamma$ Well formed typing context

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
6.94443pt\vbox{\vbox{}\hbox{\hskip-6.94441pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\bullet$}}}}}}$
WFC-empty $\displaystyle\displaystyle{\hbox{\hskip
29.86105pt\vbox{\hbox{\hskip-29.86105pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma\qquad\mathit{x}\notin\Gamma$}}}\vbox{}}}\over\hbox{\hskip
17.56941pt\vbox{\vbox{}\hbox{\hskip-17.56941pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma,\mathit{x}:\mathit{A}$}}}}}}$
WFC-cons

##  Appendix C Context Typing

$\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}$\rightsquigarrow\mathcal{D}$\/}$ Context
Typing I

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
58.36096pt\vbox{\vbox{}\hbox{\hskip-58.36095pt\hbox{\hbox{$\displaystyle\displaystyle[\cdot]:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma\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[\cdot]$\/}$}}}}}}$
CTyp-empty1 $\displaystyle\displaystyle{\hbox{\hskip
106.59131pt\vbox{\hbox{\hskip-106.5913pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}\qquad\Gamma^{\prime}\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}$\/}$}}}\vbox{}}}\over\hbox{\hskip
64.7296pt\vbox{\vbox{}\hbox{\hskip-64.7296pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}\,E_{{\mathrm{2}}}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}\,\mathit{e}$\/}$}}}}}}$
CTyp-appL1 $\displaystyle\displaystyle{\hbox{\hskip
106.59131pt\vbox{\hbox{\hskip-106.5913pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}\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}$\/}\qquad\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}$}}}\vbox{}}}\over\hbox{\hskip
64.7296pt\vbox{\vbox{}\hbox{\hskip-64.7296pt\hbox{\hbox{$\displaystyle\displaystyle
E_{{\mathrm{1}}}\,\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}\,\mathcal{D}$\/}$}}}}}}$
CTyp-appR1 $\displaystyle\displaystyle{\hbox{\hskip
121.74133pt\vbox{\hbox{\hskip-121.74132pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}\qquad\Gamma^{\prime}\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}$\/}\qquad\mathit{A_{{\mathrm{1}}}}*\mathit{A_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
85.15735pt\vbox{\vbox{}\hbox{\hskip-85.15733pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}\,,,\,E_{{\mathrm{2}}}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D},\mathit{e}\rangle$\/}$}}}}}}$
CTyp-mergeL1 $\displaystyle\displaystyle{\hbox{\hskip
121.74133pt\vbox{\hbox{\hskip-121.74132pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}\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}$\/}\qquad\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}\qquad\mathit{A_{{\mathrm{1}}}}*\mathit{A_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
85.15735pt\vbox{\vbox{}\hbox{\hskip-85.15733pt\hbox{\hbox{$\displaystyle\displaystyle
E_{{\mathrm{1}}}\,,,\,\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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},\mathcal{D}\rangle$\/}$}}}}}}$
CTyp-mergeR1 $\displaystyle\displaystyle{\hbox{\hskip
53.85327pt\vbox{\hbox{\hskip-53.85326pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Rightarrow\mathit{B})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}$}}}\vbox{}}}\over\hbox{\hskip
64.26993pt\vbox{\vbox{}\hbox{\hskip-64.26991pt\hbox{\hbox{$\displaystyle\displaystyle(\mathcal{C}:\mathit{A}):(\Gamma\Rightarrow\mathit{B})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}$}}}}}}$
CTyp-anno1

$\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}$\rightsquigarrow\mathcal{D}$\/}$ Context
Typing II

CTyp-empty2 $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
58.36096pt\vbox{\vbox{}\hbox{\hskip-58.36095pt\hbox{\hbox{$\displaystyle\displaystyle[\cdot]:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma\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[\cdot]$\/}$}}}}}}$
CTyp-abs2 $\displaystyle\displaystyle{\hbox{\hskip
87.70107pt\vbox{\hbox{\hskip-87.70107pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime},\mathit{x}:\mathit{A_{{\mathrm{1}}}}\Leftarrow\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\mathcal{D}$\/}\qquad\mathit{x}\notin\Gamma^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
81.72267pt\vbox{\vbox{}\hbox{\hskip-81.72266pt\hbox{\hbox{$\displaystyle\displaystyle\lambda\mathit{x}.\,\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\Leftarrow\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\lambda\mathit{x}.\,\mathcal{D}$\/}$}}}}}}$

$\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}$\rightsquigarrow\mathcal{D}$\/}$ Context
Typing III

$\displaystyle\displaystyle{\hbox{\hskip
106.59131pt\vbox{\hbox{\hskip-106.5913pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}\qquad\Gamma^{\prime}\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}$\/}$}}}\vbox{}}}\over\hbox{\hskip
64.7296pt\vbox{\vbox{}\hbox{\hskip-64.7296pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}\,E_{{\mathrm{2}}}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}\,\mathit{e}$\/}$}}}}}}$
CTyp-appL2 $\displaystyle\displaystyle{\hbox{\hskip
106.59131pt\vbox{\hbox{\hskip-106.5913pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}\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}$\/}\qquad\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}$}}}\vbox{}}}\over\hbox{\hskip
64.7296pt\vbox{\vbox{}\hbox{\hskip-64.7296pt\hbox{\hbox{$\displaystyle\displaystyle
E_{{\mathrm{1}}}\,\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}\,\mathcal{D}$\/}$}}}}}}$
CTyp-appR2 $\displaystyle\displaystyle{\hbox{\hskip
121.74133pt\vbox{\hbox{\hskip-121.74132pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}\qquad\Gamma^{\prime}\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}$\/}\qquad\mathit{A_{{\mathrm{1}}}}*\mathit{A_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
85.15735pt\vbox{\vbox{}\hbox{\hskip-85.15733pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}\,,,\,E_{{\mathrm{2}}}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D},\mathit{e}\rangle$\/}$}}}}}}$
CTyp-mergeL2 $\displaystyle\displaystyle{\hbox{\hskip
121.74133pt\vbox{\hbox{\hskip-121.74132pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma^{\prime}\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}$\/}\qquad\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}\qquad\mathit{A_{{\mathrm{1}}}}*\mathit{A_{{\mathrm{2}}}}$}}}\vbox{}}}\over\hbox{\hskip
85.15735pt\vbox{\vbox{}\hbox{\hskip-85.15733pt\hbox{\hbox{$\displaystyle\displaystyle
E_{{\mathrm{1}}}\,,,\,\mathcal{C}:(\Gamma\Leftarrow\mathit{A})\mapsto(\Gamma^{\prime}\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},\mathcal{D}\rangle$\/}$}}}}}}$
CTyp-mergeR2 $\displaystyle\displaystyle{\hbox{\hskip
53.85327pt\vbox{\hbox{\hskip-53.85326pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Leftarrow\mathit{B})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}$}}}\vbox{}}}\over\hbox{\hskip
58.99217pt\vbox{\vbox{}\hbox{\hskip-58.99216pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:\mathit{A}:(\Gamma\Leftarrow\mathit{B})\mapsto(\Gamma^{\prime}\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\mathcal{D}$\/}$}}}}}}$
CTyp-anno2

$\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\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}$\rightsquigarrow\mathcal{D}$\/}$ Context
Typing IV

$\displaystyle\displaystyle{\hbox{\hskip
87.70107pt\vbox{\hbox{\hskip-87.70107pt\hbox{\hbox{$\displaystyle\displaystyle\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime},\mathit{x}:\mathit{A_{{\mathrm{1}}}}\Leftarrow\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\mathcal{D}$\/}\qquad\mathit{x}\notin\Gamma^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
81.72267pt\vbox{\vbox{}\hbox{\hskip-81.72266pt\hbox{\hbox{$\displaystyle\displaystyle\lambda\mathit{x}.\,\mathcal{C}:(\Gamma\Rightarrow\mathit{A})\mapsto(\Gamma^{\prime}\Leftarrow\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\lambda\mathit{x}.\,\mathcal{D}$\/}$}}}}}}$
CTyp-abs1

##  Appendix D Meta-functions

The three meta-functions we used in Section 5 are formally defined as follows:

###### Definition D.1.

$\begin{array}[]{rcl}\llbracket{[]}\rrbracket_{\&}^{{\mathit{c}},{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}&=&\mathit{c}\\\
\llbracket{\mathit{A},\mathcal{L}}\rrbracket_{\&}^{{\mathit{c}},{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}&=&(\mathsf{id}_{\mbox{$\mid$}\mathit{A}\mbox{$\mid$}}\rightarrow\llbracket{\mathcal{L}}\rrbracket_{\&}^{{\mathit{c}},{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}})\circ\mathsf{dist}_{\rightarrow}^{\mbox{$\mid$}\mathit{A}\mbox{$\mid$},\mbox{$\mid$}\mathcal{L}\to\to\mathit{B_{{\mathrm{1}}}}\mbox{$\mid$},\mbox{$\mid$}\mathcal{L}\to\to\mathit{B_{{\mathrm{2}}}}\mbox{$\mid$}}\\\
\end{array}$

###### Definition D.2.

$\begin{array}[]{rcl}\llbracket{\mathcal{L}}\rrbracket_{\&}^{{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}&=&\llbracket{\mathcal{L}}\rrbracket_{\&}^{{(\mathsf{id}_{\mbox{$\mid$}\mathit{B_{{\mathrm{1}}}}\,\&\,\mathit{B_{{\mathrm{2}}}}\mbox{$\mid$}})},{\mathit{B_{{\mathrm{1}}}}},{\mathit{B_{{\mathrm{2}}}}}}\\\
\end{array}$

###### Definition D.3.

$\begin{array}[]{rcl}\llbracket{[]}\rrbracket_{\top}&=&\mathsf{id}_{\mbox{$\mid$}\top\mbox{$\mid$}}\\\
\llbracket{\mathit{A},\mathcal{L}}\rrbracket_{\top}&=&(\mathsf{top}_{\mbox{$\mid$}\mathit{A}\mbox{$\mid$}}\rightarrow\llbracket{\mathcal{L}}\rrbracket_{\top})\circ\mathsf{top}_{\rightarrow}\\\
\end{array}$

##  Appendix E Complete Derivation Examples of Typing and Algorithmic
Subtyping

##### Typing Derivation Example

Below we show the typing derivation for the example expression
$1:\mathsf{Nat}\,\&\,\mathsf{Nat}$, taken from Section 4.4.

$\displaystyle\displaystyle{\hbox{\hskip
164.7875pt\vbox{\hbox{\hskip-164.78749pt\hbox{\hbox{$\displaystyle\displaystyle\raise
11.0pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
163.12083pt\vbox{\hbox{\hskip-163.12082pt\hbox{\hbox{$\displaystyle\displaystyle\raise
9.47221pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
6.94443pt\vbox{\hbox{\hskip-6.94441pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\bullet$}}}\vbox{}}}\over\hbox{\hskip
36.41656pt\vbox{\vbox{}\hbox{\hskip-36.41656pt\hbox{\hbox{$\displaystyle\displaystyle\bullet\vdash
1\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
1$\/}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
T-nat}}}}}$}}$ }\qquad\raise
11.0pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
100.73204pt\vbox{\hbox{\hskip-100.73203pt\hbox{\hbox{$\displaystyle\displaystyle\raise
10.42888pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
37.81116pt\vbox{\vbox{}\hbox{\hskip-37.81116pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Nat}<:\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\mathsf{id}_{\mathsf{Nat}}$\/}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
S-refl}}}}}$}}$ }\qquad\raise
10.42888pt\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
37.81116pt\vbox{\vbox{}\hbox{\hskip-37.81116pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Nat}<:\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\mathsf{id}_{\mathsf{Nat}}$\/}$}}}}}}$}}\hbox{\hbox{}\hbox
to0.0pt{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
S-refl}}}}}$\hss}}$ }$}}}\vbox{}}}\over\hbox{\hskip
65.59451pt\vbox{\vbox{}\hbox{\hskip-65.59451pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{Nat}<:\mathsf{Nat}\,\&\,\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\langle\mathsf{id}_{\mathsf{Nat}},\mathsf{id}_{\mathsf{Nat}}\rangle$\/}$}}}}}}$}}\hbox{\hbox{}\hbox
to0.0pt{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
S-and}}}}}$\hss}}$ }$}}}\vbox{}}}\over\hbox{\hskip
72.39995pt\vbox{\vbox{}\hbox{\hskip-72.39995pt\hbox{\hbox{$\displaystyle\displaystyle\bullet\vdash
1\Leftarrow\mathsf{Nat}\,\&\,\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\langle\mathsf{id}_{\mathsf{Nat}},\mathsf{id}_{\mathsf{Nat}}\rangle\,1$\/}$}}}}}}$}}\hbox{\hbox{}\hbox
to0.0pt{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
T-sub}}}}}$\hss}}$ }$}}}\vbox{}}}\over\hbox{\hskip
95.7333pt\vbox{\vbox{}\hbox{\hskip-95.73329pt\hbox{\hbox{$\displaystyle\displaystyle\bullet\vdash
1:\mathsf{Nat}\,\&\,\mathsf{Nat}\Rightarrow\mathsf{Nat}\,\&\,\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\langle\mathsf{id}_{\mathsf{Nat}},\mathsf{id}_{\mathsf{Nat}}\rangle\,1$\/}$}}}}}}$
T-anno

The generated target term is
$\langle\mathsf{id}_{\mathsf{Nat}},\mathsf{id}_{\mathsf{Nat}}\rangle\,1$,
which reduces to $\langle 1,1\rangle$, following the operational semantics of
$\lambda_{\mathit{c}}^{\mathsf{MP}}$.

##### Algorithmic Subtyping Derivation Example

Here we illustrate how the algorithm of Section 5.1 works with an example
derivation. Due to space restrictions, we shorten $\mathsf{Nat}$,
$\mathsf{String}$, and $\mathsf{Bool}$ to $\mathsf{N}$, $\mathsf{S}$, and
$\mathit{B}$, respectively, and omit all mention of coercions.

$\displaystyle\displaystyle{\hbox{\hskip
150.39038pt\vbox{\hbox{\hskip-150.39037pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
133.37233pt\vbox{\hbox{\hskip-133.37233pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
115.62929pt\vbox{\hbox{\hskip-115.62929pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
53.26048pt\vbox{\hbox{\hskip-53.26047pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
19.83894pt\vbox{\vbox{}\hbox{\hskip-19.83893pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\mathsf{S}}\prec:{\top}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AR-top}}}}}$}}$ }$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
D_{2}$}}}}\vbox{}}}\over\hbox{\hskip
99.11124pt\vbox{\vbox{}\hbox{\hskip-99.11122pt\hbox{\hbox{$\displaystyle\displaystyle{([],\mathsf{S})};{[]};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{N}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AL-arr}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
59.4223pt\vbox{\vbox{}\hbox{\hskip-59.4223pt\hbox{\hbox{$\displaystyle\displaystyle{([],\mathsf{S})}\mathrel{\vdash_{\text{R}}}{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{N}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AR-nat}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
56.64452pt\vbox{\vbox{}\hbox{\hskip-56.64452pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{S}\rightarrow\mathsf{N}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AR-arr}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
48.75006pt\vbox{\vbox{}\hbox{\hskip-48.75006pt\hbox{\hbox{$\displaystyle\displaystyle{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{S}\rightarrow\mathsf{N}}$}}}}}}$
A-main

where $D_{2}$ is the following derivation:

$\displaystyle\displaystyle{\hbox{\hskip
119.16469pt\vbox{\hbox{\hskip-119.16467pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
102.17163pt\vbox{\hbox{\hskip-102.17163pt\hbox{\hbox{$\displaystyle\displaystyle
D_{3}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
69.25009pt\vbox{\vbox{}\hbox{\hskip-69.25008pt\hbox{\hbox{$\displaystyle\displaystyle{[]};{(\mathsf{S},[])};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\mathsf{N}}\prec:{\mathsf{N}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AL-nat}}}}}$}}$ }$}}}}\vbox{}}}\over\hbox{\hskip
75.29178pt\vbox{\vbox{}\hbox{\hskip-75.29176pt\hbox{\hbox{$\displaystyle\displaystyle{[]};{(\mathsf{S},[])};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\mathsf{B}\rightarrow\mathsf{N}}\prec:{\mathsf{N}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AL-mp}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
88.27788pt\vbox{\vbox{}\hbox{\hskip-88.27788pt\hbox{\hbox{$\displaystyle\displaystyle{[]};{(\mathsf{S},[])};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})}\prec:{\mathsf{N}}$}}}}}}$
AL-and2

where $D_{3}$ is the following derivation:

$\displaystyle\displaystyle{\hbox{\hskip
135.16402pt\vbox{\hbox{\hskip-135.16402pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
115.42096pt\vbox{\hbox{\hskip-115.42096pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
53.26048pt\vbox{\hbox{\hskip-53.26047pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
19.83894pt\vbox{\vbox{}\hbox{\hskip-19.83893pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\mathsf{S}}\prec:{\top}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AR-top}}}}}$}}$ }$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
D_{4}$}}}}\vbox{}}}\over\hbox{\hskip
98.90291pt\vbox{\vbox{}\hbox{\hskip-98.9029pt\hbox{\hbox{$\displaystyle\displaystyle{([],\mathsf{S})};{[]};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{B}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AL-arr}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
59.21397pt\vbox{\vbox{}\hbox{\hskip-59.21397pt\hbox{\hbox{$\displaystyle\displaystyle{([],\mathsf{S})}\mathrel{\vdash_{\text{R}}}{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{B}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AR-bool}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
56.43619pt\vbox{\vbox{}\hbox{\hskip-56.43619pt\hbox{\hbox{$\displaystyle\displaystyle{[]}\mathrel{\vdash_{\text{R}}}{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\prec:{\mathsf{S}\rightarrow\mathsf{B}}$}}}}}}$
AR-arr

where $D_{4}$ is the following derivation:

$\displaystyle\displaystyle{\hbox{\hskip
87.2432pt\vbox{\hbox{\hskip-87.24318pt\hbox{\hbox{$\displaystyle\displaystyle\hbox{$\displaystyle{\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
68.00012pt\vbox{\vbox{}\hbox{\hskip-68.0001pt\hbox{\hbox{$\displaystyle\displaystyle{([],\mathsf{S})};{[]};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\mathsf{B}}\prec:{\mathsf{B}}$}}}}}}$}}\hbox{\hbox{}\hbox{$\displaystyle\;\hbox{\small\small{{\small\mbox{{\tt\sc
AL-bool}}}}}$}}$ }$}}}\vbox{}}}\over\hbox{\hskip
87.23624pt\vbox{\vbox{}\hbox{\hskip-87.23624pt\hbox{\hbox{$\displaystyle\displaystyle{([],\mathsf{S})};{[]};{\top\rightarrow(\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N}))}\vdash_{\text{L}}{\mathsf{B}\,\&\,(\mathsf{B}\rightarrow\mathsf{N})}\prec:{\mathsf{B}}$}}}}}}$
AL-and1

##  Appendix F The Logical Relation for $\lambda_{i}^{\mathsf{MP}}$

$\begin{array}[]{rcl}\lx<EMAIL_ADDRESS>(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\mathsf{Nat};\mathsf{Nat}\rrbracket&~{}\triangleq{}&\exists
i,\mathit{v_{{\mathrm{1}}}}=\mathit{v_{{\mathrm{2}}}}=i\\\\[5.69054pt]
(\langle\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\rangle,\mathit{v_{{\mathrm{3}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}}\times\tau_{{\mathrm{2}}};\tau_{{\mathrm{3}}}\rrbracket&~{}\triangleq{}&(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{3}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{3}}}\rrbracket\\\
{}{}\hfil&&\land~{}~{}(\mathit{v_{{\mathrm{2}}}},\mathit{v_{{\mathrm{3}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{2}}};\tau_{{\mathrm{3}}}\rrbracket\\\\[5.69054pt]
(\mathit{v_{{\mathrm{3}}}},\langle\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\rangle)\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{3}}};\tau_{{\mathrm{1}}}\times\tau_{{\mathrm{2}}}\rrbracket&~{}\triangleq{}&(\mathit{v_{{\mathrm{3}}}},\mathit{v_{{\mathrm{1}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{3}}};\tau_{{\mathrm{1}}}\rrbracket\\\
{}{}\hfil&&\land~{}~{}(\mathit{v_{{\mathrm{3}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{3}}};\tau_{{\mathrm{2}}}\rrbracket\\\\[5.69054pt]
(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}};\tau\rrbracket&~{}\triangleq{}&~{}\text{\hskip
51.21495pt($\tau$ not function type)}\\\
\lx<EMAIL_ADDRESS>(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau;\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}\rrbracket&~{}\triangleq{}&\text{\hskip
51.21495pt($\tau$ not function type)}\\\
\lx<EMAIL_ADDRESS>(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}};\tau_{{\mathrm{3}}}\rightarrow\tau_{{\mathrm{4}}}\rrbracket&~{}\triangleq{}&\\\
\lx@intercol\hfil\begin{array}[]{c@{\quad}l}&\left(\begin{array}[]{l}\begin{aligned}
&\forall\mathit{v}~{}\mathit{v^{\prime}}~{}\tau_{{\mathrm{0}}}~{}\tau^{\prime}_{{\mathrm{0}}}~{}\mathit{c}~{}\mathit{c^{\prime}}~{}\mathit{d}~{}\mathit{d^{\prime}}~{}\tau_{{\mathrm{01}}}~{}\tau_{{\mathrm{02}}},\\\
&\mathit{d}\vdash\tau_{{\mathrm{01}}}\,\triangleright\,\tau_{{\mathrm{1}}}\Rightarrow\mathit{d^{\prime}}\vdash\tau_{{\mathrm{02}}}\,\triangleright\,\tau_{{\mathrm{3}}}\Rightarrow(\mathit{d}\,\mathit{v},\mathit{d^{\prime}}\,\mathit{v^{\prime}})\in\mathcal{E}^{(\mathit{v}:\tau_{{\mathrm{01}}};\mathit{v^{\prime}}:\tau_{{\mathrm{02}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{3}}}\rrbracket\Rightarrow\\\
&\mathit{c}\vdash\tau^{\prime}_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{01}}}\rightarrow\tau_{{\mathrm{0}}}\Rightarrow\mathit{c^{\prime}}\vdash\tau^{\prime}_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{02}}}\rightarrow\tau^{\prime}_{{\mathrm{0}}}\Rightarrow\\\
&(\mathit{v_{{\mathrm{1}}}}\,(\mathit{d}\,\mathit{v}),\mathit{v_{{\mathrm{2}}}}\,(\mathit{d^{\prime}}\,\mathit{v^{\prime}}))\in\mathcal{E}^{(\langle\mathit{v_{{\mathrm{1}}}}\,(\mathit{d}\,\mathit{v}),\mathit{c}\,\mathit{v^{\prime}_{{\mathrm{1}}}}\,\mathit{v}\rangle:\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{0}}};\langle\mathit{v_{{\mathrm{2}}}}\,(\mathit{d^{\prime}}\,\mathit{v^{\prime}}),\mathit{c^{\prime}}\,\mathit{v^{\prime}_{{\mathrm{2}}}}\,\mathit{v^{\prime}}\rangle:\tau_{{\mathrm{4}}}\times\tau^{\prime}_{{\mathrm{0}}})}\llbracket\tau_{{\mathrm{2}}};\tau_{{\mathrm{4}}}\rrbracket\end{aligned}\end{array}\right)\\\
\wedge&\forall\mathit{c},\mathit{c}\vdash\tau^{\prime}_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{1}}}\Rightarrow(\mathit{v_{{\mathrm{1}}}}\,(\mathit{c}\,\mathit{v^{\prime}_{{\mathrm{1}}}}),\mathit{v_{{\mathrm{2}}}})\in\mathcal{E}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{2}}};\tau_{{\mathrm{3}}}\rightarrow\tau_{{\mathrm{4}}}\rrbracket\\\
\wedge&\forall\mathit{c},\mathit{c}\vdash\tau^{\prime}_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{3}}}\Rightarrow(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}\,(\mathit{c}\,\mathit{v^{\prime}_{{\mathrm{2}}}}))\in\mathcal{E}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}};\tau_{{\mathrm{4}}}\rrbracket\\\\[5.69054pt]
<EMAIL_ADDRESS>(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket&~{}\triangleq{}&\mathmakebox[0pt]{~{}~{}~{}\mathsf{true}}\text{\hskip
51.21495pt(otherwise)}\\\ \\\
\lx<EMAIL_ADDRESS>(\mathit{e_{{\mathrm{1}}}},\mathit{e_{{\mathrm{2}}}})\in\mathcal{E}^{(\mathit{e^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{e^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket&~{}\triangleq{}&\\\
\lx@intercol\hfil\exists\mathit{v_{{\mathrm{1}}}}\,\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}_{{\mathrm{1}}}}\,\mathit{v^{\prime}_{{\mathrm{2}}}},\begin{array}[t]{r}\mathit{e_{{\mathrm{1}}}}\longrightarrow^{*}\mathit{v_{{\mathrm{1}}}}~{}\land~{}\mathit{e_{{\mathrm{2}}}}\longrightarrow^{*}\mathit{v_{{\mathrm{2}}}}\land~{}\mathit{e^{\prime}_{{\mathrm{1}}}}\longrightarrow^{*}\mathit{v^{\prime}_{{\mathrm{1}}}}~{}\land~{}\mathit{e^{\prime}_{{\mathrm{2}}}}\longrightarrow^{*}\mathit{v^{\prime}_{{\mathrm{2}}}}\\\
\wedge\>(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket\end{array}\lx@intercol\end{array}$

Figure 11. Logical Relations

Figure 11 shows the $\lambda_{i}^{\mathsf{MP}}$ definitions of the logical
relations $\mathcal{V}$ for values and $\mathcal{E}$ for terms. These
definitions reconcile the context-dependent nature of modus ponens with the
structural recursion needed for the well-foundedness of the definitions.

The intent of the relations is of course the same as in NeColus, to only allow
semantically indistinguishable overlap. Also the three general principles at
the basis of their definition are preserved: 1) two values of type
$\mathsf{Nat}$ have indistinguishable overlap only when they are identical, 2)
related functions should take related inputs to related outputs, and 3) the
coercion compatibility property should hold.

The first novelty to deal with modus ponens is that the family of value
relations is equipped with additional indices
$\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}}$ and
$\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}}$ to keep
track of the values that $\mathit{v_{{\mathrm{1}}}}$ and
$\mathit{v_{{\mathrm{2}}}}$ are components of; we call these indices the
respective _contexts_ of $\mathit{v_{{\mathrm{1}}}}$ and
$\mathit{v_{{\mathrm{2}}}}$. To be precise, the intention is that we use
$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v^{\prime}_{{\mathrm{1}}}}:\tau^{\prime}_{{\mathrm{1}}};\mathit{v^{\prime}_{{\mathrm{2}}}}:\tau^{\prime}_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket$
only when there exist coercions $\mathit{c_{{\mathrm{1}}}}$ and
$\mathit{c_{{\mathrm{2}}}}$ such that firstly
$\mathit{c_{{\mathrm{1}}}}\vdash\tau^{\prime}_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{1}}}$
and
$\mathit{c_{{\mathrm{2}}}}\vdash\tau^{\prime}_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{2}}}$,
and secondly
$\mathit{c_{{\mathrm{1}}}}\,\mathit{v^{\prime}_{{\mathrm{1}}}}\longrightarrow^{*}\mathit{v_{{\mathrm{1}}}}$
and
$\mathit{c_{{\mathrm{2}}}}\,\mathit{v^{\prime}_{{\mathrm{2}}}}\longrightarrow^{*}\mathit{v_{{\mathrm{2}}}}$.
When the contexts and the values are the same, we sometimes omit those
additional indices, i.e., we abbreviate
$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}^{(\mathit{v_{{\mathrm{1}}}}:\tau_{{\mathrm{1}}};\mathit{v_{{\mathrm{2}}}}:\tau_{{\mathrm{2}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket$
to
$(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\in\mathcal{V}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{2}}}\rrbracket$.
The term relation $\mathcal{E}$ is equipped with similar context indices; the
one difference is that, just like the elements in the term relation, these
indices are terms rather than values.

##### Unmodified Cases

The first three cases of the $\mathcal{V}$ definition are essentially the same
as those of NeColus: Two natural numbers are related if they are identical,
which is a direct implementation of the first general principle. Also, a pair
is related to another value if both components of the pair are related to that
value, which is a similar specialisation of the coercion compatibility
property to coercions $\pi_{1}$ and $\pi_{2}$.

##### New Modus Ponens Cases

The next two cases that relate functions to non-functions are different from
NeColus because of the addition of the modus ponens coercion. In NeColus all
functions are related to all non-functions because the only common types they
can be coerced to are top-like types whose values are indistinguishable.

This is not so in $\lambda_{\mathit{c}}^{\mathsf{MP}}$, where the S-mp rule
can be used to derive a non-function value from a function. Hence, our logical
relation states that a function and non-function are related only if all S-mp-
enabled applications of the function are related to the non-function value.
Using modus ponens implies that not only the function, but also its argument
is derived from the original value. This is why the two symmetric cases of the
relation universally quantify over all coercions that derive an argument of
the appropriate input type.

##### New Function Case

The one-but-last case, which relates two functions, is the most complicated
one. It states that two functions are related iff they satisfy three
conditions. These three conditions concern the two different ways in which the
functions can be applied to an argument.

The second and third condition are a new way compared to NeColus and analogous
to function/non-function cases; these are the cases where one of the two
functions is applied to an argument through S-mp. They expose that
$\langle\lambda\mathit{x}:\mathsf{Nat}.\,\lambda\mathit{y}:\mathsf{Bool}.\,\mathit{y},1\rangle$
can be coerced to $\lambda\mathit{y}:\mathsf{Bool}.\,\mathit{y}$ and thus has
distinguishable overlap with, for instance,
$\lambda\mathit{y}:\mathsf{Bool}.\,\mathsf{true}$.

The first condition corresponds to the NeColus condition for function types
and captures the main design principle that related functions take related
inputs to related outputs. However, as a consequence of modus ponens
subtyping, the formulation is much more elaborate. First, we need to consider
the context indices. An explicit function application demarcates the point
where the implicit subtyping derivation ends and, therefore, the previous
context is abandoned. One might thus expect the following much simpler
formulation of the condition, where the result of the function application
becomes its own new context:

$\forall(\mathit{v},\mathit{v^{\prime}})\in\mathcal{V}^{(\mathit{v}:\tau_{{\mathrm{1}}};\mathit{v^{\prime}}:\tau_{{\mathrm{3}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{3}}}\rrbracket,~{}(\mathit{v_{{\mathrm{1}}}}\,\mathit{v},\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}})\in\mathcal{E}^{(\mathit{v_{{\mathrm{1}}}}\,\mathit{v}:\tau_{{\mathrm{2}}};\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}}:\tau_{{\mathrm{4}}})}\llbracket\tau_{{\mathrm{2}}};\tau_{{\mathrm{4}}}\rrbracket$

Sadly, this formulation does not properly account for functions that – unlike
$\mathit{v_{{\mathrm{1}}}}$ and $\mathit{v_{{\mathrm{2}}}}$ – can be derived
from the context without them being structural components. Consider the
composition of multiple subcomponents by means of the S-distArr rule. For
instance, that rule can derive from the
context$\langle\lambda\mathit{x}:\mathsf{Bool}.\,1,\lambda\mathit{x}:\mathsf{Bool}.\,\mathsf{true}\rangle$
the function $\lambda\mathit{x}:\mathsf{Bool}.\,\langle
1,\mathsf{true}\rangle$ which is not a syntactic component of the initial
type. In NeColus, we do not have to separately account for these cases,
because the components of the function body never interact and can thus be
considered separately. For that reason, the logical relation of NeColus does
not explicitly have to consider S-distArr. However, in
$\lambda_{i}^{\mathsf{MP}}$ matters are different because of S-mp. When the
context is
$\langle\lambda\mathit{x}:\mathsf{Bool}.\,\lambda\mathit{y}:\mathsf{Bool}.\,1,\lambda\mathit{x}:\mathsf{Bool}.\,\mathsf{true}\rangle$,
then using S-distArr we can derive the function
$\lambda\mathit{x}:\mathsf{Bool}.\,\langle\lambda\mathit{y}:\mathsf{Bool}.\,1,\mathsf{true}\rangle$.
When this function is explicitly applied to a value, we get a new original
value $\langle\lambda\mathit{y}:\mathsf{Bool}.\,1,\mathsf{true}\rangle$ whose
two components can interact through S-mp. Thus, just checking
$\lambda\mathit{x}:\mathsf{Bool}.\,\lambda\mathit{y}:\mathsf{Bool}.\,1$ on its
own is insufficient. To reckon with all ways in which the functions
$\mathit{v_{{\mathrm{1}}}}$ and $\mathit{v_{{\mathrm{2}}}}$ under
consideration can be combined by means of S-distarr with other functions
derived from the context, we augment the condition as shown in the following
extended condition:

$\displaystyle\forall(\mathit{v},\mathit{v^{\prime}})\in\mathcal{E}^{(\mathit{v}:\tau_{{\mathrm{1}}};\mathit{v^{\prime}}:\tau_{{\mathrm{3}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{3}}}\rrbracket,\,\forall\mathit{c}\vdash\tau^{\prime}_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{0}}},\,\forall\mathit{c^{\prime}}\vdash\tau^{\prime}_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{3}}}\rightarrow\tau^{\prime}_{{\mathrm{0}}},$
$\displaystyle~{}~{}~{}(\langle\mathit{v_{{\mathrm{1}}}}\,\mathit{v},\mathit{c}\,\mathit{v^{\prime}_{{\mathrm{1}}}}\,\mathit{v}\rangle,\langle\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}},\mathit{c^{\prime}}\,\mathit{v^{\prime}_{{\mathrm{2}}}}\,\mathit{v^{\prime}}\rangle)\in\mathcal{E}^{(\langle\mathit{v_{{\mathrm{1}}}}\,\mathit{v},\mathit{c}\,\mathit{v^{\prime}_{{\mathrm{1}}}}\,\mathit{v}\rangle:\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{0}}};\langle\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}},\mathit{c^{\prime}}\,\mathit{v^{\prime}_{{\mathrm{2}}}}\,\mathit{v^{\prime}}\rangle:\tau_{{\mathrm{4}}}\times\tau^{\prime}_{{\mathrm{0}}})}\llbracket\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{0}}};\tau_{{\mathrm{4}}}\times\tau^{\prime}_{{\mathrm{0}}}\rrbracket$

Yet, this formulation breaks the well-foundedness of the recursive definition
because $\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{0}}}$ and
$\tau_{{\mathrm{4}}}\times\tau^{\prime}_{{\mathrm{0}}}$ are not necessarily
smaller than $\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{2}}}$ and
$\tau_{{\mathrm{3}}}\rightarrow\tau_{{\mathrm{4}}}$, respectively.
Fortunately, we can mention the additional components only in the context
index to make them available for interaction through S-mp. This restores the
well-foundedness of the definition.

$\displaystyle\forall(\mathit{v},\mathit{v^{\prime}})\in\mathcal{E}^{(\mathit{v}:\tau_{{\mathrm{1}}};\mathit{v^{\prime}}:\tau_{{\mathrm{3}}})}\llbracket\tau_{{\mathrm{1}}};\tau_{{\mathrm{3}}}\rrbracket,\,\forall\mathit{c}\vdash\tau^{\prime}_{{\mathrm{1}}}\,\triangleright\,\tau_{{\mathrm{1}}}\rightarrow\tau_{{\mathrm{0}}},\,\forall\mathit{c^{\prime}}\vdash\tau^{\prime}_{{\mathrm{2}}}\,\triangleright\,\tau_{{\mathrm{3}}}\rightarrow\tau^{\prime}_{{\mathrm{0}}},$
$\displaystyle~{}~{}~{}(\mathit{v_{{\mathrm{1}}}}\,\mathit{v},\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}})\in\mathcal{E}^{(\langle\mathit{v_{{\mathrm{1}}}}\,\mathit{v},\mathit{c}\,\mathit{v^{\prime}_{{\mathrm{1}}}}\,\mathit{v}\rangle:\tau_{{\mathrm{2}}}\times\tau_{{\mathrm{0}}};\langle\mathit{v_{{\mathrm{2}}}}\,\mathit{v^{\prime}},\mathit{c^{\prime}}\,\mathit{v^{\prime}_{{\mathrm{2}}}}\,\mathit{v^{\prime}}\rangle:\tau_{{\mathrm{4}}}\times\tau^{\prime}_{{\mathrm{0}}})}\llbracket\tau_{{\mathrm{2}}};\tau_{{\mathrm{4}}}\rrbracket$

There is one last twist. Rule S-distArr can still be used on two function
components with different domains. In particular, we can make the domains
agree by means of the contra-variant part of the S-arr rule. For instance, we
can derive
$\lambda\mathit{x}:\mathsf{Nat}\times\mathsf{Bool}.\,\langle\lambda\mathit{y}:\mathsf{Bool}.\,1,\mathsf{true}\rangle$
from the original value
$\langle\lambda\mathit{x}:\mathsf{Bool}.\,\lambda\mathit{y}:\mathsf{Bool}.\,1,\lambda\mathit{x}:\mathsf{Nat}\times\mathsf{Bool}.\,\mathsf{true}\rangle$