gray!50 gray!0 stix@largesymbols"0E stix@largesymbols"0F

# Structural Subtyping as Parametric Polymorphism

Wenhao Tang  0009-0000-6589-3821 The University of EdinburghUK
<EMAIL_ADDRESS>,  Daniel Hillerström  0000-0003-4730-9315 Huawei Zurich
Research CenterSwitzerland<EMAIL_ADDRESS>,  James McKinna
0000-0001-6745-2560 Heriot-Watt UniversityUK<EMAIL_ADDRESS>,  Michel
Steuwer  0000-0001-5048-0741 Technische Universität BerlinGermany The
University of EdinburghUK<EMAIL_ADDRESS>,  Ornela Dardha
0000-0001-9927-7875 University of GlasgowUK<EMAIL_ADDRESS>,
Rongxiao Fu  0009-0005-6966-4037 The University of EdinburghUK
<EMAIL_ADDRESS>and  Sam Lindley  0000-0002-1360-4714 The University of
EdinburghUK<EMAIL_ADDRESS>
(2023; 2023-04-14; 2023-08-27)

###### Abstract.

Structural subtyping and parametric polymorphism provide similar flexibility
and reusability to programmers. For example, both features enable the
programmer to provide a wider record as an argument to a function that expects
a narrower one. However, the means by which they do so differs substantially,
and the precise details of the relationship between them exists, at best, as
folklore in literature.

In this paper, we systematically study the relative expressive power of
structural subtyping and parametric polymorphism. We focus our investigation
on establishing the extent to which parametric polymorphism, in the form of
row and presence polymorphism, can encode structural subtyping for variant and
record types. We base our study on various Church-style $\lambda$-calculi
extended with records and variants, different forms of structural subtyping,
and row and presence polymorphism.

We characterise expressiveness by exhibiting compositional translations
between calculi. For each translation we prove a type preservation and
operational correspondence result. We also prove a number of non-existence
results. By imposing restrictions on both source and target types, we reveal
further subtleties in the expressiveness landscape, the restrictions enabling
otherwise impossible translations to be defined. More specifically, we prove
that full subtyping cannot be encoded via polymorphism, but we show that
several restricted forms of subtyping can be encoded via particular forms of
polymorphism.

row types, subtyping, polymorphism, expressiveness

††copyright: rightsretained††doi: 10.1145/3622836††journalyear:
2023††submissionid: oopslab23main-p306-p††journal: PACMPL††journalvolume:
7††journalnumber: OOPSLA2††article: 260††publicationmonth: 10††ccs: Theory of
computation Type theory††ccs: Software and its engineering Polymorphism††ccs:
Software and its engineering Functional languages

##  1\. Introduction

Subtyping and parametric polymorphism offer two distinct means for writing
modular and reusable code. Subtyping allows one value to be substituted for
another provided that the type of the former is a subtype of that of the
latter (Reynolds, 1980; Cardelli, 1988). Parametric polymorphism allows
functions to be defined generically over arbitrary types (Girard, 1972;
Reynolds, 1974).

There are two main approaches to _syntactic_ subtyping: nominal subtyping
(Birtwistle et al., 1979) and structural subtyping (Cardelli and Wegner, 1985;
Cardelli, 1988, 1984). The former defines a subtyping relation as a collection
of explicit constraints between named types. The latter defines a subtyping
relation inductively over the structure of types. This paper is concerned with
the latter. For programming languages with variant types (constructor-labelled
sums) and record types (field-labelled products) it is natural to define a
notion of structural subtyping. We may always treat a variant with a
collection of constructors as a variant with an _extended_ collection of
constructors (i.e., variant subtyping is covariant). Dually, we may treat a
record with a collection of fields as a record with a _restricted_ collection
of those fields (i.e., record subtyping is contravariant).

We can implement similar functionality to record and variant subtyping using
_row polymorphism_ (Wand, 1987; Rémy, 1994). A _row_ is a mapping from labels
to types and is thus a common ingredient for defining both variants and
records. Row polymorphism is a form of parametric polymorphism that allows us
to abstract over the extension of a row. Intuitively, by abstracting over the
possible extension of a variant or record we can simulate the act of
substitution realised by structural subtyping. Such intuitions are folklore,
but pinning them down turns out to be surprisingly subtle. In this paper we
make them precise by way of translations between a series of different core
calculi enjoying type preservation and operational correspondence results as
well as non-existence results. We show that though folklore intuitions are to
some extent correct, exactly how they manifest in practice is remarkably
dependent on what assumptions we make, and much more nuanced than we
anticipated. We believe that our results are not just of theoretical interest.
It is important to carefully analyse and characterise the relative expressive
power of different but related features to understand the extent to which they
overlap.

To be clear, there is plenty of other work that hinges on inducing a subtyping
relation based on generalisation (i.e., polymorphism) — and indeed this is the
basis for principal types in Hindley-Milner type inference — but this paper is
about something quite different, namely encoding prior notions of structural
subtyping using polymorphism. In short, principal types concern polymorphism
as subtyping, whereas this paper concerns subtyping as polymorphism.

In order to distil the features we are interested in down to their essence and
eliminate the interference on the expressive power of other language features
(such as higher-order store), we take plain Church-style call-by-name simply-
typed $\lambda$-calculus ($\lambda$) as our starting point and consider the
relative expressive power of minimal extensions in turn. We begin by insisting
on writing explicit upcasts, type abstractions, and type applications in order
to expose structural subtyping and parametric polymorphism at the term level.
Later we also consider ML-style calculi, enabling new expressiveness results
by exploiting the type inference for rank-1 polymorphism. For the dynamic
semantics, we focus on the reduction theory generated from the $\beta$-rules,
adding further $\beta$-rules for each term constructor and upcast rules for
witnessing subtyping.

First we extend the simply-typed $\lambda$-calculus with variants
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$), which we then further augment
with _simple subtyping_
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$) that only considers
the subtyping relation shallowly on variant and record constructors (width
subtyping), and (higher-rank) row polymorphism
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$), respectively. Dually,
we extend the simply-typed $\lambda$-calculus with records
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$), which we then
further augment with simple subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$) and
(higher-rank) _presence polymorphism_
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$),
respectively. Presence polymorphism (Rémy, 1994) is a kind of dual to row
polymorphism that allows us to abstract over which fields are present or
absent from a record independently of their potential types, supporting a
restriction of a collection of record fields, similarly to record subtyping.
We then consider richer extensions with strictly covariant subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{co}}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$),
which propagates the subtyping relation through strictly covariant positions,
and full subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{full}}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$),
which propagates the subtyping relation through any positions. We also
consider target languages with both row and presence polymorphism
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho\theta}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho\theta}$). Our
initial investigations make essential use of higher-rank polymorphism.
Subsequently, we consider ML-like calculi with rank-1 row or presence
polymorphism ($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho
1}$, $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta 1}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho 1}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta 1}$), which admit Hindley-
Milner type inference (Damas and Milner, 1982) without requirements of type
annotations or explicit type abstractions and applications. The focus on
rank-1 polymorphism demands a similar restriction to the calculi with
subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}1}^{\leqslant\mathrm{full}}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}1}^{\leqslant\mathrm{full}}$,
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}2}^{\leqslant\mathrm{full}}$), which
constrains the positions where records and variants can appear in types.

In this paper, we will consider only correspondences expressed as
_compositional translations_ inductively defined on language constructs
following Felleisen (1991). In order to give a refined characterisation of
expressiveness and usability of the type systems of different calculi, we make
use of two orthogonal notions of _local_ and _type-only_ translations.

  * •

A _local_ translation restricts which features are translated in a non-trivial
way. It provides non-trivial translations only of constructs of interest
(e.g., record types, record construction and destruction, when considering
record subtyping), and is homomorphic on other constructs; a _global_
translation may allow any construct to have a non-trivial translation.

  * •

A _type-only_ translation restricts which features a translation can use in
the target language. Every term must translate to itself modulo constructs
that serve only to manipulate types (e.g., type abstraction and application);
a _term-involved_ translation has no such restriction.

Local translations capture the intuition that a feature can be expressed
locally as a macro rather than having to be implemented by globally changing
an entire program (Felleisen, 1991). Type-only translations capture the
intuition that a feature can be expressed solely by adding or removing type
manipulation operations (such as upcasts, type abstraction, and type
application) in terms, thereby enabling a more precise comparison between the
expressiveness of different type system features.

This paper gives a _precise account of the relationship between subtyping and
polymorphism for records and variants_. We present relative expressiveness
results by way of a series of translations between calculi, type preservation
proofs, operational correspondence proofs, and non-existence proofs.

${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}}$${{\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}2}^{\leqslant\mathrm{full}}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta
1}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{co}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho\theta}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}}$${{\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}1}^{\leqslant\mathrm{full}}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho
1}}$${\lambda}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}}$${{\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}1}^{\leqslant\mathrm{full}}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta
1}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho\theta}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}}$${{\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho
1}}$$\scriptstyle{\S\ref{sec:encode-stlcvarsub-
stlcvarrow}}$$\scriptstyle{\S\ref{sec:encode-stlcvarsub-
stlcvar}}$$\scriptstyle{\S\ref{sec:encode-stlcrecsub-
stlcrec}}$$\scriptstyle{\S\ref{sec:encode-stlcrecsub-
stlcrecpre}}$$\scriptstyle{\S\ref{sec:swapping-row-and-
pre}}$$\scriptstyle{\S\ref{sec:swapping-row-and-
pre}}$$\scriptstyle{\S\ref{sec:non-full-
subtyping}}$$\scriptstyle{\S\ref{sec:encode-co-
subtyping}}$$\scriptstyle{\S\ref{sec:encode-full-
subtyping}}$$\scriptstyle{\S\ref{sec:encode-full-
subtyping}}$$\scriptstyle{\S\ref{sec:non-stlcvarsubco-
stlcvarrowpre}}$extensionlocal type-onlylocal term-involvedglobal type-
onlynon-existence of type-only$\scriptstyle{\S\ref{sec:prenex-
polymorphism}}$$\scriptstyle{\S\ref{sec:prenex-
polymorphism}}$$\scriptstyle{\S\ref{sec:prenex-
polymorphism}}$$\scriptstyle{\S\ref{sec:prenex-polymorphism}}$restriction

Extensions and restrictions go from calculi with shorter names to those with
longer names
(e.g. $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ extends $\lambda$ and
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta 1}$ restricts
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}$).

Figure 1. Overview of translations and non-existence results covered in the
paper.

The main contributions of the paper (summarised in Figure 1) are as follows.

  * •

We present a collection of examples in order to convey the intuition behind
all translations and non-existence results in Figure 1 (Section 2).

  * •

We define a family of Church-style calculi extending $\lambda$-calculus with
variants and records, simple subtyping, and (higher-rank) row or presence
polymorphism (Section 3).

  * •

We prove that simple subtyping can be elaborated away for variants and records
by way of local term-involved translations (Sections 4.1 and 4.3).

  * •

We prove that simple subtyping can be expressed as row polymorphism for
variants and presence polymorphism for records by way of local type-only
translations (Sections 4.2 and 4.4).

  * •

We prove that there exists no type-only translation of simple subtyping into
presence polymorphism for variants or row polymorphism for records (Section
4.5).

  * •

We expand our study to calculi with covariant and full subtyping and with both
row- and presence-polymorphism, covering further translations and non-
existence proofs (Section 5). In so doing we reveal a fundamental asymmetry
between variants and records.

  * •

We prove that if we suitably restrict types and switch to ML-style target
calculi with implicit rank-1 polymorphism, then we can exploit type inference
to encode full subtyping for records and variants using either row
polymorphism or presence polymorphism (Section 6).

  * •

For each translation we prove type preservation and operational correspondence
results.

Sections 7.1 and 7.2 discuss extensions. Section 7.3 discusses related work.
Section 7.4 concludes.

##  2\. Examples

To illustrate the relative expressive power of subtyping and polymorphism for
variants and records with a range of extensions, we give a collection of
examples. These cover the intuition behind the translations and non-existence
results summarised in Figure 1 and formalised later in the paper.

###  2.1. Simple Variant Subtyping as Row Polymorphism

We begin with variant types. Consider the following function.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getAge}=\lambda
x^{[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]}.~{}\mathbf{case}\
x\ \\{\mathsf{Age}\ y\mapsto y;\mathsf{Year}\ y\mapsto 2023-y\\}\\\
\end{array}~{}\end{array}$

The variant type $[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]$
denotes the type of variants with two constructors $\mathsf{Age}$ and
$\mathsf{Year}$ each containing an $\mathsf{Int}$. We cannot directly apply
$\mathtt{getAge}$ to the following variant

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{year}=(\mathsf{Year}\
1984)^{[\mathsf{Year}:\mathsf{Int}]}\\\ \end{array}~{}\end{array}$

as $\mathtt{year}$ and $x$ have different types. With simple variant subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$) which considers
subtyping shallowly on variants, we can upcast
$\mathtt{year}:[\mathsf{Year}:\mathsf{Int}]$ to the supertype
$[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]$ which has more
labels. This makes intuitive sense, as it is always safe to treat a variant
with fewer constructors ($\mathsf{Year}$ in this case) as one with more
constructors ($\mathsf{Age}$ and $\mathsf{Year}$ in this case).

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getAge}\
(\mathtt{year}\vartriangleright[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}])\\\
\end{array}~{}\end{array}$

One advantage of subtyping is reusability: by upcasting we can apply the same
$\mathtt{getAge}$ function to any value whose type is a subtype of
$[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{age}=(\mathsf{Age}\
9)^{[\mathsf{Age}:\mathsf{Int}]}\\\ &\mathtt{getAge}\
(\mathtt{age}\vartriangleright[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}])\\\
\end{array}~{}\end{array}$

In a language without subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$), we can simulate applying
$\mathtt{getAge}$ to $\mathtt{year}$ by first deconstructing the variant using
$\mathbf{case}$ and then reconstructing it at the appropriate type — a kind of
generalised $\eta$-expansion on variants.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getAge}\
(\mathbf{case}\ \mathtt{year}\ \\{\mathsf{Year}\ y\mapsto(\mathsf{Year}\
y)^{[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]}\\})\end{array}~{}\end{array}$

This is the essence of the translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}}$
in Section 4.1. The translation is _local_ in the sense that it only requires
us to transform the parts of the program that relate to variants (as opposed
to the entire program). However, it still comes at a cost. The deconstruction
and reconstruction of variants adds extra computation that was not present in
the original program.

Can we achieve the same expressive power of subtyping without non-trivial term
de- and re-construction? Yes we can! Row polymorphism
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$) allows us to rewrite
$\mathtt{year}$ with a type compatible (via row-variable substitution) with
any variant type containing $\mathsf{Year}:\mathsf{Int}$ and additional cases.
111We omit the kinds of row variables for simplicity. They can be easily
reconstructed from the contexts.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{year^{\prime}}=\Lambda\rho.~{}(\mathsf{Year}\
1984)^{[\mathsf{Year}:\mathsf{Int};\rho]}\\\ \end{array}~{}\end{array}$

As before, the translation to $\mathtt{year^{\prime}}$ also adds new term
syntax. However, the only additional syntax required by this translation
involves type abstraction and type application; in other words the program is
unchanged up to type erasure. Thus we categorise it as a _type-only_
translation as opposed to the previous one which we say is _term-involved_. We
can instantiate $\rho$ with $(\mathsf{Age}:\mathsf{Int})$ when applying
$\mathtt{getAge}$ to it. The parameter type of $\mathtt{getAge}$ must also be
translated to a row-polymorphic type, which requires higher-rank polymorphism.
Moreover, we re-abstract over $\mathtt{year^{\prime}}$ after instantiation to
make it polymorphic again.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getAge^{\prime}}=\lambda
x^{\forall\rho.[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int};\rho]}.~{}\mathbf{case}\
(x\ \cdot)\ \\{\mathsf{Age}\ y\mapsto y;\mathsf{Year}\ y\mapsto 2023-y\\}\\\
&\mathtt{getAge^{\prime}}\ (\Lambda\rho.~{}\mathtt{year^{\prime}}\
(\mathsf{Age}:\mathsf{Int};\rho))\end{array}~{}\end{array}$

The type application $x\ \cdot$ instantiates $\rho$ with the empty closed row
type $\cdot$. The above function application is well-typed because we ignore
the order of labels when comparing rows
($\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int};\rho\equiv\mathsf{Year}:\mathsf{Int};\mathsf{Age}:\mathsf{Int};\rho$)
as usual. This is the essence of the local type-only translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}}$
in Section 4.2.

We are relying on higher-rank polymorphism here in order to simulate upcasting
on demand. For instance, an upcast on the parameter of a function of type
$(\forall\rho.[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int};\rho])\to
B$ is simulated by instantiating $\rho$ appropriately. We will show in Section
2.4 that restricting the target language to rank-1 polymorphism requires
certain constraints on the source language.

###  2.2. Simple Record Subtyping as Presence Polymorphism

Now, we consider record types, through the following function.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}=\lambda
x^{\langle\mathsf{Name}:\mathsf{String}\rangle}.~{}(x.\mathsf{Name})\end{array}~{}\end{array}$

The record type $\langle\mathsf{Name}:\mathsf{String}\rangle$ denotes the type
of records with a single field $\mathsf{Name}$ containing a string. We cannot
directly apply $\mathtt{getName}$ to the following record

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{alice}=\langle\mathsf{Name}=\text{\textquotedbl
Alice\textquotedbl};\mathsf{Age}=9\rangle\end{array}~{}\end{array}$

as the types of $\mathtt{alice}$ and $x$ do not match. With simple record
subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$), we can
upcast
$\mathtt{alice}:\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle$
to the supertype $\langle\mathsf{Name}:\mathsf{String}\rangle$. It is
intuitive to treat a record with more fields ($\mathsf{Name}$ and
$\mathsf{Age}$) as a record with fewer fields (only $\mathsf{Name}$ in this
case).

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}\
(\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle)\end{array}~{}\end{array}$

Similarly to variant subtyping, we can reuse $\mathtt{getName}$ on records of
different subtypes.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{bob}=\langle\mathsf{Name}=\text{\textquotedbl
Bob\textquotedbl};\mathsf{Year}=1984\rangle\\\ &\mathtt{getName}\
(\mathtt{bob}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle)\end{array}~{}\end{array}$

In a language without subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$), we can first
deconstruct the record by projection and then reconstruct it with only the
required fields, similarly to the generalised $\eta$-expansion of records.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}\
\langle\mathsf{Name}=\mathtt{alice}.\mathsf{Name}\rangle\end{array}~{}\end{array}$

This is the essence of the local term-involved translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}}$
in Section 4.3. Using presence polymorphism
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$), we can
simulate $\mathtt{alice}$ using a type-only translation.

$\begin{array}[]{@{}r@{~}c<EMAIL_ADDRESS>Alice\textquotedbl};\mathsf{Age}=9\rangle^{\langle\mathsf{Name}^{\theta_{1}}:\mathsf{String};\mathsf{Age}^{\theta_{2}}:\mathsf{Int}\rangle}\\\
\end{array}~{}\end{array}$

The presence variables $\theta_{1}$ and $\theta_{2}$ can be substituted with a
marker indicating that the label is either present $\bullet$ or absent
$\circ$. We can instantiate $\theta_{2}$ with absent $\circ$ when applying
$\mathtt{getName}$ to it, ignoring the $\mathsf{Age}$ label. This resolves the
type mismatch as the equivalence relation on row types considers only present
labels
($\mathsf{Name}^{\theta}:\mathsf{String}~{}\equiv~{}\mathsf{Name}^{\theta}:\mathsf{String};\mathsf{Age}^{\circ}:\mathsf{Int}$).
For a general translation, we must make the parameter type of
$\mathtt{getName}$ presence-polymorphic, and re-abstract over
$\mathtt{alice^{\prime}}$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName^{\prime}}=\lambda
x^{\forall\theta.\langle\mathsf{Name}^{\theta}:\mathsf{String}\rangle}.~{}((x\
\bullet).\mathsf{Name})\\\ &\mathtt{getName^{\prime}}\
(\Lambda\theta.~{}\mathtt{alice^{\prime}}\ \theta\
\circ)\end{array}~{}\end{array}$

This is the essence of the local type-only translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}}$
in Section 4.4. The duality between variants and records is reflected by the
need for dual kinds of polymorphism, namely row and presence polymorphism,
which can extend or shrink rows, respectively.

###  2.3. Exploiting Contravariance

We have now seen how to encode simple variant subtyping as row polymorphism
and simple record subtyping as presence polymorphism. These encodings embody
the intuition that row polymorphism supports extending rows and presence
polymorphism supports shrinking rows. However, presence polymorphism is
typically treated as an optional extra for row typing. For instance, Rémy
(1994) uses row polymorphism for both record and variant types, and introduces
presence polymorphism only to support record extension and default cases
(which fall outside the scope of our current investigation).

This naturally raises the question of whether we can encode simple record
subtyping using row polymorphism alone. More generally, given the duality
between records and variants, can we swap the forms of polymorphism used by
the above translations?

Though row polymorphism enables extending rows and what upcasting does on
record types is to remove labels, we can simulate the same behaviour by
extending record types that appear in contravariant positions in a type. The
duality between row and presence polymorphism can be reconciled by way of the
duality between covariant and contravariant positions.

Let us revisit our $\mathtt{getName}\ \mathtt{alice}$ example, which we
previously encoded using polymorphism. With row polymorphism
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}$), we can give
the function a row polymorphic type where the row variable appears in the
record type of the function parameter.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}_{\text{\char
55}}=\Lambda\rho.\lambda
x^{\langle\mathsf{Name}:\mathsf{String};\rho\rangle}.~{}(x.\mathsf{Name})\\\
\end{array}~{}\end{array}$

Now in order to apply $\mathtt{getName}_{\text{\char 55}}$ to
$\mathtt{alice}$, we simply instantiate $\rho$ with
$(\mathsf{Age}:\mathsf{Int})$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}_{\text{\char
55}}\ (\mathsf{Age}:\mathsf{Int})\ \mathtt{alice}\end{array}~{}\end{array}$

Though the above example suggests a translation which only introduces type
abstractions and type applications, the idea does not extend to a general
composable translation. Intuitively, the main problem is that in general we
cannot know which type should be used for instantiation
($\mathsf{Age}:\mathsf{Int}$ in this case) in a compositional type-only
translation, which is only allowed to use the type of $\mathtt{getName}$ and
$\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle$.
These tell us nothing about $\mathsf{Age}:\mathsf{Int}$.

In fact, a much stronger result holds. In Section 4.5, we prove that there
exists no type-only encoding of simple record subtyping into row polymorphism
(
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}}$
), and dually for variant types with presence polymorphism (
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}}$
).

###  2.4. Full Subtyping as Rank-1 Polymorphism

The kind of translation sought in Section 2.3 cannot be type-only, as it would
require us to know the type used for instantiation. A natural question is
whether type inference can provide the type.

In order to support decidable, sound, and complete type inference, we consider
a target calculus with rank-1 polymorphism
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$) and
Hindley-Milner type inference. Now the $\mathtt{getName}\ \mathtt{alice}$
example type checks without an explicit upcast or type application.
222Actually, the principal type of $\mathtt{getName}$ should be
$\forall\alpha\,\rho.\langle\mathsf{Name}:\alpha;\rho\rangle\to\alpha$. We
ignore value type variables for simplicity.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}=\lambda
x.~{}(x.\mathsf{Name})&:\forall\rho.\langle\mathsf{Name}:\mathsf{String};\rho\rangle\to\mathsf{String}\\\
&\mathtt{alice}\phantom{xx}=\langle\mathsf{Name}=\text{\textquotedbl
Alice\textquotedbl};\mathsf{Age}=9\rangle&:\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\\\
&\mathtt{getName}\ \mathtt{alice}&:\mathsf{String}\end{array}~{}\end{array}$

Type inference automatically infers a polymorphic type for $\mathtt{getName}$,
and instantiates the variable $\rho$ with $\mathsf{Age}:\mathsf{Int}$. This
observation hints to us that we might encode terms with explicit record
upcasts in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$
by simply erasing all upcasts (and type annotations, given that we have type
inference). The global nature of erasure implies that it also works for full
subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$)
which lifts the width subtyping of rows to any type by propagating the
subtyping relation to the components of type constructors. For instance, the
following function upcast using full subtyping is also translated into
$\mathtt{getName}\ \mathtt{alice}$, simply by erasing the upcast.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&(\mathtt{getName}\vartriangleright(\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\to\mathsf{String}))\
\mathtt{alice}\\\ \end{array}~{}\end{array}$

Thus far, the erasure translation appears to work well even for full
subtyping. Does it have any limitations? Yes, we must restrict the target
language to rank-1 polymorphism, which can only generalise let-bound terms.
The type check would fail if we were to bind $\mathtt{getName}$ via
$\lambda$-abstraction and then use it at different record types. For instance,
consider the following function which concatenates two names using the
$+\\!\\!+$ operator and is applied to $\mathtt{getName}$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&(\lambda
f^{\langle\mathsf{Name}:\mathsf{String}\rangle\to\mathsf{String}}.~{}f\
(\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle)+\\!\\!+\
f\
(\mathtt{bob}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle))\
\mathtt{getName}\end{array}~{}\end{array}$

The erasure of it is

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&(\lambda f.~{}f\
\mathtt{alice}+\\!\\!+\ f\ \mathtt{bob})\
\mathtt{getName}\end{array}~{}\end{array}$

which is not well-typed as $f$ can only have a monomorphic function type,
whose parameter type cannot unify with both
$\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle$ and
$\langle\mathsf{Name}:\mathsf{String};\mathsf{Year}:\mathsf{Int}\rangle$.

In order to avoid such problems, we will define an erasure translation on a
restricted subcalculus of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$.
The key idea is to give row-polymorphic types for record manipulation
functions such as $\mathtt{getName}$. However, the above function takes a
record manipulation function of type
$\langle\mathsf{Name}:\mathsf{String}\rangle\to\mathsf{String}$ as a
parameter, which cannot be polymorphic as we only have rank-1 polymorphism.
Inspired by the notion of rank-$n$ polymorphism, we say that a type has _rank-
$n$ records_, if no path from the root of the type (seen as an abstract syntax
tree) to a record type passes to the left of $n$ or more arrows. We define the
translation only on the subcalculus
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
in which all types have rank-2 records.

Such an erasure translation underlies the local type-only translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho
1}}$ .

We obtain a similar result for presence polymorphism. With presence
polymorphism, we can make all records presence-polymorphic (similar to the
translation in Section 2.2), instead of making all record manipulation
functions row-polymorphic. For instance, we can infer the following types for
the $\mathtt{getName}\ \mathtt{alice}$ example.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName}=\lambda
x.~{}(x.\mathsf{Name})&:\langle\mathsf{Name}:\mathsf{String}\rangle\to\mathsf{String}\\\
&\mathtt{alice}\phantom{xx}=\langle\mathsf{Name}=\text{\textquotedbl
Alice\textquotedbl};\mathsf{Age}=9\rangle&:\forall\theta_{1}\theta_{2}.\langle\mathsf{Name}^{\theta_{1}}:\mathsf{String};\mathsf{Age}^{\theta_{2}}:\mathsf{Int}\rangle\\\
&\mathtt{getName}\ \mathtt{alice}&:\mathsf{String}\end{array}~{}\end{array}$

Consequently, records should appear only in positions that can be generalised
with rank-1 polymorphism, which can be ensured by restricting
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
to the subcalculus
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}1}^{\leqslant\mathrm{full}}$
in which all types have rank-1 records. We give a local type-only translation:
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}1}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta
1}}$ .

For variants, we can also define the notion of _rank- $n$ variants_ similarly.
Dually to records, we can either make all variants be row-polymorphic (similar
to the translation in Section 2.1) and require types to have rank-1 variants
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}1}^{\leqslant\mathrm{full}}$), or
make all variant manipulation functions be presence-polymorphic and require
types to have rank-2 variants
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}2}^{\leqslant\mathrm{full}}$). For
instance, we can make the $\mathtt{getAge}$ function presence-polymorphic.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getAge}=\lambda
x.~{}\mathbf{case}\ x\ \\{\mathsf{Age}\ y\mapsto y;\mathsf{Year}\ y\mapsto
2023-y\\}:\forall\theta_{1}\theta_{2}.{[\mathsf{Age}^{\theta_{1}}\\!:\mathsf{Int};\mathsf{Year}^{\theta_{2}}\\!:\mathsf{Int}]}\to\mathsf{Int}\\\
&\mathtt{year}\phantom{xx}=\mathsf{Year}\ 1984:[\mathsf{Age}:\mathsf{Int}]\\\
&\mathtt{getAge}\ \mathtt{year}\end{array}~{}\end{array}$

We give two type-only encodings of full variant subtyping:
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}1}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho
1}}$ and
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}2}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta
1}}$ . Section 6 discusses in detail the four erasure translations from full
subtyping to rank-1 polymorphism with type inference.

###  2.5. Strictly Covariant Record Subtyping as Presence Polymorphism

The encodings of full subtyping discussed in Section 2.4 impose restrictions
on types in the source language and rely heavily on type-inference. We now
consider to what extent we can support a richer form of subtyping than simple
subtyping, if we turn our attention to target calculi with higher-rank
polymorphism and no type inference.

One complication of extending simple subtyping to full subtyping is that if we
permit propagation through contravariant positions, then the subtyping order
is reversed. To avoid this scenario, we first consider _strictly covariant
subtyping_ relation derived by only propagating simple subtyping through
strictly covariant positions (i.e. never to the left of any arrow). For
example, the upcast
$\mathtt{getName}\vartriangleright(\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\to\mathsf{String})$
in Section 2.4 is ruled out. We write
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
for our calculus with strictly covariant record subtyping.

Consider the function $\mathtt{getChildName}$ returning the name of the child
of a person.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getChildName}=\lambda
x^{\langle\mathsf{Child}:\langle\mathsf{Name}:\mathsf{String}\rangle\rangle}.~{}\mathtt{getName}\
(x.\mathsf{Child})\end{array}~{}\end{array}$

We can apply $\mathtt{getChildName}$ to $\mathtt{carol}$ who has a daughter
$\mathtt{alice}$ with the strictly covariant subtyping relation
$\langle\mathsf{Name}:\mathsf{String};\mathsf{Child}:\langle\mathsf{Name}\\!:\\!\mathsf{String};\mathsf{Age}\\!:\\!\mathsf{Int}\rangle\rangle\leqslant\langle\mathsf{Child}:\langle\mathsf{Name}\\!:\\!\mathsf{String}\rangle\rangle$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{carol}=\langle\mathsf{Name}=\text{\textquotedbl
Carol\textquotedbl};\mathsf{Child}=\mathtt{alice}\rangle\\\
&\mathtt{getChildName}\
(\mathtt{carol}\vartriangleright\langle\mathsf{Child}:\langle\mathsf{Name}:\mathsf{String}\rangle\rangle)\end{array}~{}\end{array}$

If we work in a language without subtyping
($\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$), we can still use
$\eta$-expansions instead, by nested deconstruction and reconstruction.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getChildName}\
\langle\mathsf{Child}=\langle\mathsf{Name}=\mathtt{carol}.\mathsf{Child}.\mathsf{Name}\rangle\rangle\end{array}~{}\end{array}$

In general, we can simulate the full subtyping (not only strictly covariant
subtyping) of both records and variants using this technique. The nested de-
and re-construction can be reformulated into coercion functions to be more
compositional (Breazu-Tannen et al., 1991). In Section 5.1, we show the
standard local term-involved translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}}$
formalising this idea.

However, for type-only encodings, the idea of making every record presence-
polymorphic in Section 2.2 does not work directly. Following that idea, we
would translate $\mathtt{carol}$ to

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{carol}_{\text{\char
55}}=\Lambda\theta_{1}^{\prime}\theta_{2}^{\prime}.~{}\langle\dots;\mathsf{Child}=\mathtt{alice^{\prime}}\rangle^{\langle\mathsf{Name}^{\theta_{1}^{\prime}}:\mathsf{String};\mathsf{Child}^{\theta_{2}^{\prime}}:\forall\theta_{1}\theta_{2}.\langle\mathsf{Name}^{\theta_{1}}:\mathsf{String};\mathsf{Age}^{\theta_{2}}:\mathsf{Int}\rangle\rangle}\\\
\end{array}~{}\end{array}$

Then, as $\theta_{1}$ and $\theta_{2}$ are abstracted inside a record, we
cannot directly instantiate $\theta_{2}$ with $\circ$ to remove the
$\mathsf{Age}$ label without deconstructing the outer record. However, we can
tweak the translation by moving the quantifiers $\forall\theta_{1}\theta_{2}$
to the top-level through introducing new type abstraction and type
application, which gives rise to a translation that is type-only but global.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{carol^{\prime}}=\Lambda\theta_{1}\theta_{2}\theta_{3}\theta_{4}.\langle\dots;\mathsf{Child}=\mathtt{alice^{\prime}}\
\theta_{3}\
\theta_{4}\rangle^{\langle\mathsf{Name}^{\theta_{1}}:\mathsf{String};\mathsf{Child}^{\theta_{2}}:\langle\mathsf{Name}^{\theta_{3}}:\mathsf{String};\mathsf{Age}^{\theta_{4}}:\mathsf{Int}\rangle\rangle}\\\
\end{array}~{}\end{array}$

Now we can remove the $\mathsf{Name}$ of $\mathtt{carol^{\prime}}$ and
$\mathsf{Age}$ of $\mathtt{alice^{\prime}}$ by instantiating $\theta_{1}$ and
$\theta_{4}$ with $\circ$. As for simple subtyping, we make the parameter type
of $\mathtt{getChildName}$ polymorphic, and re-abstract over
$\mathtt{carol^{\prime}}$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getChildName^{\prime}}=\lambda
x^{\forall\theta_{1}\theta_{2}.\langle\mathsf{Child}^{\theta_{1}}:\langle\mathsf{Name}^{\theta_{2}}:\mathsf{String}\rangle\rangle}.~{}\mathtt{getName}\
((x\ \bullet\ \bullet).\mathsf{Child})\\\ &\mathtt{getChildName^{\prime}}\
(\Lambda\theta_{1}\theta_{2}.~{}\mathtt{carol^{\prime}}\ \circ\ \theta_{1}\
\theta_{2}\ \circ)\end{array}~{}\end{array}$

This is the essence of the global type-only translation
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}}$
in Section 5.2.

###  2.6. No Type-Only Encoding of Strictly Covariant Variant Subtyping as
Polymorphism

We now consider whether we could exploit hoisting of quantifiers in order to
encode strictly covariant subtyping for variants
($\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{co}}$) using
row polymorphism. Interestingly, we will see that this cannot work, thus
breaking the symmetry between the results for records and variants we have
seen so far. To understand why, consider the following example involving
nested variants.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{data}=(\mathsf{Raw}\
\mathtt{year})^{[\mathsf{Raw}:[\mathsf{Year}:\mathsf{Int}]]}\\\
&\mathtt{data}\vartriangleright{[\mathsf{Raw}:[\mathsf{Year}:\mathsf{Int};\mathsf{Age}:\mathsf{Int}]]}\end{array}~{}\end{array}$

Following the idea of moving quantifiers, we can translate $\mathtt{data}$ to
use a polymorphic variant, and the upcast can then be simulated by
instantiation and re-abstraction.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{data}_{\text{\char
55}}=\Lambda\rho_{1}\rho_{2}.~{}(\mathsf{Raw}\ (\mathtt{year^{\prime}}\
\rho_{2}))^{[\mathsf{Raw}:[\mathsf{Year}:\mathsf{Int};\rho_{2}];\rho_{1}]}\\\
&\Lambda\rho_{1}\rho_{2}.~{}\mathtt{data}_{\text{\char 55}}\ \rho_{1}\
(\mathsf{Age}:\mathsf{Int};\rho_{2})\end{array}~{}\end{array}$

So far, the translation appears to have worked. However, it breaks down when
we consider the case split on a nested variant. For instance, consider the
following function.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{parseAge}=\lambda
x^{[\mathsf{Raw}:[\mathsf{Year}:\mathsf{Int}]]}.~{}\mathbf{case}\ x\
\\{\mathsf{Raw}\ y\mapsto\mathtt{getAge}\
(y\vartriangleright[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}])\\}\\\
&\mathtt{parseAge}\ \mathtt{data}\end{array}~{}\end{array}$

Using an upcast and $\mathtt{getAge}$ from Section 2.1 in the case clause, it
accepts the nested variant $\mathtt{data}$.

The difficulty with encoding $\mathtt{parseAge}$ with row polymorphism is that
the abstraction of the row variable for the inner record of
$\mathtt{data_{\text{\char 55}}}$ is hoisted up to the top-level, but case
split requires a monomorphic value. Thus, we must instantiate $\rho_{2}$ with
$\mathsf{Age}:\mathsf{Int}$ _before_ performing the case split.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{parseAge}_{\text{\char
55}}=\lambda
x^{\forall\rho_{1}\rho_{2}.[\mathsf{Raw}:[\mathsf{Year}:\mathsf{Int};\rho_{2}];\rho_{1}]}.~{}\mathbf{case}\
(x\ \cdot\ (\mathsf{Age}:\mathsf{Int}))\ \\{\mathsf{Raw}\
y\mapsto\mathtt{getAge}\ y\\}\\\ &\mathtt{parseAge}_{\text{\char 55}}\
\mathtt{data}_{\text{\char 55}}\end{array}~{}\end{array}$

However, this would not yield a compositional type-only translation, as the
translation of the $\mathbf{case}$ construct only has access to the types of
$x$ and the whole case clause, which provide no information about
$\mathsf{Age}:\mathsf{Int}$. Moreover, even if the translation could somehow
access this type information, the translation would still fail if there were
multiple incompatible upcasts of $y$ in the case clause.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathbf{case}\ x\
\\{\mathsf{Raw}\ y\mapsto\dots
y\vartriangleright[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]\dots
y\vartriangleright[\mathsf{Age}:\mathsf{String};\mathsf{Year}:\mathsf{Int}]\\}\end{array}~{}\end{array}$

The first upcast requires $\rho_{2}$ to be instantiated with
$\mathsf{Age}:\mathsf{Int}$ but the second requires it to be instantiated with
the incompatible $\mathsf{Age}:\mathsf{String}$. The situation is no better if
we add presence polymorphism. In Section 5.3, we prove that there exists no
type-only encoding of strictly covariant variant subtyping into row and
presence polymorphism (
${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{co}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho\theta}}$
).

###  2.7. No Type-Only Encoding of Full Record Subtyping as Polymorphism

For variants, we have just seen that a type-only encoding of full subtyping
does not exist, even if we restrict propagation of simple subtyping to
strictly covariant positions. For records, we have seen how to encode strictly
covariant subtyping with presence polymorphism by hoisting quantifiers to the
top-level. We now consider whether we could somehow lift the strictly
covariance restriction and encode full record subtyping with polymorphism.

The idea of hoisting quantifiers does not work arbitrarily, exactly because we
cannot hoist quantifiers through contravariant positions. Moreover, presence
polymorphism alone cannot extend rows. Consider the full subtyping example
$\mathtt{getName}\vartriangleright(\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\to\mathsf{String})$
from Section 2.4. The $\mathtt{getName}$ function is translated to the
$\mathtt{getName^{\prime}}$ function in Section 2.2, which provides no way to
extend the parameter record type with $\mathsf{Age}:\mathsf{Int}$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName^{\prime}}=\lambda
x^{\forall\theta.\langle\mathsf{Name}^{\theta}:\mathsf{String}\rangle}.~{}((x\
\bullet).\mathsf{Name})\\\ \end{array}~{}\end{array}$

A tempting idea is to add row polymorphism:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getName^{\prime}}_{\text{\char
55}}=\Lambda\rho.\lambda
x^{\forall\theta.\langle\mathsf{Name}^{\theta}:\mathsf{String};\rho\rangle}.~{}((x\
\bullet).\mathsf{Name})\\\ \end{array}~{}\end{array}$

Now we can instantiate $\rho$ with $\mathsf{Age}:\mathsf{Int}$ to simulate the
upcast. However, this still does not work. One issue is that we have no way to
remove the labels introduced by the row variable $\rho$ in the function body,
as $x$ is only polymorphic in $\theta$. For instance, consider the following
upcast of the function $\mathtt{getUnit}$ which replaces the function body of
$\mathtt{getName}$ with an upcast of $x$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getUnit}=\lambda
x^{\langle\mathsf{Name}:\mathsf{String}\rangle}.(x\vartriangleright\langle\rangle)\\\
&\mathtt{getUnit}\vartriangleright(\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\to\langle\rangle)\end{array}~{}\end{array}$

Following the above idea, $\mathtt{getUnit}$ is translated to

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getUnit}_{\text{\char
55}}=\Lambda\rho.\lambda
x^{\forall\theta.\langle\mathsf{Name}^{\theta}:\mathsf{String};\rho\rangle}.x\
\circ\\\ \end{array}~{}\end{array}$

Then, in the translation of the upcast of $\mathtt{getUnit}$, the row variable
$\rho$ is expected to be instantiated with a row containing
$\mathsf{Age}:\mathsf{Int}$. However, we cannot remove
$\mathsf{Age}:\mathsf{Int}$ again in the translation of the function body,
meaning that the upcast inside $\mathtt{getUnit}$ cannot yield an empty
record.

Section 5.4 expands on the discussion here and proves that there exists no
type-only translation of unrestricted full record subtyping into row and
presence polymorphism (
${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}}$${\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho\theta}}$
).

##  3\. Calculi

The foundation for our exploration of relative expressive power of subtyping
and parametric polymorphism is Church’s simply-typed $\lambda$-calculus
(Church, 1940). We extend it with variants and records, respectively. We
further extend the variant calculus twice: first with simple structural
subtyping and then with row polymorphism. Similarly, we also extend the record
calculus twice: first with structural subtyping and then with presence
polymorphism. In Section 5 and 6, we explore further extensions with strictly
covariant subtyping, full subtyping and rank-1 polymorphism.

###  3.1. A Simply-Typed Base Calculus $\lambda$

Our base calculus is a Church-style simply typed $\lambda$-calculus, which we
denote $\lambda$. Figure LABEL:fig:stlc-var-rec shows the syntax, static
semantics, and dynamic semantics of it. The calculus features one kind
($\mathsf{Type}$) to classify well-formed types. We will enrich the structure
of kinds in the subsequent sections when we add rows (e.g. Sections 3.2 and
3.5). The syntactic category of types includes abstract base types ($\alpha$)
and the function types ($A\to B$), which classify functions with domain $A$
and codomain $B$. The terms consist of variables ($x$), $\lambda$-abstraction
($\lambda x^{A}.M$) binding variable $x$ of type $A$ in term $M$, and
application ($M\,N$) of $M$ to $N$. We track base types in a type environment
($\Delta$) and the type of variables in a term environment ($\Gamma$). We
treat environments as unordered mappings. The static and dynamic semantics are
standard. We implicitly require type annotations in terms to be well-kinded,
e.g., $\Delta;\Gamma\vdash\lambda x^{A}.M:A\to B$ requires $\Delta\vdash A$.

###  3.2. A Calculus with Variants
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$

$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ is the extension of $\lambda$
with variants. LABEL:fig:stlc-var-rec incorporates the extensions to the
syntax, static semantics, and dynamic semantics. _Rows_ are the basis for
variants (and later records). We assume a countably infinite set of labels
$\mathcal{L}_{\omega}$. Given a finite set of labels $\mathcal{L}$, a row of
kind $\mathsf{Row}_{\mathcal{L}}$ denotes a partial mapping from the cofinite
set $(\mathcal{L}_{\omega}\mathbin{\backslash}{\mathcal{L}})$ of all labels
except those in $\mathcal{L}$ to types. We say that a row of kind
$\mathsf{Row}_{\emptyset}$ is _complete_. A variant type ($[R]$) is given by a
complete row $R$. A row is written as a sequence of pairs of labels and types.
We often omit the leading $\cdot$, writing e.g.
$\ell_{1}:A_{1},\dots,\ell_{n}:A_{n}$ or $(\ell_{i}:A_{i})_{i}$ when $n$ is
clear from context. We identify rows up to reordering of labels. Injection
$(\ell\,M)^{A}$ introduces a term of variant type by tagging the payload $M$
with $\ell$, whose resulting type is $A$. A case split
($\mathbf{case}~{}M~{}\\{\ell_{i}~{}x_{i}\mapsto N_{i}\\}_{i}$) eliminates an
$M$ by matching against the tags $\ell_{i}$. A successful match on $\ell_{i}$
binds the payload of $M$ to $x_{i}$ in $N_{i}$. The kinding rules ensure that
rows contain no duplicate labels. The typing rules for injections and case
splits and the $\beta$-rule for variants are standard.

###  3.3. A Calculus with Variants and Structural Subtyping
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$

$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ is the extension of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ with simple structural subtyping.
Figure LABEL:fig:stlc-var-rec-sub shows the extensions to syntax, static
semantics, and dynamic semantics.

#### Syntax

The explicit upcast operator ($M\vartriangleright A$) coerces $M$ to type $A$.

#### Static Semantics

The $\mathsf{S\textrm{-}Variant}$ rule asserts that variant $[R]$ is a subtype
of variant $[R^{\prime}]$ if row $R^{\prime}$ contains at least the same
label-type pairs as row $R$. We write $\mathsf{dom}(R)$ for the domain of row
$R$ (i.e. its labels), and $R|_{\mathcal{L}}$ for the restriction of $R$ to
the label set $\mathcal{L}$. The $\mathsf{T\textrm{-}Upcast}$ rule enables the
upcast $M\vartriangleright B$ if the term $M$ has type $A$ and $A$ is a
subtype of $B$.

#### Dynamic Semantics

The $\mathsf{\vartriangleright\\!\\!\textrm{-}Variant}$ reduction rule coerces
an injection $(\ell\,M)$ of type $A$ to a larger (variant) type $B$. We
distinguish upcast rules from $\beta$ rules writing instead
$\leadsto_{\vartriangleright}$ for the reduction relation. Correspondingly, we
write $\rightsquigarrow_{\vartriangleright}$ for the compatible closure of
$\leadsto_{\vartriangleright}$.

###  3.4. A Calculus with Row Polymorphic Variants
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$

$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$ is the extension of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ with row polymorphism. Figure
LABEL:fig:var-calc-row shows the extensions to the syntax, static semantics,
and dynamic semantics.

#### Syntax

The syntax of types is extended with a quantified type ($\forall\rho^{K}.A$)
which binds the row variable $\rho$ with kind $K$ in the type $A$ (the kinding
rules restrict $K$ to always be of kind $\mathsf{Row}_{\mathcal{L}}$ for some
$\mathcal{L}$). The syntax of rows is updated to allow a row to end in a row
variable ($\rho$). A row variable enables the tail of a row to be extended
with further labels. A row with a row variable is said to be _open_ ; a row
without a row variables is said to be closed.

Terms are extended with type (row) abstraction ($\Lambda\rho^{K}.M$) binding
the row variable $\rho$ with kind $K$ in $M$ and row application ($M\,R$) of
$M$ to $R$. Finally, type environments are updated to track the kinds of row
variables.

#### Static Semantics

The kinding and typing rules for row polymorphism are the standard rules for
System F specialised to rows.

#### Dynamic Semantics

The new rule $\mathsf{\tau\textrm{-}RowLam}$ is the standard $\beta$ rule for
System F, but specialised to rows. Though it is a $\beta$ rule, we use the
notation $\leadsto_{\tau}$ to distinguish it from other $\beta$ rules as it
only influences types. This distinction helps us to make the meta theory of
translations in Section 4 clearer. We write $\rightsquigarrow_{\tau}$ for the
compatible closure of $\leadsto_{\tau}$.

###  3.5. A Calculus with Records
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$

$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$ is $\lambda$ extended
with records. LABEL:fig:stlc-var-rec incorporates the extensions to the
syntax, static semantics, and dynamic semantics. As with
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$, we use rows as the basis of
record types. The extensions of kinds, rows and labels are the same as
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$. As with variants a record type
($\langle R\rangle$) is given by a complete row $R$. Records introduction
$\langle\ell_{i}=M_{i}\rangle_{i}$ gives a record in which field $i$ has label
$\ell_{i}$ and payload $M_{i}$. Record projection ($M.\ell$) yields the
payload of the field with label $\ell$ from the record $M$. The static and
dynamic semantics for records are standard.

###  3.6. A Calculus with Records and Structural Subtyping
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$

$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ is the
extension of $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$ with
structural subtyping. Figure LABEL:fig:stlc-var-rec-sub shows the extensions
to syntax, static semantics, and dynamic semantics. The only difference from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ is the subtyping rule
$\mathsf{S\textrm{-}Record}$ and dynamic semantics rule
$\mathsf{\vartriangleright\\!\\!\textrm{-}Record}$. The subtyping relation
($\leqslant$) is just like that for
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ except $R$ and
$R^{\prime}$ are swapped. The $\mathsf{S\textrm{-}Record}$ rule states that a
record type $\langle R\rangle$ is a subtype of $\langle R^{\prime}\rangle$ if
the row $R$ contains at least the same label-type pairs as $R^{\prime}$. The
$\mathsf{\vartriangleright\\!\\!\textrm{-}Record}$ rule upcasts a record
$\langle\ell_{i}=M_{i}\rangle_{i}$ to type $\langle R\rangle$ by directly
constructing a record with only the fields required by the supertype $\langle
R\rangle$. We implicitly assume that the two indexes $j$ range over the same
set of integers.

###  3.7. A Calculus with Presence Polymorphic Records
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$

$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ is the
extension of $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$ with
presence-polymorphic records. Figure LABEL:fig:rec-calc-pre shows the
extensions to the syntax, static semantics, and dynamic semantics.

#### Syntax

The syntax of kinds is extended with the kind of presence types
($\mathsf{Pre}$). The structure of rows is updated with presence annotations
on labels $(\ell_{i}^{P_{i}}:A_{i})_{i}$. Following Rémy (1994), a label can
be marked as either absent ($\circ$), present ($\bullet$), or polymorphic in
its presence ($\theta$). In each case, the label is associated with a type.
Thus, it is perfectly possible to say that some label $\ell$ is absent with
some type $A$. As for row variables, the syntax of types is extended with a
quantified type ($\forall\theta.A$), and the syntax of terms is extended with
presence abstraction ($\Lambda\theta.M$) and application ($M~{}P$). To have a
deterministic static semantics, we need to extend record constructions with
type annotations to indicate the presence types of labels
($\langle\ell_{i}=M_{i}\rangle^{A}$). Finally, the structure of type
environments is updated to track presence variables. With presence types, we
not only ignore the order of labels, but also ignore absent labels when
comparing row types. Similarly when comparing two typed records in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$. For
instance, the row
$\langle\ell_{1}=M;\ell_{2}=N\rangle^{\langle\ell_{1}^{\bullet}:A;\ell_{2}^{\circ}:B\rangle}$
is equivalent to
$\langle\ell_{1}=M\rangle^{\langle\ell_{1}^{\bullet}:A\rangle}$.

#### Static Semantics

The kinding and typing rules for polymorphism ($\mathsf{K\textrm{-}PreAll}$,
$\mathsf{T\textrm{-}PreLam}$, $\mathsf{T\textrm{-}PreApp}$) are the standard
ones for System F specialised to presence types. The first three new kinding
rules $\mathsf{K\textrm{-}Absent}$, $\mathsf{K\textrm{-}Present}$, and
$\mathsf{K\textrm{-}PreVar}$ handle presence types directly. They assign kind
$\mathsf{Pre}$ to absent, present, and polymorphic presence annotation
respectively. The kinding rule $\mathsf{K\textrm{-}ExtendRow}$ is extended
with a new kinding judgement to check $P$ is a presence type. The typing rules
for records, $\mathsf{T\textrm{-}Record}$, and projections,
$\mathsf{T\textrm{-}Project}$, are updated to accommodate the presence
annotations on labels. The typing rule for record introduction,
$\mathsf{T\textrm{-}Record}$, is changed such that the type of each component
coincides with the annotation. The projection rule,
$\mathsf{T\textrm{-}Project}$, is changed such that the $\ell$ component must
be present in the record row.

#### Dynamic Semantics

The new rewrite rule $\mathsf{\tau\textrm{-}PreLam}$ is the standard $\beta$
rule for System F, but specialised to presence types. As with
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$ we use the notation
$\leadsto_{\tau}$ to distinguish it from other $\beta$ rules and write
$\rightsquigarrow_{\tau}$ for its compatible closure. The
$\mathsf{\beta\textrm{-}Project^{\star}}$ rule is the same as
$\mathsf{\beta\textrm{-}Project}$, but with a type annotation on the record.

##  4\. Simple Subtyping as Polymorphism

In this section, we consider encodings of simple subtyping. We present four
encodings and two non-existence results as depicted in Figure 1. Specifically,
in addition to the standard term-involved encodings of simple variant and
record subtyping in Section 4.1 and Section 4.3, we give type-only encodings
of simple variant subtyping as row polymorphism in Section 4.2, and simple
record subtyping as presence polymorphism in Section 4.4. For each
translation, we establish its correctness by demonstrating the preservation of
typing derivations and the correspondence between the operational semantics.
In Section 4.5, we show the non-existence of type-only encodings if we swap
the row and presence polymorphism of the target languages.

#### Compositional Translations

We restrict our attention to compositional translations defined inductively
over the structure of derivations. For convenience we will often write these
as if they are defined on plain terms, but formally the domain is derivations
rather than terms, whilst the codomain is terms. In this section translations
on derivations will always be defined on top of corresponding compositional
translations on types, kind environments, and type environments, in such a way
that we obtain a type preservation property for each translation. In Sections
5 and 6 we will allow non-compositional translations on types (as they will
necessarily need to be constructed in a non-compositional global fashion,
e.g., by way of a type inference algorithm).

###  4.1. Local Term-Involved Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$

We give a local term-involved compositional translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$, formalising the idea of
simulating
$\mathtt{age}\vartriangleright[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int}]$
with case split and injection in Section 2.1.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket
M^{[\ell_{i}:A_{i}]_{i}}\vartriangleright[R]\rrbracket~{}&=\hfil~{}&\mathbf{case}~{}\llbracket
M\rrbracket~{}\\{\ell_{i}~{}x_{i}\mapsto(\ell_{i}~{}x_{i})^{[R]}\\}_{i}\end{array}$

The translation has a similar structure to the $\eta$-expansion of variants:

$\begin{array}[]{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}\mathsf{\eta\textrm{-}Case}&M^{[\ell_{i}:A_{i}]_{i}}~{}~{}&\leadsto_{\eta}\hfil~{}~{}&\mathbf{case}~{}M~{}\\{\ell_{i}~{}x_{i}\mapsto(\ell_{i}\,x_{i})^{[\ell_{i}:A_{i}]_{i}}\\}_{i}\end{array}$

The following theorem states that the translation preserves typing
derivations. Note that compositional translations always translate
environments pointwise. For type environments, we have
$\llbracket\Gamma,x:A\rrbracket=\llbracket\Gamma\rrbracket,x:\llbracket
A\rrbracket$. For kind environments, we have the identity function
$\llbracket\Delta\rrbracket=\Delta$.

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

Every well-typed $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ term
$\Delta;\Gamma\vdash M:A$ is translated to a well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ term
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket A\rrbracket$.

In order to state an operational correspondence result, we first define
$\leadsto_{\beta\vartriangleright}$ as the union of $\leadsto_{\beta}$ and
$\leadsto_{\vartriangleright}$, and
$\rightsquigarrow_{\beta\vartriangleright}$ as its compatible closure. There
is a one-to-one correspondence between reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ and reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$.

###### Theorem 4.2 (Operational Correspondence).

For the translation $\llbracket-\rrbracket$ from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$, we have

  * _Simulation_

If $M\rightsquigarrow_{\beta\vartriangleright}N$, then $\llbracket
M\rrbracket\rightsquigarrow_{\beta}\llbracket N\rrbracket$.

  * _Reflection_

If $\llbracket M\rrbracket\rightsquigarrow_{\beta}\llbracket N\rrbracket$,
then $M\rightsquigarrow_{\beta\vartriangleright}N$.

Intuitively, every step of $\beta$-reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ is mapped to itself
in $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$. For every step of upcast
reduction of $M^{[R^{\prime}]}\vartriangleright[R]$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$, the
$\mathsf{\vartriangleright\\!\\!\textrm{-}Variant}$ rule guarantees that $M$
must be a variant value. Thus, it is mapped to one step of $\beta$-reduction
which reduces the $\eta$-expansion of $M$. The full proofs of type
preservation and operational correspondence can be found in Section B.1.

###  4.2. Local Type-Only Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$

We give a local type-only translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$ by making variants row-
polymorphic, as demonstrated by $\mathtt{year^{\prime}}$ and
$\mathtt{getAge^{\prime}}$ in Section 2.1.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Type}\to\mathsf{Type}\\\
\llbracket[R]\rrbracket~{}&=\hfil~{}&\forall\rho^{\mathsf{Row}_{R}}.[\llbracket
R\rrbracket;\rho]\\\
\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Row}\to\mathsf{Row}\\\
\llbracket(\ell_{i}:A_{i})_{i}\rrbracket~{}&=\hfil~{}&(\ell_{i}:\llbracket
A_{i}\rrbracket)_{i}\\\ \end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket(\ell\,M)^{[R]}\rrbracket~{}&=\hfil~{}&\Lambda\rho^{\mathsf{Row}_{R}}.(\ell\,\llbracket
M\rrbracket)^{[\llbracket R\rrbracket;\rho]}\\\
\llbracket\mathbf{case}~{}M~{}\\{\ell_{i}~{}x_{i}\mapsto
N_{i}\\}_{i}\rrbracket~{}&=\hfil~{}&\mathbf{case}~{}(\llbracket
M\rrbracket\,{\cdot})~{}\\{\ell_{i}~{}x_{i}\mapsto\llbracket
N_{i}\rrbracket\\}_{i}\\\ \llbracket
M^{[R]}\vartriangleright[R^{\prime}]\rrbracket~{}&=\hfil~{}&\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.\llbracket
M\rrbracket\,@\,(\llbracket R^{\prime}\backslash R\rrbracket;\rho)\\\
\end{array}$

The $\mathsf{Row}_{R}$ is short for $\mathsf{Row}_{\mathsf{dom}(R)}$ and
$R\backslash R^{\prime}$ is defined as row difference:

$\displaystyle R\backslash R^{\prime}$ $\displaystyle=(\ell:A)_{(\ell:A)\in
R\text{ and }(\ell:A)\notin R^{\prime}}$

The translation preserves typing derivations.

###### Theorem 4.3 (Type Preservation).

Every well-typed $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ term
$\Delta;\Gamma\vdash M:A$ is translated to a well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$ term
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket A\rrbracket$.

In order to state an operational correspondence result, we introduce two
auxiliary reduction relations. First, we annotate the type application
introduced by the translation of upcasts with the symbol @ to distinguish it
from the type application introduced by the translation of $\mathbf{case}$. We
write $\leadsto_{\nu}$ for the associated reduction and
$\rightsquigarrow_{\nu}$ for its compatible closure.

$\begin{array}[]{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}\mathsf{\nu\textrm{-}RowLam}&(\Lambda\rho^{K}.M)\,@\,A~{}~{}&\leadsto_{\nu}\hfil~{}~{}&M[A/\rho]\end{array}$

Then, we add another intuitive reduction rule for upcast in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$, which allows nested
upcasts to reduce to a single upcast.

$\begin{array}[]{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}\mathsf{\blacktriangleright\\!\\!\textrm{-}Nested}&M\vartriangleright
A\vartriangleright
B~{}~{}&\leadsto_{\blacktriangleright}\hfil~{}~{}&M\vartriangleright
B\end{array}$

We write $\leadsto_{\vartriangleright\blacktriangleright}$ for the union of
$\leadsto_{\vartriangleright}$ and $\leadsto_{\blacktriangleright}$, and
$\rightsquigarrow_{\vartriangleright\blacktriangleright}$ for its compatible
closure. There are one-to-one correspondences between $\beta$-reductions
(modulo $\rightsquigarrow_{\tau}$), and between upcast and
$\rightsquigarrow_{\nu}$.

###### Theorem 4.4 (Operational Correspondence).

For the translation $\llbracket-\rrbracket$ from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$, we have

  * _Simulation_

If $M\rightsquigarrow_{\beta}N$, then $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{?}\rightsquigarrow_{\beta}\llbracket
N\rrbracket$; if $M\rightsquigarrow_{\vartriangleright}N$, then $\llbracket
M\rrbracket\rightsquigarrow_{\nu}\llbracket N\rrbracket$.

  * _Reflection_

If $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{?}\rightsquigarrow_{\beta}\llbracket
N\rrbracket$, then $M\rightsquigarrow_{\beta}N$; if $\llbracket
M\rrbracket\rightsquigarrow_{\nu}\llbracket N\rrbracket$, then
$M\rightsquigarrow_{\vartriangleright\blacktriangleright}N$.

We write $\rightsquigarrow_{\tau}^{?}$ to represent zero or one step of
$\rightsquigarrow_{\tau}$. For the $\beta$-reduction of a case-split in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$, in order to reduce
further in $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$, the
translation of it must first reduce the empty row type application $\llbracket
M\rrbracket\,\cdot$ by $\rightsquigarrow_{\tau}$. One step of upcast reduction
in $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ is simply mapped
to the corresponding type application in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$. The other direction
(reflection) is slightly more involved as one step of $\rightsquigarrow_{\nu}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$ may correspond to a
nested upcast; hence the need for
$\rightsquigarrow_{\vartriangleright\blacktriangleright}$ instead of
$\rightsquigarrow_{\vartriangleright}$. The proofs of type preservation and
operational correspondence can be found in Section B.2.

###  4.3. Local Term-Involved Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$

We give a local term-involved translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$, formalising the idea
of simulating
$\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle$
with projection and record construction in Section 2.1.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket
M\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket~{}&=\hfil~{}&\langle\ell_{i}=\llbracket
M\rrbracket.\ell_{i}\rangle_{i}\end{array}$

The translation has a similar structure to the $\eta$-expanding of records,
which is

$\begin{array}[]{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}\mathsf{\eta\textrm{-}Project}&M^{\langle\ell_{i}:A_{i}\rangle_{i}}~{}~{}&\leadsto_{\eta}\hfil~{}~{}&\langle\ell_{i}=M.\ell_{i}\rangle_{i}\end{array}$

The translation preserves typing derivations.

###### Theorem 4.5 (Type Preservation).

Every well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ term
$\Delta;\Gamma\vdash M:A$ is translated to a well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$ term
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket A\rrbracket$.

One upcast or $\beta$-reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$
corresponds to a sequence of $\beta$-reductions in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$.

###### Theorem 4.6 (Operational Correspondence).

For the translation $\llbracket-\rrbracket$ from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$, we have

  * _Simulation_

If $M\rightsquigarrow_{\beta\vartriangleright}N$, then $\llbracket
M\rrbracket\rightsquigarrow_{\beta}^{\ast}\llbracket N\rrbracket$.

  * _Reflection_

If $\llbracket M\rrbracket\rightsquigarrow_{\beta}N^{\prime}$, then there
exists $N$ such that $N^{\prime}\rightsquigarrow_{\beta}^{\ast}\llbracket
N\rrbracket$ and $M\rightsquigarrow_{\beta\vartriangleright}N$.

We write $\rightsquigarrow_{\beta}^{\ast}$ to represent multiple (including
zero) steps of $\rightsquigarrow_{\beta}$. Unlike Theorem 4.2, one step of
reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ might be
mapped to multiple steps of reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$ because the
translation of upcast possibly introduces multiple copies of the same term.
For instance, $\llbracket
M\vartriangleright\langle\ell_{1}:A;\ell_{2}:B\rangle\rrbracket=\langle\ell_{1}=\llbracket
M\rrbracket.\ell_{1};\ell_{2}=\llbracket M\rrbracket.\ell_{2}\rangle$. One
step of $\beta$-reduction in $M$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ is mapped
to at least two steps of $\beta$-reduction in the two copies of $\llbracket
M\rrbracket$ in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$.
Reflection is basically the reverse of simulation but requires at least one
step of reduction in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$.
The proofs of type preservation and operational correspondence can be found in
Section B.3.

###  4.4. Local Type-Only Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$

Before presenting the translation, let us focus on order of labels in types.
Though generally we treat row types as unordered collections, in this section
we assume, without loss of generality, that there is a canonical order on
labels, and the labels of any rows (including records) conform to this order.
This assumption is crucial in preserving the correspondence between labels and
presence variables bound by abstraction. For example, consider the type
$A=\langle\ell_{1}:A_{1};\dots;\ell_{n}:A_{n}\rangle$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$.
Following the idea of making records presence polymorphic as exemplified by
$\mathtt{getName^{\prime}}$ and $\mathtt{alice^{\prime}}$ in Section 2.2, this
record is translated as $\llbracket
A\rrbracket=\forall\theta_{1}\dots\theta_{n}.\langle\ell_{1}^{\theta_{1}}:\llbracket
A_{1}\rrbracket;\dots;\ell_{n}^{\theta_{n}}:\llbracket
A_{n}\rrbracket\rangle$. With the canonical order, we can guarantee that
$\ell_{i}$ always appears at the $i$-th position in the record and possesses
the presence variable bound at the $i$-th position. The full translation is as
follows.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Type}\to\mathsf{Type}\\\
\llbracket\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket~{}&=\hfil~{}&(\forall\theta_{i})_{i}.\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}\\\ \end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket\langle\ell_{i}=M_{i}\rangle_{i}^{\langle\ell_{i}:A_{i}\rangle_{i}}\rrbracket~{}&=\hfil~{}&(\Lambda\theta_{i})_{i}.\langle\ell_{i}=\llbracket
M_{i}\rrbracket\rangle_{i}^{\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}}\\\ \llbracket
M^{\langle\ell_{i}:A_{i}\rangle_{i}}.\ell_{j}\rrbracket~{}&=\hfil~{}&(\llbracket
M\rrbracket\,({P_{i}})_{i}).\ell_{j}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l@{\quad}l}{}\lx@intercol
P_{i}=\circ\hfil~{}&,i\neq j&P_{j}=\bullet\end{array}\lx@intercol\\\
\llbracket
M^{\langle\ell_{i}:A_{i}\rangle_{i}}\vartriangleright\langle\ell^{\prime}_{j}:A^{\prime}_{j}\rangle_{j}\rrbracket~{}&=\hfil~{}&(\Lambda\theta_{j})_{j}.\llbracket
M\rrbracket\,(@\,P_{i})_{i}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l@{\quad}l@{~}l}{}\lx@intercol
P_{i}=\circ\hfil~{}&,\ell_{i}\notin(\ell^{\prime}_{j})_{j}&P_{i}=\theta_{j}\hfil~{}&,\ell_{i}=\ell^{\prime}_{j}\end{array}\lx@intercol\\\
\end{array}$

The translation preserves typing derivations.

###### Theorem 4.7 (Type Preservation).

Every well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ term
$\Delta;\Gamma\vdash M:A$ is translated to a well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ term
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket A\rrbracket$.

Similarly to Section 4.2, we annotate type applications introduced by the
translation of upcast with @, and write $\leadsto_{\nu}$ for the associated
reduction rule and $\rightsquigarrow_{\nu}$ for its compatible closure.

$\begin{array}[]{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}\mathsf{\nu\textrm{-}PreLam}&(\Lambda\theta.M)\,@\,P~{}~{}&\leadsto_{\nu}\hfil~{}~{}&M[P/\theta]\\\
\end{array}$

We also re-use the $\mathsf{\blacktriangleright\\!\\!\textrm{-}Nested}$
reduction rule defined in Section 4.2. There is a one-to-one correspondence
between $\beta$-reductions (modulo $\rightsquigarrow_{\tau}$), and a
correspondence between one upcast reduction and a sequence of
$\rightsquigarrow_{\nu}$ reductions.

###### Theorem 4.8 (Operational Correspondence).

The translation $\llbracket-\rrbracket$ from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ has the
following properties:

  * _Simulation_

If $M\rightsquigarrow_{\beta}N$, then $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}\llbracket
N\rrbracket$; if $M\rightsquigarrow_{\vartriangleright}N$, then $\llbracket
M\rrbracket\rightsquigarrow_{\nu}^{\ast}\llbracket N\rrbracket$.

  * _Reflection_

If $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}\llbracket
N\rrbracket$, then $M\rightsquigarrow_{\beta}N$; if $\llbracket
M\rrbracket\rightsquigarrow_{\nu}N^{\prime}$, then there exists $N$ such that
$N^{\prime}\rightsquigarrow_{\nu}^{\ast}\llbracket N\rrbracket$ and
$M\rightsquigarrow_{\vartriangleright\blacktriangleright}N$.

Unlike Theorem 4.4, one step of reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ might be
mapped to multiple steps of reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ because we
might need to reduce the type application of multiple presence types in the
translation results of projection and upcast. Reflection is again basically
the reverse of simulation, requiring at least one step of reduction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$. The proofs
of type preservation and operational correspondence can be found in Section
B.4.

###  4.5. Swapping Row and Presence Polymorphism

In Section 4.2 and Section 4.4, we encode simple subtyping for variants using
row polymorphism, and simple subtyping for records using presence
polymorphism. These encodings enjoy the property that they only introduce new
type abstractions and applications. A natural question is whether we can swap
the polymorphism used by the encodings meanwhile preserve the type-only
property. As we have seen in Section 2.3, an intuitive attempt to encode
simple record subtyping with row polymorphism failed. Specifically, we have
the problematic translation

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\phantom{=}\
\llbracket\mathtt{getName}\
(\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle)\rrbracket\\\
&=\llbracket\mathtt{getName}\rrbracket\ (\mathsf{Age}:\mathsf{Int})\
\llbracket\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle\rrbracket\\\
&=\mathtt{getName}_{\text{\char 55}}\ (\mathsf{Age}:\mathsf{Int})\
\mathtt{alice}\end{array}~{}\end{array}$

First, the type information $\mathsf{Age}:\mathsf{Int}$ is not accessible to a
compositional type-only translation of the function application here.
Moreover, the type preservation property is also broken:
$\llbracket\mathtt{alice}\vartriangleright\langle\mathsf{Name}:\mathsf{String}\rangle\rrbracket$
should have type
$\llbracket\langle\mathsf{Name}:\mathsf{String}\rangle\rrbracket$, but here it
is just translated to $\mathtt{alice}$ itself, which has an extra label
$\mathsf{Age}$ in its record type. We give a general non-existence theorem.

###### Theorem 4.9.

There exists no global type-only encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}$, and no global
type-only encoding of $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}$.

The extensions for
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}$ and
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}$ are straightforward and
can be found in Appendix A. The proofs of this theorem can be found in Section
E.1. We will give further non-existence results in Section 5. The core idea
underlying the proofs of this kind of non-existence result is to construct
counterexamples and use proof by contradiction. One important observation is
that in our case a type-only translation ensures that terms are invariant
under the translation modulo type abstraction and type application. As a
consequence, we may characterise the general form of any such translation by
accounting for the possibility of adding type abstractions and type
applications in every possible position. Then we can obtain a contradiction by
considering the general form of type-only translations of carefully selected
terms.

To give an example, let us consider the proof of Theorem 4.9. Consider
$\langle\rangle$ and $\langle\ell=y\rangle\vartriangleright\langle\rangle$
which have the same type under environments $\Delta=\alpha_{0}$ and
$\Gamma=y:\alpha_{0}$. Any type-only translation must yield
$\llbracket\langle\rangle\rrbracket=\Lambda\overline{\alpha}.\langle\rangle$
and

$\llbracket\langle\ell=y\rangle\vartriangleright\langle\rangle\rrbracket=\Lambda\overline{\beta}.\llbracket\langle\ell=y\rangle\rrbracket\
\overline{B}=\Lambda\overline{\beta}.(\Lambda\overline{\alpha}^{\prime}.\langle\ell=\llbracket
y\rrbracket\ \overline{A}^{\prime}\rangle)\
\overline{B}=\Lambda\overline{\beta}.(\Lambda\overline{\alpha}^{\prime}.\langle\ell=(\Lambda\overline{\beta}^{\prime}.y)\
\overline{A}^{\prime}\rangle)\ \overline{B}$

which can be simplified to
$\Lambda\overline{\gamma}.\langle\ell=\Lambda\overline{\delta}.y\rangle$.
Thus, $\llbracket\langle\rangle\rrbracket$ has type
$\forall\overline{\alpha}.\langle\rangle$, and
$\llbracket\langle\ell=y\rangle\vartriangleright\langle\rangle\rrbracket$ has
type
$\forall\overline{\gamma}.\langle\ell:\forall\overline{\delta}.\alpha_{0}\rangle$.
By type preservation, they should still have the same type, which implies
$\forall\overline{\alpha}.\langle\rangle=\forall\overline{\gamma}.\langle\ell:\forall\overline{\delta}.\alpha_{0}\rangle$.
However, this equation obviously does not hold, showing a contradiction.

The above proof relies on the assumption that translations should always
satisfy the type preservation theorem. Sometimes this assumption can be too
strong. In order to show the robustness of our theorem, we provide three
proofs of Theorem 4.9 in Section E.1, where only one of them relies on type
preservation. The second proof uses the compositionality and a similar
argument to the $\mathtt{getName}_{\text{\char 55}}$ example in Section 2.3,
while the third proof does not rely on either of them.

In Section 6, we will show that it is possible to simulate record subtyping
with rank-1 row polymorphism and type inference, at the cost of a weaker type
preservation property and some extra conditions on the source language.

##  5\. Full Subtyping as Polymorphism

So far we have only considered simple subtyping, which means the subtyping
judgement applies shallowly to a single variant or record constructor (width
subtyping). Any notion of simple subtyping can be mechanically lifted to full
subtyping by inductively propagating the subtyping relation to the components
of each type. The direction of the subtyping relation remains the same for
covariant positions, and is reversed for contravariant positions.

In this section, we consider encodings of full subtyping. We first formalise
the calculus
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
with full subtyping for records and variants, and give its standard term-
involved translation to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$
(Section 5.1). Next we give a type-only encoding of strictly covariant record
subtyping (Section 5.2) and a non-existence result for variants (Section 5.3).
Finally, we give a non-existence result for type-only encodings of full record
subtyping as polymorphism (Section 5.4).

###  5.1. Local Term-Involved Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$

We first consider encoding
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$,
an extension of $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ and
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ with full
subtyping, in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$,
the combination of $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ and
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$. LABEL:fig:stlc-var-
rec-sub-full shows the standard full subtyping rules of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$.
We inductively propagate the subtyping relation to sub-types, and reverse the
subtyping order for function parameters because of contravariance. The
reflexivity and transitivity rules are admissible.

For the dynamic semantics of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$,
one option is to give concrete upcast rules for each value constructor,
similar to $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ and
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$. However,
as encoding full subtyping is more intricate than encoding simple subtyping
(especially the encoding in Section 5.2), upcast reduction rules significantly
complicate the operational correspondence theorems. To avoid such
complications we adopt an _erasure semantics_ for
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
which, following Pierce (2002), interprets upcasts as no-ops. The type erasure
function $\mathsf{erase}(-)$ transforms typed terms in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
to untyped terms in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$
by erasing all upcasts and type annotations. It is given by the homomorphic
extension of the following equations.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{erase}(M\vartriangleright
A)=\mathsf{erase}(M)\quad\mathsf{erase}(\lambda x^{A}.M)=\lambda
x.\mathsf{erase}(M)\quad\mathsf{erase}((\ell\,M)^{A})=\ell\,\mathsf{erase}(M)~{}\end{array}$

We show a correspondence between upcasting and erasure in Section C.2. In the
following, we always use the erasure semantics for calculi with full subtyping
or strictly covariant subtyping.

The idea of the local term-involved translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$
in Section 2.5 has been well-studied as the _coercion semantics_ of subtyping
(Breazu-Tannen et al., 1991, 1990; Pierce, 2002), which transforms subtyping
relations $A\leqslant B$ into coercion functions $\llbracket A\leqslant
B\rrbracket$. Writing translations in the form of coercion functions ensures
compositionality. The translation is standard and shown in Section C.1. For
instance, the full subtyping relation in Section 2.5 is translated to

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\phantom{=}\
\llbracket\langle\mathsf{Name}:\mathsf{String};\mathsf{Child}:\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\rangle\leqslant\langle\mathsf{Child}:\langle\mathsf{Name}:\mathsf{String}\rangle\rangle\rrbracket\\\
&=(\lambda
x.\langle\mathsf{Child}=\llbracket\langle\mathsf{Name}:\mathsf{String};\mathsf{Age}:\mathsf{Int}\rangle\leqslant\langle\mathsf{Name}:\mathsf{String}\rangle\rrbracket\
x.\mathsf{Child}\rangle)\\\ &=\lambda x.\langle\mathsf{Child}=(\lambda
x.\langle\mathsf{Name}=x.\mathsf{Name}\rangle)\ x.\mathsf{Child}\rangle)\\\
&\rightsquigarrow_{\beta}^{\ast}\lambda
x.\langle\mathsf{Child}=\langle\mathsf{Name}=x.\mathsf{Child}.\mathsf{Name}\rangle\rangle\end{array}~{}\end{array}$

We refer the reader to Pierce (2002) and Breazu-Tannen et al. (1990) for the
standard type preservation and operational correspondence theorems and proofs.

###  5.2. Global Type-Only Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$

As a stepping stone towards exploring the possibility of type-only encodings
of full subtyping, we first consider an easier problem: the encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$,
a calculus with strictly covariant structural subtyping for records. Strictly
covariant subtyping lifts simple subtyping through only the covariant
positions of all type constructors. For
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$,
the only change with respect to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
is to replace the subtyping rule $\mathsf{FS\textrm{-}Fun}$ with the following
rule which requires the parameter types to be equal:

$\displaystyle\displaystyle{\hbox{\hskip
15.52342pt\vbox{\hbox{\hskip-15.5234pt\hbox{\hbox{$\displaystyle\displaystyle
B\leqslant B^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
33.57887pt\vbox{\vbox{}\hbox{\hskip-33.57886pt\hbox{\hbox{$\displaystyle\displaystyle
A\to B\leqslant A\to B^{\prime}$}}}}}}$

As illustrated by the examples $\mathtt{carol}_{\text{\char 55}}$ and
$\mathtt{carol^{\prime}}$ from Section 2.5, we can extend the idea of encoding
simple record subtyping as presence polymorphism described in Section 4.4 by
hoisting quantifiers to the top-level, yielding a global but type-only
encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$. The full
type and term translations are spelled out in Figure 7 together with three
auxiliary functions.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Type}\to\mathsf{Type}\\\
\llbracket A\to B\rrbracket~{}&=\hfil~{}&\forall\overline{\theta}.\llbracket
A\rrbracket\to\llbracket B,\overline{\theta}\rrbracket\\\
\lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\theta}=\llparenthesis\theta,B\rrparenthesis\hfil~{}\\\
\end{array}\lx@intercol\\\
\llbracket\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket~{}&=\hfil~{}&\forall(\theta_{i})_{i}\,(\overline{\theta}_{i})_{i}.\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i},\overline{\theta}_{i}\rrbracket\rangle_{i}\\\
\lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\theta}_{i}=\llparenthesis\theta_{i},A_{i}\rrparenthesis\hfil~{}\\\
<EMAIL_ADDRESS>\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket\lambda
x^{A}.M^{B}\rrbracket~{}&=\hfil~{}&\Lambda\overline{\theta}.\lambda
x^{\llbracket A\rrbracket}.\llbracket M\rrbracket\ \overline{\theta}\\\
\lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\theta}=\llparenthesis\theta,B\rrparenthesis\hfil~{}\end{array}\lx@intercol\\\
\llbracket M^{A}\
N^{B}\rrbracket~{}&=\hfil~{}&\Lambda\overline{\theta}.(\llbracket M\rrbracket\
\overline{\theta})\ \llbracket N\rrbracket\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\theta}=\llparenthesis\theta,A\rrparenthesis\hfil~{}\end{array}\lx@intercol\\\
\llbracket\langle\ell_{i}=M_{i}^{A_{i}}\rangle_{i}\rrbracket~{}&=\hfil~{}&\Lambda(\theta_{i})_{i}\,(\overline{\theta}_{i})_{i}.\langle\ell_{i}=\llbracket
M_{i}\rrbracket\
\overline{\theta}_{i}\rangle_{i}^{\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\theta}_{i}=\llparenthesis\theta_{i},A_{i}\rrparenthesis\hfil~{}\\\
\end{array}\lx@intercol\\\ \llbracket
M^{\langle\ell_{i}:A_{i}\rangle_{i}}.\ell_{j}\rrbracket~{}&=\hfil~{}&\Lambda\overline{\theta}.(\llbracket
M\rrbracket\ (P_{i})_{i}\ (\overline{P}_{i})_{i<j}\ \overline{\theta}\
(\overline{P}_{i})_{j<i}).\ell_{j}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l@{\qquad}l}{}\lx@intercol
P_{i}=\circ\hfil~{}&,i\neq
j&\overline{\theta}=\llparenthesis\theta,A_{j}\rrparenthesis\\\ {}\lx@intercol
P_{j}=\bullet\hfil~{}&&\overline{P}_{i}=\llparenthesis\circ,A_{i}\rrparenthesis\end{array}\lx@intercol\\\
\llbracket M^{A}\vartriangleright
B\rrbracket~{}&=\hfil~{}&\Lambda\overline{\theta}.\llbracket M\rrbracket\
{\overline{P}}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol(\overline{\theta},\overline{P})=\llparenthesis\theta,A\leqslant
B\rrparenthesis\hfil~{}\end{array}\lx@intercol\\\ \end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-,-\rrbracket~{}&:\hfil~{}&(\mathsf{Type},\overline{\mathsf{Pre}})\to\mathsf{Type}\\\
\llbracket
A,\overline{P}\rrbracket~{}&=\hfil~{}&A^{\prime}[\overline{P}/\overline{\theta}^{\prime}]\\\
\lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l<EMAIL_ADDRESS><EMAIL_ADDRESS>\llparenthesis-,-\rrparenthesis~{}&:\hfil~{}&(\mathsf{Pre},\mathsf{Type})\to\overline{\mathsf{Pre}}\\\
\llparenthesis P,\alpha\rrparenthesis~{}&=\hfil~{}&\cdot\\\ \llparenthesis
P,A\to B\rrparenthesis~{}&=\hfil~{}&\llparenthesis P,B\rrparenthesis\\\
\llparenthesis
P,\langle\ell_{i}:A_{i}\rangle_{i}\rrparenthesis~{}&=\hfil~{}&(P_{i})_{i}\
\llparenthesis P_{i},A_{i}\rrparenthesis_{i}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol P_{i}=\theta_{i}\hfil~{}&,P\text{
is a variable }\theta\\\ {}\lx@intercol P_{i}=\circ\hfil~{}&,P=\circ\\\
{}\lx@intercol
<EMAIL_ADDRESS>~{}\\\
\lx@intercol\hfil\llparenthesis-,-\rrparenthesis:(\mathsf{Pre},\mathsf{Type}\leqslant\mathsf{Type})\to(\overline{\mathsf{Pre}},\overline{\mathsf{Pre}}){}\hfil{}\hfil\\\
\llparenthesis\theta,\alpha\leqslant\alpha\rrparenthesis~{}&=\hfil~{}&(\cdot,\cdot)\\\
\llparenthesis\theta,A\to B\leqslant A\to
B^{\prime}\rrparenthesis~{}&=\hfil~{}&\llparenthesis\theta,B\leqslant
B^{\prime}\rrparenthesis\\\
\llparenthesis\theta,\langle\ell_{i}:A_{i}\rangle_{i}\leqslant\langle\ell_{j}^{\prime}:A_{j}^{\prime}\rangle_{j}\rrparenthesis~{}&=\hfil~{}&((\theta_{j})_{j}\
(\overline{\theta}_{j})_{j},(P_{i})_{i}\ (\overline{P}_{i})_{i})\\\
\lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l@{\qquad}l@{~}l}~{}\lx@intercol(\overline{\theta}_{j},\overline{P}_{j}^{\prime})=\llparenthesis\theta_{j},A_{i}\leqslant
A_{j}^{\prime}\rrparenthesis,\ell_{i}=\ell_{j}^{\prime}{}\hfil{}\hfil\hfil\\\
{}\lx@intercol
P_{i}=\circ\hfil~{}&,\ell_{i}\notin(\ell^{\prime}_{j})_{j}&\overline{P}_{i}=\llparenthesis\circ,A_{i}\rrparenthesis\hfil~{}&,\ell_{i}\notin(\ell^{\prime}_{j})_{j}\\\
{}\lx@intercol
P_{i}=\theta_{j}\hfil~{}&,\ell_{i}=\ell_{j}^{\prime}&\overline{P}_{i}=\overline{P}_{j}^{\prime}\hfil~{}&,\ell_{i}=\ell_{j}^{\prime}\end{array}\lx@intercol\\\
\end{array}$

Figure 7. A global type-only translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
to $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$.

As in Section 4.4, we rely on a canonical order on labels. The auxiliary
function $\llbracket A,\overline{P}\rrbracket$ instantiates a polymorphic type
$A$ with $\overline{P}$, simulating the type application in the term level.
The auxiliary function $\llparenthesis\theta,A\rrparenthesis$ takes a presence
variable $\theta$ and a type $A$, and generates a sequence of presence
variables based on $\theta$ that have the same length as the presence
variables bound by $\llbracket A\rrbracket$. It is used to allocate a fresh
presence variable for every label in records on strictly covariant positions.
We can also use it to generate a sequence of $\bullet$ or $\circ$ for the
instantiation of $\llbracket A\rrbracket$ by
$\llparenthesis\bullet,A\rrparenthesis$ and
$\llparenthesis\circ,A\rrparenthesis$. The auxiliary function
$\llparenthesis\theta,A\leqslant B\rrparenthesis$ takes a presence variable
$\theta$ and a subtyping relation $A\leqslant B$, and returns a pair
$(\overline{\theta},\overline{P})$. The sequence of presence variables
$\overline{\theta}$ is the same as $\llparenthesis\theta,B\rrparenthesis$. The
sequence of presence types are used to instantiate $\llbracket A\rrbracket$ to
get $\llbracket B\rrbracket$ (as illustrated by the term translation
$\llbracket M^{A}\vartriangleright
B\rrbracket=\Lambda\overline{\theta}.\llbracket M\rrbracket\,{\overline{P}}$
which has type $\llbracket B\rrbracket$).

The translation on types is straightforward. We not only introduce a presence
variable for every element of record types, but also move the quantifiers of
the types of function bodies and record elements to the top level, as they are
on strictly covariant positions. While the translation on terms (derivations)
may appear complicated, it mainly focuses on moving type abstractions to the
top level by type application and re-abstraction using the auxiliary
functions. For the projection and upcast cases, it also instantiates the sub-
terms with appropriate presence types. Notice that for function application
$M\ N$, we only need to move the type abstractions in $\llbracket
M\rrbracket$, and for projection $M.\ell_{j}$, we only need to move the type
abstractions in the payload of $\ell_{j}$.

Strictly speaking, the type translation is actually not compositional because
of the type application introduced by the term translation. As a consequence,
in the type translation, we need to use the auxiliary function $\llbracket
A,\overline{P}\rrbracket$ which looks into the concrete structure of
$\llbracket A\rrbracket$ instead of using it compositionally. However, we
believe that it is totally fine to slightly compromise the compositionality of
the type translation, which is much less interesting than the compositionality
of the term translation. Moreover, we can still make the type translation
compositional by extending the type syntax with type operators and type-level
type application of System F$\omega$.

We have the following type preservation theorem. The proof shown in Section
C.3 follows from induction on typing derivations of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$.

###### Theorem 5.1 (Type Preservation).

Every well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
term $\Delta;\Gamma\vdash M:A$ is translated to a well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ term
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket A\rrbracket$.

In order to state an operational correspondence result, we use the erasure
semantics for
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ given by the
standard type erasure function defined as the homomorphic extension of the
following equations.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\mathsf{erase}(\Lambda\theta.M)=\mathsf{erase}(M)\quad\mathsf{erase}(M\
P)=\mathsf{erase}(M)\quad\mathsf{erase}(\lambda x^{A}.M)=\lambda
x.\mathsf{erase}(M)~{}\end{array}$

Since the terms in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
and $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ are both
erased to untyped $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$,
for the operational correspondence we need only show that any term in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
is still erased to the same term after translation.

###### Theorem 5.2 (Operational Correspondence).

The translation $\llbracket-\rrbracket$ from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
to $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$ satisfies
the equation $\mathsf{erase}(M)=\mathsf{erase}(\llbracket M\rrbracket)$ for
any well-typed term $M$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$.

###### Proof.

By straightforward induction on $M$. ∎

By using erasure semantics, the operational correspondence becomes concise and
obvious for type-only translations, as all constructs introduced by type-only
translations are erased by type erasure functions. It is also possible to
reformulate Theorem 4.4 and Theorem 4.8 to use erasure semantics, but the
current versions are somewhat more informative and not excessively complex.

###  5.3. Non-Existence of Type-Only Encodings of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{co}}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho\theta}$

As illustrated by the example $\mathtt{parseAge}_{\text{\char 55}}\
\mathtt{data}_{\text{\char 55}}$ in Section 2.6, the approach of hoisting
quantifiers to the top-level does not work for variants, because of case
splits. Formally, we have the following general non-existence theorem showing
that no other approaches exist.

###### Theorem 5.3.

There exists no global type-only encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{co}}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho\theta}$.

The idea of the proof is the same as that of Theorem 4.9 which we have shown
in Section 4.5: construct the schemes of type-only translations for certain
terms and derive a contradiction. The terms we choose here are the nested
variant $M=(\ell\,(\ell\,y)^{[\ell]})^{[\ell:[\ell]]}$ for some free term
variable $y$ in the environment together with its upcast
$M_{1}=M\vartriangleright[\ell:[\ell;\ell^{\prime}]]$ and its case split
$M_{2}=\mathbf{case}\ M\ \\{\ell\ x\mapsto
x\vartriangleright[\ell;\ell^{\prime}]\\}$, similar to the counterexamples we
give in Section 2.6. To obtain a contradiction, we show that we cannot give a
uniform type-only translation of $M$ such that both $M_{1}$ and $M_{2}$ can be
translated compositionally. The details of the proof can be found in Section
E.2.

As a corollary, there can be no global type-only encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant\mathrm{full}}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho\theta}$.

One might worry that Theorem 5.3 contradicts the duality between records and
variants, especially in light of Blume et al. (2006)’s translation from
variants with default cases to records with record extensions. In their
translation, a variant is translated to a function which takes a record of
functions. For instance, the translation of variant types is:

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket[\ell_{i}:A_{i}]_{i}\rrbracket=\forall\alpha.\langle\ell_{i}:A_{i}\to\alpha\rangle_{i}\to\alpha~{}\end{array}$

In fact, there is no contradiction because a variant in a covariant position
corresponds to a record in a contravariant position, which means that the
encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{co}}$
in Section 5.2 cannot be used. Moreover, the translation from variants to
records is not type-only as it introduces $\lambda$-abstractions.

###  5.4. Non-Existence of Type-Only Encodings of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho\theta}$

As illustrated by the examples $\mathtt{getName^{\prime}}_{\text{\char 55}}$
and $\mathtt{getUnit}_{\text{\char 55}}$ in Section 2.7, one attempt to
simulate full record subtyping by both making record types presence-
polymorphic and adding row variables for records in contravariant positions
fails. In fact no such encoding exists.

###### Theorem 5.4.

There exists no global type-only encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho\theta}$.

Again, the proof idea is to give general forms of type-only translations for
certain terms and proof by contradiction. Our choice of terms here are
different from the counterexamples in Section 2.7 this time. Instead, we first
consider two functions $f_{1}=\lambda x^{\langle\rangle}.x$ and $f_{2}=\lambda
x^{\langle\rangle}.\langle\rangle$ of the same type
$\langle\rangle\to\langle\rangle$. Any type-only translations of these
functions must yield terms of the following forms:

$\begin{array}[]{l@{}l@{}c@{}l}\llbracket
f_{1}\rrbracket&=\Lambda\overline{\alpha}_{1}.\lambda
x^{A_{1}}.\Lambda\overline{\beta}_{1}.&x&\ \overline{B}_{1}\\\ \llbracket
f_{2}\rrbracket&=\Lambda\overline{\alpha}_{2}.\lambda
x^{A_{2}}.\Lambda\overline{\beta}_{2}.&\llbracket\langle\rangle\rrbracket&\
\overline{B}_{2}=\Lambda\overline{\alpha}_{2}.\lambda
x^{A_{2}}.\Lambda\overline{\beta}_{2}.(\Lambda\overline{\gamma}.\langle\rangle)\
\overline{B}_{2}\end{array}$

By type preservation, they should have the same type, which means $x\
\overline{B}_{1}$ and $(\Lambda\overline{\gamma}.\langle\rangle)\
\overline{B}_{2}$ should also have the same type. As a result, the type
$A_{1}$ of $x$ cannot contain any type variables bound in
$\overline{\alpha}_{1}$ unless they are inside the type of some labels which
are instantiated to absent by the type application $x\ \overline{B}_{1}$.
Then, it is problematic when we want to upcast the parameter of $f_{1}$ to be
a wider record, e.g.,
$f_{1}\vartriangleright(\langle\ell:\langle\rangle\rangle\to\langle\rangle)$.
Intuitively, because $A_{1}$ cannot be an open record type with the row
variable bound in $\overline{\alpha}_{1}$, we actually have no way to expand
$A_{1}$, which leads to a contradiction. The full proof can be found in
Section E.3.

##  6\. Full Subtyping as Rank-1 Polymorphism

In Section 4.5, we showed that no type-only encoding of record subtyping as
row polymorphism exists. The main obstacle is a lack of type information for
instantiation. By focusing on rank-1 polymorphism in the target language, we
need no longer concern ourselves with type abstraction and application
explicitly anymore. Instead we defer to Hindley-Milner type inference (Damas
and Milner, 1982) as demonstrated by the examples in Section 2.4. In this
section, we formalise the encodings of full subtyping as rank-1 polymorphism.

Here we focus on the encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$, a ML-
style calculus with records and rank-1 row polymorphism (the same idea applies
to each combination of encoding records or variants as rank-1 row polymorphism
or rank-1 presence polymorphism). The specification of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ is given in
Section A.3, which uses a standard declarative Hindley-Milner style type
system and extends the term syntax with let-binding
$\mathbf{let}\,x=M\,\mathbf{in}\,N$ for polymorphism. We also extend
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
with let-binding syntax and its standard typing and operational semantics
rules.

As demonstrated in Section 2.4, we can use the following (local and type-only)
erasure translation to encode
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$,
the fragment of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
where types are restricted to have rank-2 records, in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket M\vartriangleright A\rrbracket~{}&=\hfil~{}&M\end{array}$

Since the types of translated terms in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ are given by
type inference, we do not need to use a translation on types in the
translation on terms. Moreover, we implicitly allow type annotations on
$\lambda$-abstractions to be erased as they no longer exist in the target
language.

To formalise the definition of rank-$n$ records defined in Section 2.4, we
introduce the predicate $\mho^{n}(A)$ defined as follows for any natural
number $n$.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{split}\mho^{n}(\alpha)&=\mathsf{true}\\\
\mho^{n}(A\to B)&=\mho^{n-1}(A)\land\mho^{n}(B)\\\
\mho^{n}(\langle\ell_{i}:A_{i}\rangle_{i})&=\land_{i}\mho^{n}(A_{i})\end{split}\qquad\begin{split}\mho^{0}(\alpha)&=\mathsf{true}\\\
\mho^{0}(A\to B)&=\mho^{0}(A)\land\mho^{0}(B)\\\
\mho^{0}(\langle\ell_{i}:A_{i}\rangle_{i})&=\mathsf{false}\end{split}~{}\end{array}$

We define a type $A$ to have rank-$n$ records, if $\mho^{n}(A)$ holds. The
predicate $\mho^{n}(A)$ basically means no record types can appear in the left
subtrees of $n$ or more arrows.

The operational correspondence of the erasure translation comes for free. Note
that both
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
and $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ are type
erased to untyped $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$.
The type erasure function of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
inherited from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
in Section 5.1 is identical to the erasure translation. The type erasure
function $\mathsf{erase}(-)$ of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ is simply
the identity function (as there is no type annotation at all). We have the
following theorem.

###### Theorem 6.1 (Operational Correspondence).

The translation $\llbracket-\rrbracket$ from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
to $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ satisfies
the equation $\mathsf{erase}(M)=\mathsf{erase}(\llbracket M\rrbracket)$ for
any well-typed term $M$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$.

###### Proof.

By definition of $\mathsf{erase}(-)$ and $\llbracket-\rrbracket$. ∎

Proving type preservation is more challenging. To avoid the complexity of
reasoning about type inference, we state the type preservation theorem using
the declarative type system of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$, which
requires us to give translations on types. We define the translations on types
and environments in Figure 8. As in Section 4.4 and Section 5.2, we assume a
canonical order on labels and require all rows and records to conform to this
order. The translation on type environments is still the identity
$\llbracket\Delta\rrbracket=\Delta$. To define the translation on term
environments, we need to explicitly distinguish between variables bound by
$\lambda$ and variables bound by $\mathbf{let}$. We write $a,b$ for the
former, and $x,y$ for the latter. Because the translation on term environments
may introduce fresh free type variables which are not in the original type
environments, we define $\llbracket\Delta;\Gamma\rrbracket$ as a shortcut for
$(\llbracket\Delta\rrbracket,\mathsf{ftv}(\llbracket\Gamma\rrbracket));\llbracket\Gamma\rrbracket$.

The type translation $\llbracket A\rrbracket$ returns a type scheme. It opens
up row types in $A$ that appear strictly covariantly inside the left-hand-side
of strictly covariant function types, binding all of the freshly generated row
variables at the top-level. It applies the auxiliary translation $\llbracket
A\rrbracket^{\ast}$ to function parameter types, similarly extending all
record types appearing strictly covariantly in $A$ with fresh row variables,
and binding them all at the top-level.

We define four auxiliary functions for the translation. The functions
$\llparenthesis\rho,A\rrparenthesis$ and
$\llparenthesis\rho,A\rrparenthesis^{\ast}$ are used to generate fresh row
variables. The $\llparenthesis\rho,A\rrparenthesis$ takes a row variable
$\rho$ and a type $A$, and generates a sequence of row variables based on
$\rho$ with the same length of row variables bound by $\llbracket
A\rrbracket$. The function $\llparenthesis\rho,A\rrparenthesis^{\ast}$ does
the same thing for $\llbracket A\rrbracket^{\ast}$. The functions $\llbracket
A,\overline{\rho}\rrbracket$ and $\llbracket
A,\overline{\rho}\rrbracket^{\ast}$ instantiate polymorphic types, simulating
term-level type application. As we discussed in Section 5.2, these functions
actually break the compositionality of the type translation, because they must
inspect the concrete structure of $\llbracket A\rrbracket$. However, we only
use the type translation in the theorem and proof; the compositionality of the
erasure translation itself remains intact.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Type}\to\mathsf{TypeScheme}\\\
\llbracket A\to
B\rrbracket~{}&=\hfil~{}&\forall\overline{\rho}_{1}\overline{\rho}_{2}.\llbracket
A,\overline{\rho}_{1}\rrbracket^{\ast}\to\llbracket
B,\overline{\rho}_{2}\rrbracket\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\rho}_{1}=\llparenthesis\rho_{1},A\rrparenthesis^{\ast},\
\overline{\rho}_{2}=\llparenthesis\rho_{2},B\rrparenthesis\hfil~{}\\\
\end{array}\lx@intercol\\\
\llbracket\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket~{}&=\hfil~{}&\forall(\overline{\rho}_{i})_{i}.\langle\ell_{i}:\llbracket
A_{i},\overline{\rho}_{i}\rrbracket\rangle_{i}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\rho}_{i}=\llparenthesis\rho_{i},A_{i}\rrparenthesis\hfil~{}\\\
<EMAIL_ADDRESS>\llbracket-,-\rrbracket~{}&:\hfil~{}&(\mathsf{Type},\overline{\mathsf{RowVar}})\to\mathsf{Type}\\\
\llbracket
A,\overline{\rho}\rrbracket~{}&=\hfil~{}&A^{\prime}[\overline{\rho}/\overline{\rho}^{\prime}]\
\text{where}\ \forall\overline{\rho}^{\prime}.A^{\prime}=\llbracket
A\rrbracket\\\\[7.74997pt]
\llparenthesis-,-\rrparenthesis~{}&:\hfil~{}&(\mathsf{RowVar},\mathsf{Type})\to\overline{\mathsf{RowVar}}\\\
\llparenthesis\rho,\alpha\rrparenthesis~{}&=\hfil~{}&\cdot\\\
\llparenthesis\rho,A\to
B\rrparenthesis~{}&=\hfil~{}&\llparenthesis\rho_{1},A\rrparenthesis^{\ast}\,\llparenthesis\rho_{2},B\rrparenthesis\\\
\llparenthesis\rho,\langle\ell_{i}:A_{i}\rangle_{i}\rrparenthesis~{}&=\hfil~{}&\llparenthesis\rho_{i},A_{i}\rrparenthesis_{i}\\\\[7.74997pt]
\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Env}\to\mathsf{Env}\\\
\llbracket\cdot\rrbracket~{}&=\hfil~{}&\cdot\\\
\llbracket\Gamma,x:A\rrbracket~{}&=\hfil~{}&\llbracket\Gamma\rrbracket,x:\llbracket
A\rrbracket\\\
\llbracket\Gamma,a:A\rrbracket~{}&=\hfil~{}&\llbracket\Gamma\rrbracket,a:\llbracket
A,\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\rrbracket^{\ast}\\\
\end{array}$

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket^{\ast}~{}&:\hfil~{}&\mathsf{Type}\to\mathsf{TypeScheme}\\\
\llbracket A\to
B\rrbracket^{\ast}~{}&=\hfil~{}&\forall\overline{\rho}.A\to\llbracket
B,\overline{\rho}\rrbracket^{\ast}\\\ \lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\rho}=\llparenthesis\rho,B\rrparenthesis^{\ast}\hfil~{}\\\
\end{array}\lx@intercol\\\
\llbracket\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket^{\ast}~{}&=\hfil~{}&\forall\rho\,(\overline{\rho}_{i})_{i}.\langle\ell_{i}:\llbracket
A_{i},\overline{\rho}_{i}\rrbracket^{\ast};\rho\rangle_{i}\\\
\lx@intercol\hfil\text{where
}\begin{array}[t]{@{~}l@{~}l}{}\lx@intercol\overline{\rho}_{i}=\llparenthesis\rho_{i},A_{i}\rrparenthesis^{\ast}\hfil~{}\\\
<EMAIL_ADDRESS>\llbracket-,-\rrbracket^{\ast}~{}&:\hfil~{}&(\mathsf{Type},\overline{\mathsf{RowVar}})\to\mathsf{Type}\\\
\llbracket
A,\overline{\rho}\rrbracket^{\ast}~{}&=\hfil~{}&A^{\prime}[\overline{\rho}/\overline{\rho}^{\prime}]\
\text{where}\ \forall\overline{\rho}^{\prime}.A^{\prime}=\llbracket
A\rrbracket^{\ast}\\\\[7.74997pt]
\llparenthesis-,-\rrparenthesis^{\ast}~{}&:\hfil~{}&(\mathsf{RowVar},\mathsf{Type})\to\overline{\mathsf{RowVar}}\\\
\llparenthesis\rho,\alpha\rrparenthesis^{\ast}~{}&=\hfil~{}&\cdot\\\
\llparenthesis\rho,A\to
B\rrparenthesis^{\ast}~{}&=\hfil~{}&\llparenthesis\rho,B\rrparenthesis^{\ast}\\\
\llparenthesis\rho,\langle\ell_{i}:A_{i}\rangle_{i}\rrparenthesis^{\ast}~{}&=\hfil~{}&\rho\,\llparenthesis\rho_{i},A_{i}\rrparenthesis^{\ast}_{i}\\\
\end{array}$

Figure 8. The translations of types and environments from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
to $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$.

After giving the type and environment translation, we aim for a weak type
preservation theorem which allows the translated terms to have subtypes of the
original terms, because the erasure translation ignores all upcasts. As we
have row variables in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$, the types
of translated terms may contain extra row variables in strictly covariant
positions. We need to define an auxiliary subtype relation $\preccurlyeq$
which only considers row variables.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
11.75732pt\vbox{\vbox{}\hbox{\hskip-11.75731pt\hbox{\hbox{$\displaystyle\displaystyle\alpha\preccurlyeq\alpha$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
16.60454pt\vbox{\hbox{\hskip-16.60454pt\hbox{\hbox{$\displaystyle\displaystyle[A_{i}\preccurlyeq
A_{i}^{\prime}]_{i}$}}}\vbox{}}}\over\hbox{\hskip
31.98688pt\vbox{\vbox{}\hbox{\hskip-31.98686pt\hbox{\hbox{$\displaystyle\displaystyle\langle\ell_{i}:A_{i}\rangle_{i}\preccurlyeq\langle\ell_{i}:A_{i}^{\prime}\rangle_{i}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
16.60454pt\vbox{\hbox{\hskip-16.60454pt\hbox{\hbox{$\displaystyle\displaystyle[A_{i}\preccurlyeq
A_{i}^{\prime}]_{i}$}}}\vbox{}}}\over\hbox{\hskip
39.81345pt\vbox{\vbox{}\hbox{\hskip-39.81343pt\hbox{\hbox{$\displaystyle\displaystyle\langle(\ell_{i}:A_{i})_{i};\rho\rangle\preccurlyeq\langle\ell_{i}:A_{i}^{\prime}\rangle_{i}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
13.97115pt\vbox{\hbox{\hskip-13.97113pt\hbox{\hbox{$\displaystyle\displaystyle
B\preccurlyeq B^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
30.22118pt\vbox{\vbox{}\hbox{\hskip-30.22116pt\hbox{\hbox{$\displaystyle\displaystyle
A\to B\preccurlyeq A\to B^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
10.6274pt\vbox{\hbox{\hskip-10.62738pt\hbox{\hbox{$\displaystyle\displaystyle\tau\preccurlyeq\tau^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
31.17155pt\vbox{\vbox{}\hbox{\hskip-31.17154pt\hbox{\hbox{$\displaystyle\displaystyle\forall\rho^{K}.\tau\preccurlyeq\forall\rho^{K}.\tau^{\prime}$}}}}}}$

Finally, we have the following weak type preservation theorem.

###### Theorem 6.2 (Weak Type Preservation).

Every well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
term $\Delta;\Gamma\vdash M:A$ is translated to a well-typed
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ term
$\llbracket\Delta;\Gamma\rrbracket\vdash\llbracket M\rrbracket:\tau$ for some
$A^{\prime}\leqslant A$ and $\tau\preccurlyeq\llbracket A^{\prime}\rrbracket$.

The proof makes use of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{afull}}$,
an algorithmic variant of the type system of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
which combines $\mathsf{T\textrm{-}App}$ and $\mathsf{T\textrm{-}Upcast}$ into
one rule $\mathsf{T\textrm{-}AppSub}$, and removes all explicit upcasts in
terms.

$\displaystyle\mathsf{T\textrm{-}AppSub}$
$\displaystyle\displaystyle{\hbox{\hskip
100.12477pt\vbox{\hbox{\hskip-100.12477pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash
M:A\to B$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash
N:A^{\prime}$}\hskip 20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
A^{\prime}\leqslant A$}}}}}\vbox{}}}\over\hbox{\hskip
34.3488pt\vbox{\vbox{}\hbox{\hskip-34.34879pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\Gamma\vdash
M\,N:B$}}}}}}$

It is standard that
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{afull}}$
is sound and complete with respect to
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
(Pierce, 2002). Immediately, we have that $\Delta;\Gamma\vdash M:A$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
implies $\Delta;\Gamma\vdash\widehat{M}:A^{\prime}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{afull}}$
for some $A^{\prime}\leqslant A$, where $\widehat{M}$ is defined as $M$ with
all upcasts erased. Thus, we only need to prove that $\Delta;\Gamma\vdash M:A$
in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{afull}}$
implies $\llbracket\Delta;\Gamma\rrbracket\vdash\llbracket M\rrbracket:\tau$
for some $\tau\preccurlyeq\llbracket A\rrbracket$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$. The
remaining proof can be done by induction on the typing derivations in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{afull}}$,
where the most non-trivial case is the $\mathsf{T\textrm{-}AppSub}$ rule. The
core idea is to use instantiation in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$ to simulate
the subtyping relation $A^{\prime}\leqslant A$ in the
$\mathsf{T\textrm{-}AppSub}$ rule. This is possible because the source
language
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{afull}}$
is restricted to have rank-$2$ records, which implies that $A\to B$ is
translated to a polymorphic type where the record types in parameters are open
and can be extended to simulate the subtyping relation. The full proof can be
found in Section D.1.

So far, we have formalised the erasure translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
to $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$. As shown
in Section 2.4, we have three other results. For records, we have another
erasure translation from
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}1}^{\leqslant\mathrm{full}}$,
the fragment of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
where types are restricted to have rank-1 records, to
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta 1}$ with
rank-1 presence polymorphism. Similarly, for variants, we formally define a
type $A$ to have rank-$n$ variants, if the predicate $\Omega^{n}(A)$ defined
as follows holds.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{split}\Omega^{n}(\alpha)&=\mathsf{true}\\\
\Omega^{n}(A\to B)&=\Omega^{n-1}(A)\land\Omega^{n}(B)\\\
\Omega^{n}([\ell_{i}:A_{i}]_{i})&=\land_{i}\Omega^{n}(A_{i})\end{split}\qquad\begin{split}\Omega^{0}(\alpha)&=\mathsf{true}\\\
\Omega^{0}(A\to B)&=\Omega^{0}(A)\land\Omega^{0}(B)\\\
\Omega^{0}([\ell_{i}:A_{i}]_{i})&=\mathsf{false}\end{split}~{}\end{array}$

We also have two erasure translations from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}1}^{\leqslant\mathrm{full}}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho 1}$ and from
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}2}^{\leqslant\mathrm{full}}$ to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta 1}$. They all use the same
idea to let type inference infer row/presence-polymorphic types for terms
involving records/variants, and use instantiation to automatically simulate
subtyping. We omit the metatheory of these three results as they are similar
to what we have seen for the encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
in $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$.

The requirement of rank-1 polymorphism and Hindley-Milner type inference for
target languages is not mandatory; target languages can support more advanced
type inference for higher-rank polymorphism like FreezeML (Emrich et al.,
2020), as long as no type annotation is needed to infer rank-1 polymorphic
types. One might hope to also relax the $\mho^{2}(-)$ restriction in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
via enabling higher-rank polymorphism. However, at least the erasure
translation do not work anymore. For instance, consider the functions
$\mathtt{id}=\lambda x^{\langle\ell:\mathsf{Int}\rangle}.x$ and
$\mathtt{const}=\lambda
x^{\langle\ell:\mathsf{Int}\rangle}.\langle\ell=1\rangle$ with the same type
$\langle\ell:\mathsf{Int}\rangle\to\langle\ell:\mathsf{Int}\rangle$. Type
inference would give $\llbracket\mathtt{id}\rrbracket$ the type
$\forall\rho^{\mathsf{Row}_{\\{\ell\\}}}.\langle\ell:\mathsf{Int};\rho\rangle\to\langle\ell:\mathsf{Int};\rho\rangle$,
and $\llbracket\mathtt{const}\rrbracket$ the type
$\forall\rho^{\mathsf{Row}_{\\{\ell\\}}}.\langle\ell:\mathsf{Int};\rho\rangle\to\langle\ell:\mathsf{Int}\rangle$.
For a second-order function of type
$(\langle\ell:\mathsf{Int}\rangle\to\langle\ell:\mathsf{Int}\rangle)\to A$, we
cannot give a type to the parameter of the function after translation which