can be unified with the types of both $\llbracket\mathtt{id}\rrbracket$ and
$\llbracket\mathtt{const}\rrbracket$. We leave it to future work to explore
whether there exist other translations making use of type inference for
higher-rank polymorphism.

##  7\. Discussion

We have now explored a range of encodings of structural subtyping for variants
and records as parametric polymorphism under different conditions. These
encodings and non-existence results capture the extent to which row and
presence polymorphism can simulate structural subtyping and crystallise
longstanding folklore and informal intuitions. In the remainder of this
section we briefly discuss record extensions and default cases (Section 7.1),
combining subtyping and polymorphism (Section 7.2), related work (Section 7.3)
and conclusions and future work (Section 7.4).

###  7.1. Record Extensions and Default Cases

Two important extensions to row and presence polymorphism are record
extensions (Rémy, 1994), and its dual, default cases (Blume et al., 2006).
These operations provide extra expressiveness beyond structural subtyping. For
example, with default cases, we can give a default age $42$ to the function
$\mathtt{getAge}$ in Section 2.1, and then apply it to variants with arbitrary
constructors.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\begin{array}[]{rll}&\mathtt{getAgeD}:\>\,\forall\rho^{\mathsf{Row}_{\\{\mathsf{Age},\mathsf{Year}\\}}}.{[\mathsf{Age}:\mathsf{Int};\mathsf{Year}:\mathsf{Int};\rho]}\to\mathsf{Int}\\\
&\mathtt{getAgeD}=\lambda x.~{}\mathbf{case}\,x\,\\{\mathsf{Age}\,y\mapsto
y;\mathsf{Year}\,y\mapsto 2023-y;z\mapsto 42\\}\\\ &\mathtt{getAgeD}\
(\mathsf{Name}\,\text{\textquotedbl
Carol\textquotedbl})\rightsquigarrow_{\beta}^{\ast}42\end{array}~{}\end{array}$

###  7.2. Combining Subtyping and Polymorphism

Though row and presence polymorphism can simulate subtyping well and support
expressive extensions like record extension and default cases, it can still be
beneficial to allow both subtyping and polymorphism together in the same
language. For example, the OCaml programming language combines row and
presence polymorphism with subtyping. Row and presence variables are hidden in
its core language. It supports both polymorphic variants and polymorphic
objects (a variation on polymorphic records) as well as explicit upcast for
closed variants and records. Our results give a rationalisation for why OCaml
supports subtyping in addition to row polymorphism. Row polymorphism simply is
not expressive enough to give a local encoding of unrestricted structural
subtyping, even though OCaml indirectly supports full first-class
polymorphism.

Bounded quantification (Cardelli and Wegner, 1985; Cardelli et al., 1994)
extends system F with subtyping by introducing subtyping bounds to type
variables. There is also much work on the type inference for both polymorphism
and subtyping based on collecting, solving, and simplifying constraints
(Trifonov and Smith, 1996; Pottier, 1998, 2001). Algebraic subtyping (Dolan
and Mycroft, 2017; Dolan, 2016) combines subtyping and parametric
polymorphism, offering compact principal types and decidable subsumption
checking. MLstruct (Parreaux and Chau, 2022) extends algebraic subtyping with
intersection and union types, giving rise to another alternative to row
polymorphism.

###  7.3. Related Work

#### Row types.

Wand (1987) first introduced rows and row polymorphism. There are many further
papers on row types, which take a variety of approaches, particularly focusing
on extensible records. Harper and Pierce (1990) extended System F with
constrained quantification, where predicates $\rho\,\mathsf{lacks}\,L$ and
$\rho\,\mathsf{has}\,L$ are used to indicate the presence and absence of
labels in row variables. Gaster and Jones (1996) and Gaster (1998) explored a
calculus with a similar $\mathsf{lacks}$ predicate based on qualified types.
Rémy (1989) introduced the concept of presence types and polymorphism, and
Rémy (1994) combines row and presence polymorphism. Leijen (2005) proposed a
variation on row polymorphism with support for scoped labels. Pottier and Rémy
(2004) considered type inference for row and presence polymorphism in HM(X).
Morris and McKinna (2019) introduced Rose, an algebraic foundation for row
typing via a rather general language with two predicates representing the
containment and combination of rows. It is parametric over a row theory which
enables it to express different styles of row types (including Wand and Rémy’s
style and Leijen’s style).

#### Row polymorphism vs structural subtyping.

Wand (1987) compared his calculus with row polymorphism (similar to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho
1}$) with Cardelli (1984)’s calculus with structural subtyping (similar to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$)
and showed that they cannot be encoded in each other by examples. Pottier
(1998) conveyed the intuition that row polymorphism can lessen the need for
subtyping to some extent, but there are still situations where subtyping are
necessary, e.g., the reuse of $\lambda$-bound variables which cannot be
polymorphic given only rank-1 polymorphism.

#### Disjoint polymorphism.

Disjoint intersection types (d. S. Oliveira et al., 2016) generalise record
types. Record concatenation and restriction (Cardelli and Mitchell, 1991) are
replaced by a merge operator (Dunfield, 2014) and a type difference operator
(Xu et al., 2023), respectively. Parametric polymorphism of disjoint
intersection types is supported via disjoint polymorphism (Alpuim et al.,
2017) where type variables are associated with disjointness constraints.
Similarly to our work, Xie et al. (2020) formally prove that both row
polymorphism and bounded quantification of record types can be encoded in
terms of disjoint polymorphism.

###  7.4. Conclusion and Future Work

We carried out a formal and systematic study of the encoding of structural
subtyping as parametric polymorphism. To better reveal the relative expressive
power of these two type system features, we introduced the notion of type-only
translations to avoid the influence of non-trivial term reconstruction. We
gave type-only translations from various calculi with subtyping to calculi
with different kinds of polymorphism and proved their correctness; we also
proved a series of non-existence results. Our results provide a precise
characterisation of the long-standing folklore intuition that row polymorphism
can often replace subtyping. Additionally, they offer insight into the trade-
offs between subtyping and polymorphism in the design of programming
languages.

In future, we would like to explore whether it might be possible to extend our
encodings relying on type inference to systems supporting higher-rank
polymorphism, such as FreezeML (Emrich et al., 2020). We would also like to
consider other styles of row typing such as those based on scoped labels
(Leijen, 2005) and Rose (Morris and McKinna, 2019). In addition to variant and
record types, row types are also the foundation for various effect type
systems, e.g. for effect handlers (Hillerström and Lindley, 2016; Leijen,
2017). It would be interesting to investigate to what extent our approach can
be applied to effect typing. Aside from studying the relationship between
subtyping and row and presence polymorphism we would also like to study the
ergonomics of these programming language features in practice, especially
their compatibility with others such as algebraic data types.

###### Acknowledgements.

This work was supported by the UKRI Future Leaders Fellowship “Effect Handler
Oriented Programming” (reference number MR/T043830/1) and ERC Consolidator
Grant no. 682315 (Skye).

## References

  * (1)
  * Alpuim et al. (2017) João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017.  Disjoint Polymorphism. In _Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings_ _(Lecture Notes in Computer Science, Vol. 10201)_ , Hongseok Yang (Ed.). Springer, 1–28.  https://doi.org/10.1007/978-3-662-54434-1_1
  * Birtwistle et al. (1979) Graham M. Birtwistle, Ole-Johan Dahl, Bjorn Myhrhaug, and Kristen Nygaard. 1979.  Simula Begin.  Studentlitteratur (Lund, Sweden), Bratt Institut fuer nues Lernen (Goch, FRG), Charwell-Bratt Ltd (Kent, England).
  * Blume et al. (2006) Matthias Blume, Umut A. Acar, and Wonseok Chae. 2006\.  Extensible programming with first-class cases. In _ICFP_. ACM, 239–250.
  * Breazu-Tannen et al. (1991) Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. 1991.  Inheritance as implicit coercion.  _Information and Computation_ 93, 1 (1991), 172–221.  https://doi.org/10.1016/0890-5401(91)90055-7 Selections from 1989 IEEE Symposium on Logic in Computer Science.
  * Breazu-Tannen et al. (1990) Val Breazu-Tannen, Carl A. Gunter, and Andre Scedrov. 1990\.  Computing with Coercions. In _Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP 1990, Nice, France, 27-29 June 1990_ , Gilles Kahn (Ed.). ACM, 44–60.  https://doi.org/10.1145/91556.91590
  * Cardelli (1984) Luca Cardelli. 1984\.  A Semantics of Multiple Inheritance. In _Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings_ _(Lecture Notes in Computer Science, Vol. 173)_ , Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin (Eds.). Springer, 51–67.  https://doi.org/10.1007/3-540-13346-1_2
  * Cardelli (1988) Luca Cardelli. 1988\.  Structural Subtyping and the Notion of Power Type. In _POPL_. ACM Press, 70–79.
  * Cardelli et al. (1994) Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1994.  An Extension of System F with Subtyping.  _Inf. Comput._ 109, 1/2 (1994), 4–56.  https://doi.org/10.1006/inco.1994.1013
  * Cardelli and Mitchell (1991) Luca Cardelli and John C. Mitchell. 1991.  Operations on Records.  _Math. Struct. Comput. Sci._ 1, 1 (1991), 3–48.  https://doi.org/10.1017/S0960129500000049
  * Cardelli and Wegner (1985) Luca Cardelli and Peter Wegner. 1985.  On Understanding Types, Data Abstraction, and Polymorphism.  _ACM Comput. Surv._ 17, 4 (1985), 471–522.  https://doi.org/10.1145/6041.6042
  * Church (1940) Alonzo Church. 1940\.  A Formulation of the Simple Theory of Types.  _J. Symb. Log._ 5, 2 (1940), 56–68.
  * d. S. Oliveira et al. (2016) Bruno C. d. S. Oliveira, Zhiyuan Shi, and João Alpuim. 2016\.  Disjoint intersection types. In _Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016_ , Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 364–377.  https://doi.org/10.1145/2951913.2951945
  * Damas and Milner (1982) Luis Damas and Robin Milner. 1982.  Principal Type-Schemes for Functional Programs. In _Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Albuquerque, New Mexico) _(POPL ’82)_. Association for Computing Machinery, New York, NY, USA, 207–212.  https://doi.org/10.1145/582153.582176
  * Dolan (2016) Stephen Dolan. 2016\.  _Algebraic Subtyping_.  Ph. D. Dissertation. Computer Laboratory, University of Cambridge, United Kingdom.
  * Dolan and Mycroft (2017) Stephen Dolan and Alan Mycroft. 2017.  Polymorphism, subtyping, and type inference in MLsub. In _POPL_. ACM, 60–72.
  * Dunfield (2014) Jana Dunfield. 2014\.  Elaborating intersection and union types.  _J. Funct. Program._ 24, 2-3 (2014), 133–165.  https://doi.org/10.1017/S0956796813000270
  * Emrich et al. (2020) Frank Emrich, Sam Lindley, Jan Stolarek, James Cheney, and Jonathan Coates. 2020.  FreezeML: Complete and Easy Type Inference for First-Class Polymorphism. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ (London, UK) _(PLDI 2020)_. Association for Computing Machinery, New York, NY, USA, 423–437.  https://doi.org/10.1145/3385412.3386003
  * Felleisen (1991) Matthias Felleisen. 1991\.  On the Expressive Power of Programming Languages.  _Sci. Comput. Program._ 17, 1-3 (1991), 35–75.  Revised version.
  * Gaster (1998) Benedict R Gaster. 1998\.  _Records, variants and qualified types_.  Ph. D. Dissertation. University of Nottingham.
  * Gaster and Jones (1996) Benedict R Gaster and Mark P Jones. 1996.  _A polymorphic type system for extensible records and variants_.  Technical Report. Technical Report NOTTCS-TR-96-3, Department of Computer Science, University ….
  * Girard (1972) Jean-Yves Girard. 1972\.  _Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur_.  Ph. D. Dissertation. Université Paris 7, France.
  * Harper and Pierce (1990) Robert William Harper and Benjamin C. Pierce. 1990.  Extensible records without subsumption.  (2 1990).  https://doi.org/10.1184/R1/6605507.v1
  * Hillerström and Lindley (2016) Daniel Hillerström and Sam Lindley. 2016.  Liberating effects with rows and handlers. In _TyDe@ICFP_. ACM, 15–27.
  * Leijen (2005) Daan Leijen. 2005\.  Extensible records with scoped labels. In _Proceedings of the 2005 Symposium on Trends in Functional Programming (TFP’05), Tallinn, Estonia_.  https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/
  * Leijen (2017) Daan Leijen. 2017\.  Type directed compilation of row-typed algebraic effects. In _Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017_ , Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 486–499.  https://doi.org/10.1145/3009837.3009872
  * Morris and McKinna (2019) J. Garrett Morris and James McKinna. 2019.  Abstracting extensible data types: or, rows by any other name.  _Proc. ACM Program. Lang._ 3, POPL (2019), 12:1–12:28.
  * Parreaux and Chau (2022) Lionel Parreaux and Chun Yin Chau. 2022.  MLstruct: principal type inference in a Boolean algebra of structural types.  _Proc. ACM Program. Lang._ 6, OOPSLA2 (2022), 449–478.  https://doi.org/10.1145/3563304
  * Pierce (2002) Benjamin C. Pierce. 2002\.  _Types and programming languages_.  MIT Press.
  * Pottier (1998) François Pottier. 1998\.  _Type Inference in the Presence of Subtyping: from Theory to Practice_.  Research Report RR-3483. INRIA.  https://hal.inria.fr/inria-00073205
  * Pottier (2001) François Pottier. 2001\.  Simplifying Subtyping Constraints: A Theory.  _Inf. Comput._ 170, 2 (2001), 153–183.  https://doi.org/10.1006/inco.2001.2963
  * Pottier and Rémy (2004) François Pottier and Didier Rémy. 2004.  The Essence of ML Type Inference.  In _Advanced Topics in Types and Programming Languages_ , Benjamin C. Pierce (Ed.). The MIT Press, Chapter 10, 460–489.  https://doi.org/10.7551/mitpress/1104.003.0016
  * Rémy (1989) Didier Rémy. 1989\.  Typechecking Records and Variants in a Natural Extension of ML. In _Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989_. ACM Press, 77–88.  https://doi.org/10.1145/75277.75284
  * Rémy (1994) Didier Rémy. 1994\.  _Type Inference for Records in Natural Extension of ML_.  MIT Press, Cambridge, MA, USA, 67–95.
  * Reynolds (1974) John C. Reynolds. 1974\.  Towards a theory of type structure. In _Symposium on Programming_ _(LNCS, Vol. 19)_. Springer, 408–423.
  * Reynolds (1980) John C. Reynolds. 1980\.  Using category theory to design implicit conversions and generic operators. In _Semantics-Directed Compiler Generation_ _(Lecture Notes in Computer Science, Vol. 94)_. Springer, 211–258.
  * Trifonov and Smith (1996) Valery Trifonov and Scott F. Smith. 1996.  Subtyping Constrained Types. In _Static Analysis, Third International Symposium, SAS’96, Aachen, Germany, September 24-26, 1996, Proceedings_ _(Lecture Notes in Computer Science, Vol. 1145)_ , Radhia Cousot and David A. Schmidt (Eds.). Springer, 349–365.  https://doi.org/10.1007/3-540-61739-6_52
  * Wand (1987) Mitchell Wand. 1987\.  Complete Type Inference for Simple Objects. In _LICS_. IEEE Computer Society, 37–44.
  * Xie et al. (2020) Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers. 2020.  Row and Bounded Polymorphism via Disjoint Polymorphism. In _34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference)_ _(LIPIcs, Vol. 166)_ , Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 27:1–27:30.  https://doi.org/10.4230/LIPIcs.ECOOP.2020.27
  * Xu et al. (2023) Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira. 2023\.  Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations.  _Proc. ACM Program. Lang._ 7, POPL (2023), 893–920.  https://doi.org/10.1145/3571224

##  Appendix A More Calculi

In this section, we elaborate on calculi that are not fully detailed in the
body of the paper.

###  A.1. A Calculus with Row Polymorphic Records
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}$

The extensions to the syntax, static semantics, and dynamic semantics of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$ for a calculus with
row polymorphic records are shown in LABEL:fig:stlcrecrow. Actually, they are
exactly the same as the extensions to
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ for
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$ in LABEL:fig:var-calc-row.

###  A.2. A Calculus with Presence Polymorphic Variants
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}$

The extensions and modifications to the syntax, static semantics, and dynamic
semantics of $\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$ for a calculus with
presence polymorphic variants
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\theta}$ are shown in
LABEL:fig:stlcvarpre.

One thing worth noting is that in $\mathsf{T\textrm{-}Case}$, we do not
require all labels in the type of $M$ to be present, which is dual to the
$\mathsf{T\textrm{-}Record}$ rule in LABEL:fig:rec-calc-pre. It does not loss
any generality as our equivalence relation between rows only considers present
labels.

###  A.3. A Calculus with Rank-1 Row Polymorphic Records
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$

The extensions to the syntax, static semantics, and dynamic semantics for
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$, a calculus
with records and rank-1 row polymorphism are shown in LABEL:fig:rec-calc-
prenex. For the type syntax, we introduce row variables and type schemes. For
the term syntax, we drop the type annotation on $\lambda$ abstractions, and
add the $\mathbf{let}$ syntax for polymorphism. We only give the declarative
typing rules, as the syntax-directed typing rules and type inference are just
standard (Damas and Milner, 1982). Notice that we do not introduce type
variables for values in type schemes for simplicity. The lack of principal
types is fine here as we are working with declarative typing rules. It is easy
to regain principal types by adding value type variables.

##  Appendix B Proofs of Encodings in Section 4

In this section, we show the proofs of type preservation and operational
correspondence for all the four translations in Section 4.

###  B.1. Proof of the Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}$

###### Lemma B.1 (Translation commutes with substitution).

If $\Delta;\Gamma,x:A\vdash M:B$ and $\Delta;\Gamma\vdash N:A$, then
$\llbracket M[N/x]\rrbracket=\llbracket M\rrbracket[\llbracket
N\rrbracket/x]$.

###### Proof.

By straightforward induction on $M$.

$x$:

$\llbracket x[N/x]\rrbracket=\llbracket N\rrbracket=\llbracket
x\rrbracket[\llbracket N\rrbracket/x]$.

$y(y\neq x)$:

$\llbracket y[N/x]\rrbracket=y=\llbracket y\rrbracket[\llbracket
N\rrbracket/x]$

$M_{1}\,M_{2}$:

Our goal follows from IH and definition of substitution.

$(\ell\,M^{\prime})^{A}$:

Our goal follows from IH and definition of substitution.

$\mathbf{case}\,M^{\prime}\,\\{\ell_{i}\,x_{i}\mapsto N_{i}\\}_{i}$:

Our goal follows from IH and definition of substitution.

$M^{\prime}\vartriangleright A$:

By IH and definition of substitution, we have
$\llbracket(M^{[\ell_{i}:A_{i}]_{i}}\vartriangleright[R])[N/x]\rrbracket=\llbracket
M^{[\ell_{i}:A_{i}]_{i}}[N/x]\vartriangleright[R]\rrbracket=\mathbf{case}~{}\llbracket
M[N/x]\rrbracket~{}\\{\ell_{i}~{}x_{i}\mapsto(\ell_{i}~{}x_{i})^{[R]}\\}_{i}=\mathbf{case}~{}\llbracket
M\rrbracket[\llbracket
N\rrbracket/x]~{}\\{\ell_{i}~{}x_{i}\mapsto(\ell_{i}~{}x_{i})^{[R]}\\}_{i}=(\mathbf{case}~{}\llbracket
M\rrbracket~{}\\{\ell_{i}~{}x_{i}\mapsto(\ell_{i}~{}x_{i})^{[R]}\\}_{i})[\llbracket
N\rrbracket/x]=\llbracket
M^{[\ell_{i}:A_{i}]_{i}}\vartriangleright[R]\rrbracket[\llbracket
N\rrbracket/x]$.

∎

See 4.1

###### Proof.

By straightforward induction on typing derivations.

$\mathsf{T\textrm{-}Var}$:

Our goal follows from $\llbracket x\rrbracket=x$ and
$\mathsf{T\textrm{-}Var}$.

$\mathsf{T\textrm{-}Lam}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Lam}$.

$\mathsf{T\textrm{-}App}$:

Our goal follows from IH and $\mathsf{T\textrm{-}App}$.

$\mathsf{T\textrm{-}Inject}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Inject}$.

$\mathsf{T\textrm{-}Case}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Case}$.

$\mathsf{T\textrm{-}Upcast}$:

The only subtyping relation in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ is for variant types.
Given $\Delta;\Gamma\vdash M^{[R]}\vartriangleright[R^{\prime}]:[R^{\prime}]$,
by $\Delta;\Gamma\vdash M:[R]$ and IH we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:[R]$. Then, supposing $R=(\ell_{i}:A_{i})_{i}$, by definition of
translation, $[R]\leqslant[R^{\prime}]$ and $\mathsf{T\textrm{-}Case}$ we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\mathbf{case}~{}\llbracket
M\rrbracket~{}\\{\ell_{i}~{}x_{i}\mapsto(\ell_{i}~{}x_{i})^{[R^{\prime}]}\\}_{i}:[R^{\prime}]$.

∎

See 4.2

###### Proof.

Simulation: First, we prove the base case that the whole term $M$ is reduced,
i.e. $M\leadsto_{\beta\vartriangleright}N$ implies $\llbracket
M\rrbracket\leadsto_{\beta}\llbracket N\rrbracket$. The proof proceeds by case
analysis on the reduction relation:

$\mathsf{\beta\textrm{-}Lam}$:

We have $(\lambda x^{A}.M_{1})\,M_{2}\leadsto_{\beta}M_{1}[M_{2}/x]$. Then,
(1)$\llbracket(\lambda x^{A}.M_{1})\,M_{2}\rrbracket=(\lambda x^{A}.\llbracket
M_{1}\rrbracket)\ \llbracket M_{2}\rrbracket\leadsto_{\beta}\llbracket
M_{1}\rrbracket[\llbracket M_{2}\rrbracket/x]=\llbracket
M_{1}[M_{2}/x]\rrbracket$, where the last equation follows from Lemma B.1.

$\mathsf{\beta\textrm{-}Case}$:

We have $\mathbf{case}~{}M^{\prime}~{}\\{\ell_{i}\,x_{i}\mapsto
N_{i}\\}_{i}\leadsto_{\beta}N_{j}[M_{j}/x_{j}]$. Similar to the
$\mathsf{\beta\textrm{-}Lam}$ case.

$\mathsf{\vartriangleright\\!\\!\textrm{-}Upcast}$:

We have $(\ell\,M_{1})^{[R]}\vartriangleright
A\leadsto_{\vartriangleright}(\ell\,M_{1})^{A}$. Supposing
$R=(\ell_{i}:A_{i})_{i}$, we have
(2)$\llbracket(\ell\,M_{1})^{[R]}\vartriangleright A\rrbracket=\mathbf{case}\
(\ell\,\llbracket M_{1}\rrbracket)^{[R]}\
\\{\ell_{i}\,x_{i}\mapsto(\ell_{i}\,x_{i})^{A}\\}_{i}\leadsto_{\beta}(\ell\,\llbracket
M_{1}\rrbracket)^{A}=\llbracket(\ell\,M_{1})^{A}\rrbracket$.

Then, we prove the full theorem by induction on $M$. We only need to prove the
case where reduction happens in sub-terms of $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

The reduction can only happen in $M^{\prime}$. Supposing $\lambda
x^{A}.M^{\prime}\rightsquigarrow_{\beta\vartriangleright}\lambda
x^{A}.N^{\prime}$, by IH on $M^{\prime}$, we have $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\beta}\llbracket N^{\prime}\rrbracket$,
which then gives $\llbracket\lambda x^{A}.M^{\prime}\rrbracket=\lambda
x^{A}.\llbracket M^{\prime}\rrbracket\rightsquigarrow_{\beta}\lambda
x^{A}.\llbracket N^{\prime}\rrbracket=\llbracket\lambda
x^{A}.N^{\prime}\rrbracket$.

$M_{1}\,M_{2}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen
either in $M_{1}$ or $M_{2}$.

$(\ell\,M^{\prime})^{A}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

$\mathbf{case}~{}M^{\prime}~{}\\{\ell_{i}\,x_{i}\mapsto N_{i}\\}_{i}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$ or one of $(N_{i})_{i}$.

$M^{\prime}\vartriangleright A$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

Reflection: First, we prove the base case that the whole term $\llbracket
M\rrbracket$ is reduced, i.e. $\llbracket
M\rrbracket\leadsto_{\beta}\llbracket N\rrbracket$ implies
$M\leadsto_{\beta\vartriangleright}N$. The proof proceeds by case analysis on
the reduction relation:

$\mathsf{\beta\textrm{-}Lam}$:

By definition of translation, there exists $M_{1}$ and $M_{2}$ such that
$M=(\lambda x^{A}.M_{1})\ M_{2}$. Our goal follows from  (1) and $M=(\lambda
x^{A}.M_{1})\ M_{2}\leadsto_{\beta}M_{1}[M_{2}/x]$.

$\mathsf{\beta\textrm{-}Case}$:

By definition of translation, the top-level syntax construct of $M$ can either
be $\mathbf{case}$ or upcast. Proceed by a case analysis:

  * •:

$M=\mathbf{case}~{}(\ell_{j}\,M_{j})^{[R]}~{}\\{\ell_{i}\,x_{i}\mapsto
N_{i}\\}_{i}$ where $R=(\ell_{i}:A_{i})_{i}$. Similar to the
$\mathsf{\beta\textrm{-}Lam}$ case.

  * •:

$M=(\ell\,M_{1})^{[R]}\vartriangleright A$ where $R=(\ell_{i}:A_{i})_{i}$. Our
goal follows from  (2) and $(\ell\,M_{1})^{[R]}\vartriangleright
A\leadsto_{\vartriangleright}(\ell\,M_{1})^{A}$.

Then, we prove the full theorem by induction on $M$. We only need to prove the
case where reduction happens in sub-terms of $\llbracket M\rrbracket$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

By definition of translation, there exists $N^{\prime}$ such that $N=\lambda
x^{A}.N^{\prime}$ and $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\beta}\llbracket N^{\prime}\rrbracket$.
By IH, we have
$M^{\prime}\rightsquigarrow_{\beta\vartriangleright}N^{\prime}$, which then
implies $\lambda
x^{A}.M^{\prime}\rightsquigarrow_{\beta\vartriangleright}\lambda
x^{A}.N^{\prime}$.

$M_{1}\,M_{2}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen
either in $\llbracket M_{1}\rrbracket$ or $\llbracket M_{2}\rrbracket$.

$(\ell\,M^{\prime})^{A}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$\llbracket M^{\prime}\rrbracket$.

$\mathbf{case}~{}M^{\prime}~{}\\{\ell_{i}\,x_{i}\mapsto N_{i}\\}_{i}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$\llbracket M^{\prime}\rrbracket$ or one of $(\llbracket
N_{i}\rrbracket)_{i}$.

$M^{\prime}\vartriangleright A$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$\llbracket M^{\prime}\rrbracket$.

∎

###  B.2. Proof of the Encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\rho}$

###### Lemma B.2 (Translation commutes with substitution).

If $\Delta;\Gamma,x:A\vdash M:B$ and $\Delta;\Gamma\vdash N:A$, then
$\llbracket M[N/x]\rrbracket=\llbracket M\rrbracket[\llbracket
N\rrbracket/x]$.

###### Proof.

By straightforward induction on $M$. Only consider cases that are different
from the proof of Lemma B.1.

$(\ell\,M^{\prime})^{[R]}$:

By IH and definition of substitution, we have

$\begin{array}[]{ll}&\llbracket(\ell\,M)^{[R]}[N/x]\rrbracket\\\
=&\llbracket(\ell\,M[N/x])^{[R]}\rrbracket\\\
=&\Lambda\rho^{\mathsf{Row}_{R}}.(\ell\,\llbracket
M[N/x]\rrbracket)^{[\llbracket R\rrbracket;\rho]}\\\
=&\Lambda\rho^{\mathsf{Row}_{R}}.(\ell\,\llbracket M\rrbracket[\llbracket
N\rrbracket/x])^{[\llbracket R\rrbracket;\rho]}\\\
=&(\Lambda\rho^{\mathsf{Row}_{R}}.(\ell\,\llbracket M\rrbracket)^{[\llbracket
R\rrbracket;\rho]})[\llbracket N\rrbracket/x]\\\
=&\llbracket(\ell\,M)^{[R]}\rrbracket[\llbracket N\rrbracket/x]\end{array}$

$\mathbf{case}\,M^{\prime}\,\\{\ell_{i}\,x_{i}\mapsto N_{i}\\}_{i}$:

By an equational reasoning similar to the case of $(\ell\,M^{\prime})^{[R]}$.

$M^{\prime}\vartriangleright A$:

By an equational reasoning similar to the case of $(\ell\,M^{\prime})^{[R]}$.

∎

See 4.3

###### Proof.

By induction on typing derivations.

$\mathsf{T\textrm{-}Var}$:

Our goal follows from $\llbracket x\rrbracket=x$.

$\mathsf{T\textrm{-}Lam}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Lam}$.

$\mathsf{T\textrm{-}App}$:

Our goal follows from IH and $\mathsf{T\textrm{-}App}$.

$\mathsf{T\textrm{-}Inject}$:

By definition we have $(l:A)\in R$ implies $(l:\llbracket
A\rrbracket)\in\llbracket R\rrbracket\rho$ for any $\rho$. Then our goal
follows from IH, $\mathsf{T\textrm{-}Inject}$ and
$\mathsf{T\textrm{-}RowLam}$.

$\mathsf{T\textrm{-}Case}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Case}$.

$\mathsf{T\textrm{-}Upcast}$:

The only subtyping relation in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}}^{\leqslant}$ is for variant types.
Given $\Delta;\Gamma\vdash M^{[R]}\vartriangleright[R^{\prime}]:[R^{\prime}]$,
by $\Delta;\Gamma\vdash M:[R]$ and IH we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket[R]\rrbracket$. Then, by definition of translation and
$\mathsf{T\textrm{-}RowApp}$ we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M^{[R]}\vartriangleright[R^{\prime}]\rrbracket:\llbracket[R^{\prime}]\rrbracket$.

∎

See 4.4

###### Proof.

Simulation: First, we prove the base case where the whole term $M$ is reduced,
i.e. $M\leadsto_{\beta}N$ implies $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{?}\rightsquigarrow_{\beta}\llbracket
N\rrbracket$, and $M\leadsto_{\vartriangleright}N$ implies $\llbracket
M\rrbracket\rightsquigarrow_{\nu}\llbracket N\rrbracket$. The proof proceeds
by case analysis on the reduction relation:

$\mathsf{\beta\textrm{-}Lam}$:

We have $(\lambda x^{A}.M_{1})\,M_{2}\leadsto_{\beta}M_{1}[M_{2}/x]$. Then,
(1)$\llbracket(\lambda x^{A}.M_{1})\,M_{2}\rrbracket=(\lambda x^{A}.\llbracket
M_{1}\rrbracket)\ \llbracket M_{2}\rrbracket\leadsto_{\beta}\llbracket
M_{1}\rrbracket[\llbracket M_{2}\rrbracket/x]=\llbracket
M_{1}[M_{2}/x]\rrbracket$, where the last equation follows from Lemma B.2.

$\mathsf{\beta\textrm{-}Case}$:

We have $\mathbf{case}\ (\ell_{j}\,M_{j})^{[R]}\ \\{\ell_{i}\ x_{i}\mapsto
N_{i}\\}\leadsto_{\beta}N_{j}[M_{j}/x_{j}]$. Supposing
$R=(\ell_{i}:A_{i})_{i}$, we have  (2)$\llbracket\mathbf{case}\
(\ell_{j}\,M_{j})^{[R]}\ \\{\ell_{i}\ x_{i}\mapsto
N_{i}\\}\rrbracket=\mathbf{case}\
(\llbracket(\ell_{j}\,M_{j})^{[R]}\rrbracket\,{\cdot})\ \\{\ell_{i}\
x_{i}\mapsto\llbracket N_{i}\rrbracket\\}\rightsquigarrow_{\tau}\mathbf{case}\
((\ell_{j}\,\llbracket M_{j}\rrbracket)^{[\llbracket R\rrbracket]})\
\\{\ell_{i}\ x_{i}\mapsto\llbracket
N_{i}\rrbracket\\}\leadsto_{\beta}\llbracket N_{j}\rrbracket[\llbracket
M_{j}\rrbracket/x_{j}]=\llbracket N_{j}[M_{j}/x_{j}]\rrbracket$, where the
last equation follows from Lemma B.2.

$\mathsf{\vartriangleright\\!\\!\textrm{-}Upcast}$:

We have
$(\ell\,M_{1})^{[R]}\vartriangleright[R^{\prime}]\leadsto_{\vartriangleright}(\ell\,M_{1})^{[R^{\prime}]}$.
We have
(3)$\llbracket(\ell\,M_{1})^{[R]}\vartriangleright[R^{\prime}]\rrbracket=$
$\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.\llbracket(\ell\,M_{1})^{[R]}\rrbracket@\,(\llbracket
R^{\prime}\backslash
R\rrbracket;\rho)\rightsquigarrow_{\nu}\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.(\ell\,M_{1})^{[\llbracket
R^{\prime}\rrbracket;\rho]}=\llbracket(\ell\,M_{1})^{[R^{\prime}]}\rrbracket$.

Then, we prove the full theorem by induction on $M$. We only need to prove the
case where reduction happens in sub-terms of $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

The reduction can only happen in $M^{\prime}$. Supposing $\lambda
x^{A}.M^{\prime}\rightsquigarrow_{\beta}\lambda x^{A}.N^{\prime}$, by IH on
$M^{\prime}$, we have $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\tau}^{?}\rightsquigarrow_{\beta}\llbracket
N^{\prime}\rrbracket$, which then gives $\llbracket\lambda
x^{A}.M^{\prime}\rrbracket=\lambda x^{A}.\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\tau}^{?}\rightsquigarrow_{\beta}\lambda
x^{A}.\llbracket N^{\prime}\rrbracket=\llbracket\lambda
x^{A}.N^{\prime}\rrbracket$. The same applies to the second case of the
theorem.

$(\ell\,M^{\prime})^{[R]}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

$M_{1}\ M_{2}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen
either in $M_{1}$ or $M_{2}$.

$\mathbf{case}~{}M^{\prime}~{}\\{\ell_{i}\,x_{i}\mapsto N_{i}\\}_{i}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$ or one of $(N_{i})_{i}$.

$M^{\prime}\vartriangleright A$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

Reflection: We proceed by induction on $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

We have $\llbracket M\rrbracket=\lambda x^{\llbracket A\rrbracket}.\llbracket
M^{\prime}\rrbracket$. The reduction can only happen in $\llbracket
M^{\prime}\rrbracket$. By definition of translation, there exists $N^{\prime}$
such that $N=\lambda x^{A}.N^{\prime}$ and $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\tau}^{?}\rightsquigarrow_{\beta}\llbracket
N^{\prime}\rrbracket$. By IH, we have
$M^{\prime}\rightsquigarrow_{\beta}N^{\prime}$, which then implies
$M\rightsquigarrow_{\beta}N$. The same applies to the second case of the
theorem.

$M_{1}\ M_{2}$:

We have $\llbracket M\rrbracket=\llbracket M_{1}\rrbracket\ \llbracket
M_{2}\rrbracket$. Proceed by case analysis where the first step of reduction
happens.

  * •:

Reduction happens in either $\llbracket M_{1}\rrbracket$ or $\llbracket
M_{2}\rrbracket$. Similar to the $\lambda x^{A}.M^{\prime}$ case.

  * •:

The application is reduced by $\mathsf{\beta\textrm{-}Lam}$. By definition of
translation, we have $M_{1}=\lambda x^{A}.M^{\prime}$. By  (1), we have
$\llbracket M\rrbracket\leadsto_{\beta}\llbracket
M^{\prime}[M_{2}/x]\rrbracket$, which then gives $N=M^{\prime}[M_{2}/x]$. Our
goal follows from $M\leadsto_{\beta}N$.

$(\ell\,M^{\prime})^{[R]}$:

We have $\llbracket
M\rrbracket=\Lambda\rho^{\mathsf{Row}_{R}}.(\ell\,\llbracket
M^{\prime}\rrbracket)^{[\llbracket R\rrbracket;\rho]}$. Similar to the
$\lambda x^{A}.M^{\prime}$ case as the reduction can only happen in
$\llbracket M^{\prime}\rrbracket$.

$\mathbf{case}~{}M^{\prime}~{}\\{\ell_{i}\,x_{i}\mapsto N_{i}\\}_{i}$:

We have $\llbracket M\rrbracket=\mathbf{case}~{}(\llbracket
M^{\prime}\rrbracket\,{\cdot})~{}\\{\ell_{i}~{}x_{i}\mapsto\llbracket
N_{i}\rrbracket\\}_{i}$. Proceed by case analysis where the first step of
reduction happens.

  * •:

Reduction happens in $\llbracket M^{\prime}\rrbracket$ or one of $\llbracket
N_{i}\rrbracket$. Similar to the $\lambda x^{A}.M^{\prime}$ case.

  * •:

The row type application $\llbracket M^{\prime}\rrbracket\,{\cdot}$ is reduced
by $\mathsf{\tau\textrm{-}RowLam}$. Supposing $\llbracket
M\rrbracket\rightsquigarrow_{\tau}N^{\prime}$, by the definition of
translation, because $\llbracket N\rrbracket$ must be in the codomain of the
translation, we can only have $N^{\prime}\leadsto_{\beta}\llbracket
N\rrbracket$ by applying $\mathsf{\beta\textrm{-}Case}$, which implies
$M^{\prime}=(\ell_{j}\,M_{j})^{[R]}$. By  (2), we have $\llbracket
M\rrbracket\rightsquigarrow_{\tau}\leadsto_{\beta}\llbracket
N_{j}[M_{j}/x_{j}]\rrbracket$, which then gives us $N=N_{j}[M_{j}/x_{j}]$. Our
goal follows from $M\leadsto_{\beta}N$.

$M^{\prime[R]}\vartriangleright[R^{\prime}]$:

We have $\llbracket
M\rrbracket=\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.\llbracket
M^{\prime}\rrbracket\,(\llbracket R^{\prime}\backslash R\rrbracket;\rho)$.
Proceed by case analysis where the first step of reduction happens.

  * •:

Reduction happens in $\llbracket M^{\prime}\rrbracket$. Similar to the
$\lambda x^{A}.M^{\prime}$ case.

  * •:

The row type application $\llbracket M^{\prime}\rrbracket\,(\llbracket
R^{\prime}\backslash R\rrbracket;\rho)$ is reduced by
$\mathsf{\tau\textrm{-}RowLam}$. Because $\llbracket M^{\prime}\rrbracket$
should be a type abstraction, there are only two cases. Proceed by case
analysis on $M^{\prime}$.

    * –:

$M^{\prime}=(\ell\,M_{1})^{[R]}$. By  (3), we have $\llbracket
M\rrbracket\rightsquigarrow_{\beta}\llbracket(\ell\,M_{1})^{[R^{\prime}]}\rrbracket$,
which then gives us $N={(\ell\,M_{1})^{[R^{\prime}]}}$. Our goal follows from
$M\rightsquigarrow_{\beta}N$.

    * –:

$M^{\prime}=M_{1}^{[R_{1}]}\vartriangleright[R]$. We have

$\begin{array}[]{ll}\llbracket
M\rrbracket&=\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.\llbracket
M_{1}^{[R_{1}]}\vartriangleright[R]\rrbracket\,(\llbracket
R^{\prime}\backslash R\rrbracket;\rho)\\\
&=\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.(\Lambda\rho^{\mathsf{Row}_{R}}.\llbracket
M_{1}\rrbracket@\,(\llbracket R\backslash R_{1}\rrbracket;\rho))@\,(\llbracket
R^{\prime}\backslash R\rrbracket;\rho)\\\
&\rightsquigarrow_{\nu}\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.\llbracket
M_{1}\rrbracket@\,(\llbracket R\backslash R_{1}\rrbracket;\llbracket
R^{\prime}\backslash R\rrbracket;\rho)\\\
&=\Lambda\rho^{\mathsf{Row}_{R^{\prime}}}.\llbracket
M_{1}\rrbracket@\,(\llbracket R^{\prime}\backslash R_{1}\rrbracket;\rho)\\\
&=\llbracket
M_{1}^{[R_{1}]}\vartriangleright[R^{\prime}]\rrbracket\end{array}$

By the definition of translation, we know that
$N={M_{1}^{[R_{1}]}\vartriangleright[R^{\prime}]}$. Our goal follows from
$M\rightsquigarrow_{\blacktriangleright}N$.

∎

###  B.3. Proof of the Encoding
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$

###### Lemma B.3 (Translation commutes with substitution).

If $\Delta;\Gamma,x:A\vdash M:B$ and $\Delta;\Gamma\vdash N:A$, then
$\llbracket M[N/x]\rrbracket=\llbracket M\rrbracket[\llbracket
N\rrbracket/x]$.

###### Proof.

By straightforward induction on $M$.

$x$:

$\llbracket x[N/x]\rrbracket=\llbracket N\rrbracket=\llbracket
x\rrbracket[\llbracket N\rrbracket/x]$.

$y(y\neq x)$:

$\llbracket y[N/x]\rrbracket=y=\llbracket y\rrbracket[\llbracket
N\rrbracket/x]$

$M_{1}\,M_{2}$:

Our goal follows from IH and definition of substitution.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

Our goal follows from IH and definition of substitution.

$M^{\prime}.\ell$:

Our goal follows from IH and definition of substitution.

$M^{\prime}\vartriangleright A$:

By IH and definition of substitution, we have

$\begin{array}[]{ll}&\llbracket(M^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i})[N/x]\rrbracket\\\
=&\llbracket
M^{\prime}[N/x]\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket\\\
=&\langle\ell_{i}=\llbracket M^{\prime}[N/x]\rrbracket.\ell_{i}\rangle_{i}\\\
=&\langle\ell_{i}=\llbracket M^{\prime}\rrbracket[\llbracket
N\rrbracket/x].\ell_{i}\rangle_{i}\\\ =&(\langle\ell_{i}=\llbracket
M^{\prime}\rrbracket.\ell_{i}\rangle_{i})[\llbracket N\rrbracket/x]\\\
=&\llbracket
M^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket[\llbracket
N\rrbracket/x]\end{array}$

∎

See 4.5

###### Proof.

By straightforward induction on typing derivations.

$\mathsf{T\textrm{-}Var}$:

Our goal follows from $\llbracket x\rrbracket=x$ and
$\mathsf{T\textrm{-}Var}$.

$\mathsf{T\textrm{-}Lam}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Lam}$.

$\mathsf{T\textrm{-}App}$:

Our goal follows from IH and $\mathsf{T\textrm{-}App}$.

$\mathsf{T\textrm{-}Record}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Record}$.

$\mathsf{T\textrm{-}Project}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Project}$.

$\mathsf{T\textrm{-}Upcast}$:

The only subtyping relation in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ is for
record types. Given $\Delta;\Gamma\vdash M\vartriangleright\langle
R^{\prime}\rangle:\langle R^{\prime}\rangle$ and $\Delta;\Gamma\vdash
M:\langle R\rangle$, by IH we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\langle R\rangle$. Then, supposing
$M=\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}$ and
$R^{\prime}=(\ell_{j}^{\prime}:A_{j})_{j}$, by definition of translation,
$\langle R\rangle\leqslant\langle R^{\prime}\rangle$ and
$\mathsf{T\textrm{-}Record}$ we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\langle\ell_{j}^{\prime}=M_{\ell_{j}^{\prime}}\rangle_{j}:\langle
R^{\prime}\rangle$.

∎

See 4.6

###### Proof.

Simulation:

First, we prove the base case that the whole term $M$ is reduced, i.e.
$M\leadsto_{\beta\vartriangleright}N$ implies $\llbracket
M\rrbracket\leadsto_{\beta}^{\ast}\llbracket N\rrbracket$. The proof proceeds
by case analysis on the reduction relation.

$\mathsf{\beta\textrm{-}Lam}$:

We have $(\lambda x^{A}.M_{1})\,M_{2}\leadsto_{\beta}M_{1}[M_{2}/x]$. Then,
(1)$\llbracket(\lambda x^{A}.M_{1})\,M_{2}\rrbracket=(\lambda x^{A}.\llbracket
M_{1}\rrbracket)\ \llbracket M_{2}\rrbracket\leadsto_{\beta}\llbracket
M_{1}\rrbracket[\llbracket M_{2}\rrbracket/x]=\llbracket
M_{1}[M_{2}/x]\rrbracket$, where the last equation follows from Lemma B.3.

$\mathsf{\beta\textrm{-}Project}$:

We have $\langle(\ell_{i}=M_{i})_{i}\rangle.\ell_{j}\leadsto_{\beta}M_{j}$.
Our goal follows from
(2)$\llbracket\langle(\ell_{i}=M_{i})_{i}\rangle.\ell_{j}\rrbracket=\langle(\ell_{i}=\llbracket
M_{i}\rrbracket)_{i}\rangle.\ell_{j}\leadsto_{\beta}\llbracket
M_{j}\rrbracket$.

$\mathsf{\vartriangleright\\!\\!\textrm{-}Upcast}$:

We have
$\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}\vartriangleright\langle\ell_{j}^{\prime}:A_{j}\rangle_{j}\leadsto_{\vartriangleright}\langle\ell^{\prime}_{j}=M_{\ell^{\prime}_{j}}\rangle_{j}$.
Our goal follows from
$\llbracket\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}\vartriangleright\langle\ell_{j}^{\prime}:A_{j}\rangle_{j}\rrbracket=\langle\ell_{j}^{\prime}={\llbracket\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}\rrbracket}.{\ell_{j}^{\prime}}\rangle_{j}=\langle\ell_{j}^{\prime}={\langle\ell_{i}=\llbracket
M_{\ell_{i}}\rrbracket\rangle_{i}}.{\ell_{j}^{\prime}}\rangle_{j}\rightsquigarrow_{\beta}^{\ast}\langle\ell_{j}^{\prime}=\llbracket
M_{\ell_{j}^{\prime}}\rrbracket\rangle_{j}$.

Then, we prove the full theorem by induction on $M$. We only need to prove the
case where reduction happens in sub-terms of $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

The reduction can only happen in $M^{\prime}$. Supposing $\lambda
x^{A}.M^{\prime}\rightsquigarrow_{\beta\vartriangleright}\lambda
x^{A}.N^{\prime}$, by IH on $M^{\prime}$, we have $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\beta}^{\ast}\llbracket
N^{\prime}\rrbracket$, which then gives $\llbracket\lambda
x^{A}.M^{\prime}\rrbracket=\lambda x^{A}.\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\beta}^{\ast}\lambda x^{A}.\llbracket
N^{\prime}\rrbracket=\llbracket\lambda x^{A}.N^{\prime}\rrbracket$.

$M_{1}\ M_{2}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen
either in $M_{1}$ or $M_{2}$.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
one of $(M_{i})_{i}$.

$M^{\prime}.\ell$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

$M^{\prime}\vartriangleright A$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

Reflection: We proceed by induction on $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

We have $\llbracket M\rrbracket=\lambda x^{\llbracket A\rrbracket}.\llbracket
M^{\prime}\rrbracket$. The reduction can only happen in $\llbracket
M^{\prime}\rrbracket$. Suppose $\llbracket
M\rrbracket\rightsquigarrow_{\beta}\lambda x^{\llbracket A\rrbracket}.N_{1}$.
By IH on $\llbracket M^{\prime}\rrbracket$, there exists $N^{\prime}$ such
that $N_{1}\rightsquigarrow_{\beta}^{\ast}\llbracket N^{\prime}\rrbracket$ and
$M^{\prime}\rightsquigarrow_{\beta\vartriangleright}N^{\prime}$. Our goal
follows from setting $N$ to $\lambda x^{A}.N^{\prime}$.

$M_{1}\ M_{2}$:

We have $\llbracket M\rrbracket=\llbracket M_{1}\rrbracket\ \llbracket
M_{2}\rrbracket$. Proceed by case analysis where the reduction happens.

  * •:

Reduction happens in either $\llbracket M_{1}\rrbracket$ or $\llbracket
M_{2}\rrbracket$. Similar to the $\lambda x^{A}.M^{\prime}$ case.

  * •:

The application is reduced by $\mathsf{\beta\textrm{-}Lam}$. By definition of
translation, we have $M_{1}=\lambda x^{A}.M^{\prime}$. By  (1), we have
$\llbracket M\rrbracket\leadsto_{\beta}\llbracket
M^{\prime}[M_{2}/x]\rrbracket$. Our goal follows from setting setting $N$ to
$M^{\prime}[M_{2}/x]$.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

We have $\llbracket M\rrbracket=\langle\ell_{i}=\llbracket
M_{i}\rrbracket\rangle_{i}$. Similar to the $\lambda x^{A}.M^{\prime}$ case as
the reduction can only happen in one of $\llbracket M_{i}\rrbracket$.

$M^{\prime}.\ell_{j}$:

We have $\llbracket M\rrbracket=\llbracket M^{\prime}\rrbracket.\ell_{j}$.
Proceed by case analysis where the reduction happens.

  * •:

Reduction happens in $\llbracket M^{\prime}\rrbracket$. Similar to the
$\lambda x^{A}.M^{\prime}$ case.

  * •:

The projection is reduced by $\mathsf{\beta\textrm{-}Project}$. By definition
of translation, we have $M^{\prime}=\langle\ell_{i}=M_{i}\rangle_{i}$. By
(2), we have $\llbracket M\rrbracket\leadsto_{\beta}\llbracket
M_{j}\rrbracket$. Our goal follows from setting setting $N$ to $M_{j}$.

$M^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}$:

We have $\llbracket
M^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket=\langle\ell_{i}=\llbracket
M^{\prime}\rrbracket.\ell_{i}\rangle_{i}$. Proceed by case analysis where the
reduction happens.

  * •:

Reduction happens in one of $\llbracket M^{\prime}\rrbracket$ in the result
record. Supposing $\llbracket M\rrbracket\rightsquigarrow_{\beta}M_{1}$, and
in $M_{1}$ one of $\llbracket M^{\prime}\rrbracket$ is reduced to $N_{1}$. By
IH on $\llbracket M^{\prime}\rrbracket$, there exists $N^{\prime}$ such that
$N_{1}\rightsquigarrow_{\beta}^{\ast}\llbracket N^{\prime}\rrbracket$ and
$M^{\prime}\rightsquigarrow_{\beta\vartriangleright}N^{\prime}$. Thus, we can
apply the reduction $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\beta}N_{1}\rightsquigarrow_{\beta}^{\ast}\llbracket
N^{\prime}\rrbracket$ to all $\llbracket M^{\prime}\rrbracket$ in the result
record, which gives us $\llbracket
M\rrbracket\rightsquigarrow_{\beta}M_{1}\rightsquigarrow_{\beta}^{\ast}\llbracket
N^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket$. Our
goal follows from setting $N$ to
$N^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}$ and
${M^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}}\rightsquigarrow_{\beta\vartriangleright}{N^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}}$.

  * •:

One of $\llbracket M^{\prime}\rrbracket.\ell_{i}$ is reduced by
$\mathsf{\beta\textrm{-}Project}$. By the definition of translation, we know
that $M^{\prime}=\langle\ell_{j}^{\prime}=M_{\ell_{j}^{\prime}}\rangle_{j}$.
Supposing $\llbracket M\rrbracket\rightsquigarrow_{\beta}M_{1}$, we can reduce
all projection in $\llbracket M\rrbracket$, which gives us
$M_{1}\rightsquigarrow_{\beta}^{\ast}\langle\ell_{i}=\llbracket
M_{\ell_{i}}\rrbracket\rangle_{i}=\llbracket\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}\rrbracket$.
Our goal follows from setting $N$ to
${\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}}$ and
$M^{\prime}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\leadsto_{\vartriangleright}N$.

∎

###  B.4. Proof of the Encoding
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$

###### Lemma B.4 (Translation commutes with substitution).

If $\Delta;\Gamma,x:A\vdash M:B$ and $\Delta;\Gamma\vdash N:A$, then
$\llbracket M[N/x]\rrbracket=\llbracket M\rrbracket[\llbracket
N\rrbracket/x]$.

###### Proof.

By straightforward induction on $M$. We only need to consider cases that are
different from the proof of Lemma B.3.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

By IH and definition of substitution, we have

$\begin{array}[]{ll}&\llbracket\langle\ell_{i}=M_{i}\rangle_{i}^{\langle\ell_{i}:A_{i}\rangle_{i}}[N/x]\rrbracket\\\
=&\llbracket\langle\ell_{i}=M_{i}[N/x]\rangle_{i}^{\langle\ell_{i}:A_{i}\rangle_{i}}\rrbracket\\\
=&(\Lambda\theta_{i})_{i}.\langle\ell_{i}=\llbracket
M_{i}[N/x]\rrbracket\rangle_{i}^{\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}}\\\
=&(\Lambda\theta_{i})_{i}.\langle\ell_{i}=\llbracket
M_{i}\rrbracket[\llbracket
N\rrbracket/x]\rangle_{i}^{\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}}\\\
=&((\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 N\rrbracket/x]\\\
=&\llbracket\langle\ell_{i}=M_{i}\rangle_{i}^{\langle\ell_{i}:A_{i}\rangle_{i}}\rrbracket[\llbracket
N\rrbracket/x]\end{array}$

$M^{\prime}.\ell$:

By an equational reasoning similar to the case of
$\langle\ell_{i}=M_{i}\rangle_{i}$.

$M^{\prime}\vartriangleright A$:

By an equational reasoning similar to the case of
$\langle\ell_{i}=M_{i}\rangle_{i}$.

∎

See 4.7

###### Proof.

By induction on typing derivations.

$\mathsf{T\textrm{-}Var}$:

Our goal follows from $\llbracket x\rrbracket=x$.

$\mathsf{T\textrm{-}Lam}$:

Our goal follows from IH and $\mathsf{T\textrm{-}Lam}$.

$\mathsf{T\textrm{-}App}$:

Our goal follows from IH and $\mathsf{T\textrm{-}App}$.

$\mathsf{T\textrm{-}Record}$:

Our goal follows from IH, $\mathsf{T\textrm{-}Record}$ and
$\mathsf{T\textrm{-}PreLam}$.

$\mathsf{T\textrm{-}Project}$:

Supposing $M=M^{\prime}.\ell_{j}$ and $\Delta;\Gamma\vdash
M^{\prime}:\langle\ell_{i}:A_{i}\rangle_{i}$, by definition of translation we
have $\llbracket M^{\prime}.\ell_{j}\rrbracket=(\llbracket
M^{\prime}\rrbracket(P_{i})_{i}).\ell_{j}$ where $P_{j}=\bullet$. IH on
$M^{\prime}$ implies
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M^{\prime}\rrbracket:(\forall\theta_{i})_{i}.\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}$. Our goal follows from
$\mathsf{T\textrm{-}PreApp}$ and $\mathsf{T\textrm{-}Project}$.

$\mathsf{T\textrm{-}Upcast}$:

The only subtyping relation in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ is for
record types. Given $\Delta;\Gamma\vdash M^{\langle
R\rangle}\vartriangleright[R^{\prime}]:[R^{\prime}]$, by $\Delta;\Gamma\vdash
M:\langle R\rangle$ and IH we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket\langle R\rangle\rrbracket$. Then, by definition of
translation and $\mathsf{T\textrm{-}RowApp}$ we have
$\llbracket\Delta\rrbracket;\llbracket\Gamma\rrbracket\vdash\llbracket
M^{\langle R\rangle}\vartriangleright\langle
R^{\prime}\rangle\rrbracket:\llbracket\langle R^{\prime}\rangle\rrbracket$.

∎

See 4.8

###### Proof.

Simulation: First, we prove the base case that the whole term $M$ is reduced,
i.e. $M\leadsto_{\beta}N$ implies $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{\ast}\leadsto_{\beta}\llbracket
N\rrbracket$, and $M\leadsto_{\vartriangleright}N$ implies $\llbracket
M\rrbracket\rightsquigarrow_{\nu}^{\ast}\llbracket N\rrbracket$. The proof
proceeds by case analysis on the reduction relation:

$\mathsf{\beta\textrm{-}Lam}$:

We have $(\lambda x^{A}.M_{1})\,M_{2}\leadsto_{\beta}M_{1}[M_{2}/x]$. Then,
(1)$\llbracket(\lambda x^{A}.M_{1})\,M_{2}\rrbracket=(\lambda x^{A}.\llbracket
M_{1}\rrbracket)\ \llbracket M_{2}\rrbracket\leadsto_{\beta}\llbracket
M_{1}\rrbracket[\llbracket M_{2}\rrbracket/x]=\llbracket
M_{1}[M_{2}/x]\rrbracket$, where the last equation follows from Lemma B.4.

$\mathsf{\beta\textrm{-}Project}$:

We have $\langle(\ell_{i}=M_{i})_{i}\rangle.\ell_{j}\leadsto_{\beta}M_{j}$. By
definition of translation, we have
$\llbracket\langle(\ell_{i}=M_{i})_{i}\rangle.\ell_{j}\rrbracket=(\llbracket\langle\ell_{i}=M_{i}\rangle_{i}\rrbracket(P_{i})_{i}).\ell_{j}=(((\Lambda\theta_{i})_{i}.\langle\ell_{i}^{\theta_{i}}=\llbracket
M_{i}\rrbracket\rangle_{i})(P_{i})_{i}).\ell_{j}$, where $P_{j}=\bullet$ and
$P_{i}=\circ(i\neq j)$. Applying $\mathsf{\beta\textrm{-}PreLam}$, we have
(2)$\llbracket\langle(\ell_{i}=M_{i})_{i}\rangle.\ell_{j}\rrbracket\rightsquigarrow_{\tau}^{\ast}(\langle\ell_{i}^{P_{i}}=\llbracket
M_{i}\rrbracket\rangle_{i}).\ell_{j}\leadsto_{\beta}\llbracket
M_{j}\rrbracket$.

$\mathsf{\vartriangleright\\!\\!\textrm{-}Upcast}$:

We have $\langle(\ell_{i}=M_{\ell_{i}})_{i}\rangle^{\langle
R\rangle}\vartriangleright\langle
R^{\prime}\rangle\leadsto_{\vartriangleright}\langle\ell_{j}^{\prime}=M_{\ell_{j}^{\prime}}\rangle_{j}$,
where $R=(\ell_{i}:A_{\ell_{i}})_{i}$ and
$R^{\prime}=(\ell_{j}^{\prime}:A_{\ell_{j}^{\prime}})_{j}$. By definition,
(3)$\llbracket\langle(\ell_{i}=M_{\ell_{i}})_{i}\rangle^{\langle
R\rangle}\vartriangleright\langle
R^{\prime}\rangle\rrbracket=(\Lambda\theta_{j}^{\prime})_{j}.\llbracket\langle(\ell_{i}=M_{\ell_{i}})_{i}\rangle^{\langle
R\rangle}\rrbracket\,(@\,P_{i})_{i}=(\Lambda\theta_{j}^{\prime})_{j}.((\Lambda\theta_{i})_{i}.\langle\ell_{i}=\llbracket
M_{\ell_{i}}\rrbracket\rangle_{i}^{\langle\ell_{i}^{\theta_{i}}:A_{\ell_{i}}\rangle_{i}})\,(@\,P_{i})_{i}\rightsquigarrow_{\nu}^{\ast}(\Lambda\theta_{j}^{\prime})_{j}.\langle\ell_{i}=\llbracket
M_{\ell_{i}}\rrbracket\rangle_{i}^{\langle\ell_{i}^{P_{i}}:A_{\ell_{i}}\rangle_{i}}$,
where $P_{i}=\circ$ when $\ell_{i}\notin(\ell_{j}^{\prime})_{j}$, and
$P_{i}=\theta_{j}^{\prime}$ when $\ell_{i}=\ell_{j}^{\prime}$. By the fact
that we ignore absent labels when comparing records in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\theta}$, we have
(4)$(\Lambda\theta^{\prime}_{j})_{j}.\langle\ell_{i}=\llbracket
M_{\ell_{i}}\rrbracket\rangle_{i}^{\langle\ell_{i}^{P_{i}}:A_{\ell_{i}}\rangle_{i}}=(\Lambda\theta_{j}^{\prime})_{j}.\langle\ell_{j}^{\prime}=\llbracket
M_{\ell_{j}^{\prime}}\rrbracket\rangle^{\langle\ell_{j}^{\prime\theta_{j}^{\prime}}:A_{\ell_{j}^{\prime}}\rangle_{j}}=\llbracket\langle\ell_{j}^{\prime}=M_{\ell_{j}^{\prime}}\rangle_{j}\rrbracket$.

Then, we prove the full theorem by induction on $M$. We only need to prove the
case where reduction happens in sub-terms of $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

The reduction can only happen in $M^{\prime}$. Supposing $\lambda
x^{A}.M^{\prime}\rightsquigarrow_{\beta}\lambda x^{A}.N^{\prime}$, by IH on
$M^{\prime}$, we have $\llbracket
M^{\prime}\rrbracket\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}\llbracket
N^{\prime}\rrbracket$, which then gives $\llbracket\lambda
x^{A}.M^{\prime}\rrbracket=\lambda x^{A}.\llbracket
M^{\prime}\rrbracket\leadsto_{\tau}^{\ast}\rightsquigarrow_{\beta}\lambda
x^{A}.\llbracket N^{\prime}\rrbracket=\llbracket\lambda
x^{A}.N^{\prime}\rrbracket$. The same applies to the second part of the
theorem.

$M_{1}\ M_{2}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen
either in $M_{1}$ or $M_{2}$.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
one of $(M_{i})_{i}$.

$M^{\prime}.\ell$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

$M^{\prime}\vartriangleright A$:

Similar to the $\lambda x^{A}.M^{\prime}$ case as reduction can only happen in
$M^{\prime}$.

Reflection: We proceed by induction on $M$.

$x$:

No reduction.

$\lambda x^{A}.M^{\prime}$:

We have $\llbracket M\rrbracket=\lambda x^{\llbracket A\rrbracket}.\llbracket
M^{\prime}\rrbracket$. The reduction can only happen in $\llbracket
M^{\prime}\rrbracket$. Suppose $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}\lambda
x^{\llbracket A\rrbracket}.\llbracket N^{\prime}\rrbracket$. By IH on
$\llbracket M^{\prime}\rrbracket$,
$M^{\prime}\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}N^{\prime}$.
Our goal follows from $\lambda
x^{A}.M^{\prime}\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}\lambda
x^{A}.N^{\prime}$. Suppose $\llbracket
M\rrbracket\rightsquigarrow_{\nu}\lambda x^{\llbracket A\rrbracket}.N_{1}$. By
IH on $\llbracket M^{\prime}\rrbracket$, there exists $N^{\prime}$ such that
$N_{1}\rightsquigarrow_{\nu}^{\ast}\llbracket N^{\prime}\rrbracket$ and
$M^{\prime}\rightsquigarrow_{\vartriangleright\blacktriangleright}N^{\prime}$.
Our goal follows from setting $N$ to $\lambda x^{A}.N^{\prime}$.

$M_{1}\ M_{2}$:

We have $\llbracket M\rrbracket=\llbracket M_{1}\rrbracket\ \llbracket
M_{2}\rrbracket$. Proceed by case analysis where the reduction happens.

  * •:

Reduction happens in either $\llbracket M_{1}\rrbracket$ or $\llbracket
M_{2}\rrbracket$. Similar to the $\lambda x^{A}.M^{\prime}$ case.

  * •:

The application is reduced by $\mathsf{\beta\textrm{-}Lam}$. By definition of
translation, we have $M_{1}=\lambda x^{A}.M^{\prime}$. By  (1), we have
$\llbracket M\rrbracket\leadsto_{\beta}\llbracket
M^{\prime}[M_{2}/x]\rrbracket$. Our goal follows from setting setting $N$ to
$M^{\prime}[M_{2}/x]$.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

We have $\llbracket
M\rrbracket=(\Lambda\theta_{i})_{i}.\langle\ell_{i}=\llbracket
M_{i}\rrbracket\rangle_{i}^{\langle\ell_{i}^{\theta_{i}}:\llbracket
A_{i}\rrbracket\rangle_{i}}$. Similar to the $\lambda x^{A}.M^{\prime}$ case
as the reduction can only happen in one of $\llbracket M_{i}\rrbracket$.

$M^{\prime}.\ell_{j}$:

We have $\llbracket M\rrbracket=(\llbracket
M^{\prime}\rrbracket\,({P_{i}})_{i}).\ell_{j}$, where $P_{i}=\circ$ for $i\neq
j$ and $P_{j}=\bullet$. Proceed by case analysis where the $\beta$-reduction
happens.

  * •:

Reduction happens in $\llbracket M^{\prime}\rrbracket$. Similar to the
$\lambda x^{A}.M^{\prime}$ case.

  * •:

The projection is reduced by $\mathsf{\beta\textrm{-}Project^{\star}}$.
Supposing $\llbracket
M\rrbracket\rightsquigarrow_{\tau}^{\ast}\rightsquigarrow_{\beta}\llbracket
N\rrbracket$, because $\llbracket N\rrbracket$ is in the codomain of the
translation, the $\rightsquigarrow_{\tau}^{\ast}$ can only be the type
applications of $(P_{i})_{i}$ and
$M^{\prime}=\langle\ell_{i}=M_{i}\rangle_{i}$. By  (2), we have $\llbracket
M^{\prime}.\ell_{j}\rrbracket\rightsquigarrow_{\tau}^{\ast}\leadsto_{\beta}\llbracket
M_{j}\rrbracket$. Our goal follows from
$M^{\prime}.\ell_{j}\leadsto_{\beta}M_{j}$.

${M^{\prime\langle\ell_{i}:A_{i}\rangle_{i}}\vartriangleright\langle\ell^{\prime}_{j}:A^{\prime}_{j}\rangle_{j}}$:

We have $\llbracket M\rrbracket=(\Lambda\theta_{j})_{j}.\llbracket
M^{\prime}\rrbracket\,(@\,P_{i})_{i}$, where $P_{i}=\circ$ for
$\ell_{i}\notin(\ell_{j}^{\prime})_{j}$, and $P_{i}=\theta_{j}$ for
$\ell_{i}=\ell_{j}^{\prime}$. Proceed by case analysis where the reduction
happens.

  * •:

Reduction happens in $\llbracket M^{\prime}\rrbracket$. Similar to the
$\lambda x^{A}.M^{\prime}$ case.

  * •:

The presence type application $\llbracket M^{\prime}\rrbracket\,@\,P_{1}$ is
reduced by $\mathsf{\nu\textrm{-}PreLam}$. Because the top-level constructor
of $\llbracket M^{\prime}\rrbracket$ should be type abstraction, there are two
cases. Proceed by case analysis on $M^{\prime}$.

    * –:

$M^{\prime}=\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}$. We can reduce all
presence type application of $P_{i}$. By  (3) and  (4), we have $\llbracket
M\rrbracket\rightsquigarrow_{\nu}^{\ast}\llbracket\langle\ell_{j}^{\prime}=M_{\ell_{j}^{\prime}}\rangle_{j}\rrbracket$.
Our goal follows from setting $N$ to
${\langle\ell_{j}^{\prime}=M_{\ell_{j}^{\prime}}\rangle_{j}}$ and
$M\leadsto_{\vartriangleright}N$.

    * –:

$M^{\prime}=M_{1}^{\langle\ell_{k}^{\prime\prime}:B_{k}\rangle_{k}}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}$.
We can reduce all presence type application of $P_{i}$. We have $\llbracket
M\rrbracket=(\Lambda\theta_{j})_{j}.\llbracket
M_{1}\vartriangleright\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket\,(@\,P_{i})_{i}=$
$(\Lambda\theta_{j})_{j}.((\Lambda\theta_{i})_{i}.\llbracket
M_{1}\rrbracket\,(@\,P_{k}^{\prime})_{k})\,(@\,P_{i})_{i}\rightsquigarrow_{\nu}^{\ast}(\Lambda\theta_{j})_{j}.\llbracket
M_{1}\rrbracket\,(@\,Q_{k})_{k}$, where $P_{k}^{\prime}=\circ$ for
$\ell_{k}^{\prime\prime}\notin(\ell_{i})_{i}$, and $P_{k}^{\prime}=\theta_{i}$
for $\ell_{k}^{\prime\prime}=\ell_{i}$. Thus, we have $Q_{k}=\circ$ for
$\ell_{k}^{\prime\prime}\notin(\ell_{j}^{\prime})_{j}$, and $Q_{k}=\theta_{j}$
for $\ell_{k}^{\prime\prime}=\ell_{j}^{\prime}$, which implies $\llbracket
M_{1}\vartriangleright\langle\ell_{j}^{\prime}:A_{j}^{\prime}\rangle_{j}\rrbracket=(\Lambda\theta_{j})_{j}.\llbracket
M_{1}\rrbracket\,(@\,Q_{k}^{\prime})_{k}$. Our goal follows from setting $N$
to
${M_{1}\vartriangleright\langle\ell_{j}^{\prime}:A_{j}^{\prime}\rangle_{j}}$
and $M\leadsto_{\blacktriangleright}N$.

∎

##  Appendix C Encodings, Proofs and Definitions in Section 5

In this section, we provide the encodings, proofs, and definitions missing
from Section 5.

###  C.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$}}}$

The 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$}}}$
(Pierce, 2002; Breazu-Tannen et al., 1991) is formalised as follows.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llbracket-\rrbracket~{}&:\hfil~{}&\mathsf{Derivation}\to\mathsf{Term}\\\
\llbracket M^{A}\vartriangleright B\rrbracket~{}&=\hfil~{}&\llbracket
A\leqslant B\rrbracket\ \llbracket M\rrbracket\\\\[8.61108pt]
\llbracket-\rrbracket~{}&:\hfil~{}&\mathrm{Subtyping}\to\mathsf{Term}\\\
\llbracket\alpha\leqslant\alpha\rrbracket~{}&=\hfil~{}&\lambda x^{\alpha}.x\\\
\llbracket A\to B\leqslant A^{\prime}\to
B^{\prime}\rrbracket~{}&=\hfil~{}&\lambda f^{A\to B}.\lambda
x^{A^{\prime}}.\llbracket B\leqslant B^{\prime}\rrbracket\ (f\ (\llbracket
A^{\prime}\leqslant A\rrbracket\ x))\\\
\Bigl{\llbracket}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
86.76523pt\vbox{\hbox{\hskip-86.76523pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{dom}(R)\subseteq\mathsf{dom}(R^{\prime})\quad[A_{i}\leqslant
A_{i}^{\prime}]_{(\ell_{i}:A_{i})\in R,(\ell_{i}:A_{i}^{\prime})\in
R^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
20.66234pt\vbox{\vbox{}\hbox{\hskip-20.66232pt\hbox{\hbox{$\displaystyle\displaystyle[R]\leqslant[R^{\prime}]$}}}}}}$}}\Bigr{\rrbracket}~{}&=\hfil~{}&\lambda
x^{[R]}.\mathbf{case}~{}x~{}\\{\ell_{i}\ y\mapsto(\ell_{i}\ (\llbracket
A_{i}\leq A_{i}^{\prime}\rrbracket\ y))^{[R^{\prime}]}\\}\\\
\Bigl{\llbracket}{\hbox{$\displaystyle\displaystyle{\hbox{\hskip
86.76523pt\vbox{\hbox{\hskip-86.76523pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{dom}(R^{\prime})\subseteq\mathsf{dom}(R)\quad[A_{i}\leqslant
A_{i}^{\prime}]_{(\ell_{i}:A_{i})\in R,(\ell_{i}:A_{i}^{\prime})\in
R^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
20.10686pt\vbox{\vbox{}\hbox{\hskip-20.10684pt\hbox{\hbox{$\displaystyle\displaystyle\langle
R\rangle\leqslant\langle
R^{\prime}\rangle$}}}}}}$}}\Bigr{\rrbracket}~{}&=\hfil~{}&\lambda x^{\langle
R\rangle}.\langle\ell_{i}=\llbracket A_{i}\leq A_{i}^{\prime}\rrbracket\
x.\ell_{i}\rangle\end{array}$

###  C.2. Dynamic Semantics of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$

In addition to the erasure semantics, the other style of dynamic semantics of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
is given by extending the operational semantics rules with the following four
upcast rules.

$\begin{array}[]{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}\mathsf{\vartriangleright\\!\\!\textrm{-}Var}&M\vartriangleright\alpha~{}~{}&\leadsto_{\vartriangleright}\hfil~{}~{}&M\\\
\mathsf{\vartriangleright\\!\\!\textrm{-}Lam}&(\lambda
x^{A}.M)\vartriangleright A^{\prime}\to
B^{\prime}~{}~{}&\leadsto_{\vartriangleright}\hfil~{}~{}&\lambda
y^{A^{\prime}}.(M[(y\vartriangleright A)/x]\vartriangleright B^{\prime})\\\
\mathsf{\vartriangleright\\!\\!\textrm{-}Variant}&(\ell_{j}\,M)^{A}\vartriangleright[\ell_{i}:A_{i}]_{i}~{}~{}&\leadsto_{\vartriangleright}\hfil~{}~{}&(\ell_{j}\,(M\vartriangleright
A_{j}))^{[\ell_{i}:A_{i}]_{i}}\\\
\mathsf{\vartriangleright\\!\\!\textrm{-}Record}&\langle\ell_{i}=M_{\ell_{i}}\rangle_{i}\vartriangleright\langle\ell_{j}^{\prime}:A_{j}\rangle_{j}~{}~{}&\leadsto_{\vartriangleright}\hfil~{}~{}&\langle\ell^{\prime}_{j}=M_{\ell^{\prime}_{j}}\vartriangleright
A_{j}\rangle_{j}\end{array}$

We show that there is a correspondence between these two styles of dynamic
semantics of
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$.
We first give a preorder $M\sqsubseteq N$ on terms of the untyped
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$
which allows records in $M$ to contain more elements than those in $N$,
because the erasure semantics does not truly perform upcasts. The full
definition is shown in Figure 12.

$\displaystyle\displaystyle{\hbox{\hskip
58.71625pt\vbox{\hbox{\hskip-58.71625pt\hbox{\hbox{$\displaystyle\displaystyle\\{\ell_{j}^{\prime}\\}_{j}\subseteq\\{\ell_{i}\\}_{i}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle[M_{i}\sqsubseteq
N_{j}]_{\ell_{i}=\ell_{j}^{\prime}}$}}}}\vbox{}}}\over\hbox{\hskip
43.18115pt\vbox{\vbox{}\hbox{\hskip-43.18114pt\hbox{\hbox{$\displaystyle\displaystyle\langle\ell_{i}=M_{i}\rangle_{i}\sqsubseteq\langle\ell_{j}^{\prime}=N_{j}\rangle_{j}$}}}}}}$
$\displaystyle\displaystyle x\sqsubseteq x$
$\displaystyle\displaystyle{\hbox{\hskip
18.22827pt\vbox{\hbox{\hskip-18.22826pt\hbox{\hbox{$\displaystyle\displaystyle
M\sqsubseteq M^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
34.22131pt\vbox{\vbox{}\hbox{\hskip-34.2213pt\hbox{\hbox{$\displaystyle\displaystyle\lambda
x.M\sqsubseteq\lambda x.M^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
44.78986pt\vbox{\hbox{\hskip-44.78986pt\hbox{\hbox{$\displaystyle\displaystyle
M\sqsubseteq M^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle N\sqsubseteq
N^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
33.12323pt\vbox{\vbox{}\hbox{\hskip-33.12323pt\hbox{\hbox{$\displaystyle\displaystyle
M\ N\sqsubseteq M^{\prime}\ N^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
18.22827pt\vbox{\hbox{\hskip-18.22826pt\hbox{\hbox{$\displaystyle\displaystyle
M\sqsubseteq M^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
24.06158pt\vbox{\vbox{}\hbox{\hskip-24.06157pt\hbox{\hbox{$\displaystyle\displaystyle\ell\,M\sqsubseteq\ell\,M^{\prime}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
48.3027pt\vbox{\hbox{\hskip-48.3027pt\hbox{\hbox{$\displaystyle\displaystyle
M\sqsubseteq M^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle[N_{i}\sqsubseteq
N_{i}^{\prime}]_{i}$}}}}\vbox{}}}\over\hbox{\hskip
77.78557pt\vbox{\vbox{}\hbox{\hskip-77.78555pt\hbox{\hbox{$\displaystyle\displaystyle\mathbf{case}\,M\,\\{\ell_{i}\,x_{i}\mapsto
N_{i}\\}_{i}\sqsubseteq\mathbf{case}\,M^{\prime}\,\\{\ell_{i}\,x_{i}\mapsto
N_{i}^{\prime}\\}_{i}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
18.22827pt\vbox{\hbox{\hskip-18.22826pt\hbox{\hbox{$\displaystyle\displaystyle
M\sqsubseteq M^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
26.56158pt\vbox{\vbox{}\hbox{\hskip-26.56158pt\hbox{\hbox{$\displaystyle\displaystyle
M.\ell\sqsubseteq M^{\prime}.\ell$}}}}}}$ Figure 12. The preorder
$\sqsubseteq$ of untyped
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$.

The correspondence is given by the following theorem.

###### Theorem C.1 (Operational Correspondence).

Given a well-typed term $M$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$
and a term $M^{\prime}$ in untyped
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}$
with $M^{\prime}\sqsubseteq\mathsf{erase}(M)$, we have:

  * _Simulation_

If $M\rightsquigarrow_{\beta}N$, then there exists $N^{\prime}$ such that
$N^{\prime}\sqsubseteq\mathsf{erase}(N)$ and
$M^{\prime}\rightsquigarrow_{\beta}N^{\prime}$; if
$M\rightsquigarrow_{\vartriangleright}N$, then
$M^{\prime}\sqsubseteq\mathsf{erase}(N)$.

  * _Reflection_

If $M^{\prime}\rightsquigarrow_{\beta}N^{\prime}$, then there exists $N$ such
that $N^{\prime}\sqsubseteq\mathsf{erase}(N)$ and
$M\rightsquigarrow_{\vartriangleright}^{\ast}\rightsquigarrow_{\beta}N$.

To prove it, we need two lemmas.

###### Lemma C.2 (Erasure commutes with substitution).

If $\Delta;\Gamma,x:A\vdash M:B$ and $\Delta;\Gamma\vdash N:A$, then for
$M^{\prime}\sqsubseteq\mathsf{erase}(M)$ and
$N^{\prime}\sqsubseteq\mathsf{erase}(N)$, we have
$M^{\prime}[N^{\prime}/x]\sqsubseteq\mathsf{erase}(M[N/x])$.

###### Proof.

By straightforward induction on $M$. ∎

###### Lemma C.3 (Upcasts shrink terms).

For any $M\vartriangleright A\rightsquigarrow_{\vartriangleright}N$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$[]$}}\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{full}}$,
we have $\mathsf{erase}(M)\sqsubseteq\mathsf{erase}(N)$.

###### Proof.

By definition of $\mathsf{erase}(-)$ and
$\rightsquigarrow_{\vartriangleright}$. ∎

Then, we give the proof of Theorem C.1.

###### Proof.

Simulation: We proceed by induction on $M$.

$x$:

No reduction.

$\lambda x^{A}.M_{1}$:

Supposing $M^{\prime}=\lambda x.M_{1}^{\prime}$, by
$M^{\prime}\sqsubseteq\mathsf{erase}(M)$ we have
$M_{1}^{\prime}\sqsubseteq\mathsf{erase}(M_{1})$. The reduction must happen in
$M_{1}$. Our goal follows from the IH on $M_{1}$.

$M_{1}\ M_{2}$:

Supposing $M^{\prime}=M_{1}^{\prime}\ M_{2}^{\prime}$, by
$M^{\prime}\sqsubseteq\mathsf{erase}(M)$ we have
$M_{1}^{\prime}\sqsubseteq\mathsf{erase}(M_{1})$ and
$M_{2}^{\prime}\sqsubseteq\mathsf{erase}(M_{2})$. We proceed by case analysis
where the reduction happens.

  * •:

The reduction happens in either $M_{1}$ or $M_{2}$. Our goal follows from the
IH.

  * •:

The reduction reduces the top-level function application. Supposing
$M_{1}=\lambda x^{A}.M_{3}$ and $M_{1}^{\prime}=\lambda x.M_{3}^{\prime}$ with
$M_{3}^{\prime}\sqsubseteq\mathsf{erase}(M_{3})$, we have $(\lambda
x^{A}.M_{3})\ M_{2}\rightsquigarrow_{\beta}M_{3}[M_{2}/x]$ and $(\lambda
x^{A}.M_{3}^{\prime})\
M_{2}^{\prime}\rightsquigarrow_{\beta}M_{3}^{\prime}[M_{2}^{\prime}/x]$. Our
goal follows from Lemma C.2.

$N.\ell_{k}$:

Supposing $M^{\prime}=N^{\prime}.\ell_{k}$, by
$M^{\prime}\sqsubseteq\mathsf{erase}(M)$ we have
$N^{\prime}\sqsubseteq\mathsf{erase}(N^{\prime})$. We proceed by case analysis
where the reduction happens.

  * •:

The reduction happens in $N$. Our goal follows from the IH on $N$.

  * •:

The reduction reduces the top-level projection. Supposing
$N=\langle\ell_{i}=M_{i}\rangle_{i}$ and
$N^{\prime}=\langle\ell_{j}^{\prime}=M_{j}^{\prime}\rangle_{j}$ with
$\\{\ell_{j}^{\prime}\\}_{j}\subseteq\\{\ell_{i}\\}_{i}$ and
$(M_{j}^{\prime}\sqsubseteq\mathsf{erase}(M_{i}))_{\ell_{i}=\ell_{j}^{\prime}}$,
we have $N.\ell_{k}\rightsquigarrow_{\beta}M_{k}$ and
$N^{\prime}.\ell_{k}\rightsquigarrow_{\beta}M_{n}^{\prime}$ where
$\ell_{k}=\ell_{n}^{\prime}$. Our goal follows from
$M_{n}^{\prime}\sqsubseteq\mathsf{erase}(M_{k})$.

$\langle\ell_{i}=M_{i}\rangle_{i}$:

The reduction must happen in one of the $M_{i}$. Our goal follows from the IH.

$M_{1}\vartriangleright A$:

For the $\beta$-reduction, it must happen in $M_{1}$. Our goal follows from
the IH. For the upcast reduction, by $M^{\prime}\sqsubseteq\mathsf{erase}(M)$
we have $M^{\prime}\sqsubseteq\mathsf{erase}(M_{1})$. By Lemma C.3, we have
$M^{\prime}\sqsubseteq\mathsf{erase}(M_{1})\sqsubseteq\mathsf{erase}(N)$.

Reflection: We proceed by induction on $M^{\prime}$.

$x$:

No reduction.

$\lambda x.M_{1}^{\prime}$:

By $M^{\prime}\sqsubseteq\mathsf{erase}(M)$, we know that there exists
$\lambda x^{A}.M_{1}$ such that
$M\rightsquigarrow_{\vartriangleright}^{\ast}\lambda x^{A}.M_{1}$. By Lemma
C.3, $\mathsf{erase}(M)\sqsubseteq\mathsf{erase}(\lambda x^{A}.M_{1})$. Then,
by $M^{\prime}\sqsubseteq\mathsf{erase}(M)$ and transitivity, we have
$M_{1}^{\prime}\sqsubseteq\mathsf{erase}(M_{1})$. The $\beta$-reduction must
happen in $M_{1}^{\prime}$. Our goal follows from the IH on $M_{1}^{\prime}$.

$M_{1}^{\prime}\ M_{2}^{\prime}$:

By $M^{\prime}\sqsubseteq\mathsf{erase}(M)$, we know that there exists $M_{1}\
M_{2}$ such that $M\rightsquigarrow_{\vartriangleright}^{\ast}M_{1}\ M_{2}$.
By Lemma C.3 and $M^{\prime}\sqsubseteq\mathsf{erase}(M)$, we have
$M_{1}^{\prime}\sqsubseteq\mathsf{erase}(M_{1})$ and
$M_{2}^{\prime}\sqsubseteq\mathsf{erase}(M_{2})$. We proceed by case analysis
where the reduction happens.

  * •:

The reduction happens in either $M_{1}^{\prime}$ or $M_{2}^{\prime}$. Our goal
follows from the IH.

  * •:

The reduction reduces the top-level function application. Supposing
$M_{1}^{\prime}=\lambda x.M_{3}^{\prime}$, by
$M_{1}^{\prime}\sqsubseteq\mathsf{erase}(M_{1})$, we know that there exists
$\lambda x^{A}.M_{3}$ such that
$M_{1}\rightsquigarrow_{\vartriangleright}^{\ast}\lambda x^{A}.M_{3}$. Thus,
$M_{1}\
M_{2}\rightsquigarrow_{\vartriangleright}^{\ast}\rightsquigarrow_{\beta}M_{3}[M_{2}/x]$
and $M_{1}^{\prime}\
M_{2}^{\prime}\rightsquigarrow_{\beta}M_{3}^{\prime}[M_{2}^{\prime}/x]$. By
Lemma C.3, we have
$M_{1}^{\prime}\sqsubseteq\mathsf{erase}(M_{1})\sqsubseteq\mathsf{erase}(\lambda
x^{A}.M_{3})$, which implies $M_{3}^{\prime}\sqsubseteq\mathsf{erase}(M_{3})$.
Our goal follows from Lemma C.2.

$N^{\prime}.\ell_{k}$:

By $M^{\prime}\sqsubseteq\mathsf{erase}(M)$, we know that there exists
$N.\ell_{k}$ such that
$M\rightsquigarrow_{\vartriangleright}^{\ast}N.\ell_{k}$. By Lemma C.3 and
$M^{\prime}\sqsubseteq\mathsf{erase}(M)$, we have
$N^{\prime}\sqsubseteq\mathsf{erase}(N)$. We proceed by case analysis where
the reduction happens.

  * •:

The reduction happens in $N^{\prime}$. Our goal follows from the IH on $N$.

  * •:

The reduction reduces the top-level projection. Supposing
$N^{\prime}=\langle\ell_{j}^{\prime}=M_{j}^{\prime}\rangle_{j}$, by
$N^{\prime}\sqsubseteq\mathsf{erase}(N)$, we know that there exists
$\langle\ell_{i}=M_{i}\rangle_{i}$ such that
$N\rightsquigarrow_{\vartriangleright}^{\ast}\langle\ell_{i}=M_{i}\rangle_{i}$.
Thus,
$N.\ell_{k}\rightsquigarrow_{\vartriangleright}^{\ast}\rightsquigarrow_{\beta}M_{k}$
and $N^{\prime}.\ell_{k}\rightsquigarrow_{\beta}M_{n}^{\prime}$ where
$\ell_{n}^{\prime}=\ell_{k}$. By Lemma C.3, we have
$\mathsf{erase}(N)\sqsubseteq\mathsf{erase}(\langle\ell_{i}=M_{i}\rangle_{i})$.
We can further conclude that $M_{n}^{\prime}\sqsubseteq\mathsf{erase}(M_{k})$
from $N^{\prime}\sqsubseteq\mathsf{erase}(N)$.

∎

###  C.3. Proof of the 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}$

###### Lemma C.4 (Upcast Translation).

If $A\leqslant B$, then $\forall\overline{\theta}.\llbracket
A,\overline{P}\rrbracket=\llbracket B\rrbracket$ for
$(\overline{\theta},\overline{P})=\llparenthesis\theta,A\leqslant
B\rrparenthesis$.

###### Proof.

By a straightforward induction on the definition of
$\llparenthesis\theta,A\leqslant B\rrparenthesis$. ∎

See 5.1

###### Proof.

By induction on typing derivations.

$\mathsf{T\textrm{-}Var}$:

Our goal follows from $\llbracket x\rrbracket=x$.

$\mathsf{T\textrm{-}Lam}$:

By the IH on $\Delta;\Gamma,x:A\vdash M:B$, we have

$\Delta;\llbracket\Gamma\rrbracket,x:\llbracket A\rrbracket\vdash\llbracket
M\rrbracket:\llbracket B\rrbracket$

Let $\overline{\theta}=\llparenthesis\theta,B\rrparenthesis$. By
$\mathsf{T\textrm{-}PreApp}$ and context weakening, we have

$\Delta,\overline{\theta};\llbracket\Gamma\rrbracket,x:\llbracket
A\rrbracket\vdash\llbracket M\rrbracket\,\overline{\theta}:\llbracket
B,\overline{\theta}\rrbracket$

Notice that we always assume variable names in the same context are unique, so
we do not need to worry that $\overline{\theta}$ conflicts with $\Delta$.
Then, by $\mathsf{T\textrm{-}Lam}$, we have

$\Delta,\overline{\theta};\llbracket\Gamma\rrbracket\vdash\lambda
x^{\llbracket A\rrbracket}.\llbracket
M\rrbracket\,\overline{\theta}:\llbracket A\rrbracket\to\llbracket
B,\overline{\theta}\rrbracket$

Finally, by $\mathsf{T\textrm{-}PreLam}$, we have

$\Delta;\llbracket\Gamma\rrbracket\vdash\Lambda\overline{\theta}.\lambda
x^{\llbracket A\rrbracket}.\llbracket
M\rrbracket\,\overline{\theta}:\forall\overline{\theta}.\llbracket
A\rrbracket\to\llbracket B,\overline{\theta}\rrbracket$

Our goal follows from $\llbracket A\to
B\rrbracket=\forall\overline{\theta}.\llbracket A\rrbracket\to\llbracket
B,\overline{\theta}\rrbracket$.

$\mathsf{T\textrm{-}App}$:

Similar to the $\mathsf{T\textrm{-}Lam}$ case. Our goal follows from IH,
$\mathsf{T\textrm{-}App}$, $\mathsf{T\textrm{-}PreApp}$ and
$\mathsf{T\textrm{-}PreLam}$.

$\mathsf{T\textrm{-}Record}$:

Similar to the $\mathsf{T\textrm{-}Lam}$ case. Our goal follows from IH,
$\mathsf{T\textrm{-}Record}$, $\mathsf{T\textrm{-}PreApp}$ and
$\mathsf{T\textrm{-}PreLam}$.

$\mathsf{T\textrm{-}Project}$:

Given the derivation of $\Delta;\Gamma\vdash M.\ell_{j}{A_{j}}$, by the IH on
$\Delta;\Gamma\vdash M:\langle\ell_{i}:A_{i}\rangle_{i}$, we have

$\Delta;\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket\langle\ell_{i}:A_{i}\rangle_{i}\rrbracket$

Let $P_{i}=\circ(i\neq
j),P_{j}=\bullet,\overline{\theta}=\llparenthesis\theta,A_{j}\rrparenthesis,\overline{P}_{i}=\llparenthesis\circ,A_{i}\rrparenthesis$.
By $\mathsf{T\textrm{-}PreApp}$ and context weakening, we have

$\Delta,\overline{\theta};\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket\ (P_{i})_{i}\ (\overline{P}_{i})_{i<j}\ \overline{\theta}\
(\overline{P}_{i})_{j<i}:\langle R\rangle$

where $\ell_{j}:\llbracket A_{j},\overline{\theta}\rrbracket\in R$ by the
definition of translations and the canonical order. Then, by
$\mathsf{T\textrm{-}Proj}$, we have

$\Delta,\overline{\theta};\llbracket\Gamma\rrbracket\vdash(\llbracket
M\rrbracket\ (P_{i})_{i}\ (\overline{P}_{i})_{i<j}\ \overline{\theta}\
(\overline{P}_{i})_{j<i}).\ell_{j}:\llbracket
A_{j},\overline{\theta}\rrbracket$

Finally, by $\mathsf{T\textrm{-}PreLam}$, we have

$\Delta;\llbracket\Gamma\rrbracket\vdash(\llbracket M\rrbracket\ (P_{i})_{i}\
(\overline{P}_{i})_{i<j}\ \overline{\theta}\
(\overline{P}_{i})_{j<i}).\ell_{j}:\forall\overline{\theta}.\llbracket
A_{j},\overline{\theta}\rrbracket$

Our goal follows from $\llbracket
A_{j}\rrbracket=\forall\overline{\theta}.\llbracket
A_{j},\overline{\theta}\rrbracket$ where
$\overline{\theta}=\llparenthesis\theta,A_{j}\rrparenthesis$.

$\mathsf{T\textrm{-}Upcast}$:

Given the derivation of $\Delta;\Gamma\vdash M\vartriangleright B:B$, by the
IH on $\Delta;\Gamma\vdash M:A$, we have

$\Delta;\llbracket\Gamma\rrbracket\vdash\llbracket M\rrbracket:\llbracket
A\rrbracket$

Let $(\overline{\theta},\overline{P})=\llparenthesis\theta,A\leqslant
B\rrparenthesis$. By $\mathsf{T\textrm{-}PreApp}$ and context weakening, we
have

$\Delta,\overline{\theta};\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket\ \overline{P}:\llbracket A,\overline{P}\rrbracket$

Then, by $\mathsf{T\textrm{-}PreLam}$, we have

$\Delta;\llbracket\Gamma\rrbracket\vdash\Lambda\overline{\theta}.\llbracket
M\rrbracket\ \overline{P}:\forall\overline{\theta}.\llbracket
A,\overline{P}\rrbracket$

By Lemma C.4, we have $\llbracket
B\rrbracket=\forall\overline{\theta}.\llbracket A,\overline{P}\rrbracket$.

∎

##  Appendix D The Proof in Section 6

In this section, we spell out the proofs that are missing from Section 6.

###  D.1. Proof of encoding
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}2}^{\leqslant\mathrm{full}}$
using $\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho 1}$

See 6.2

###### Proof.

As shown in Section 6, we only need to prove that $\Delta;\Gamma\vdash M:A$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\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}$. We proceed
by induction on the typing derivations in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant\mathrm{afull}}$.

$\mathsf{T\textrm{-}Var}$:

Our goal follows directly from the definition of translations.

$\mathsf{T\textrm{-}Lam}$:

Given the derivation of $\Delta;\Gamma\vdash\lambda a^{A}.M:A\to B$, by the IH
on $\Delta;\Gamma,a:A\vdash M:B$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket),\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast};\Gamma,a:\llbracket
A,\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\rrbracket^{\ast}\vdash\llbracket
M\rrbracket:\tau_{B}$

for some $\tau_{B}\preccurlyeq\llbracket B\rrbracket$. Supposing
$\tau_{B}=\forall\overline{\rho}_{B}.B^{\prime}$, by
$\mathsf{T\textrm{-}Inst}$ and environment weakening, we have 333We always
assume type variables in type environments have different names, and we omit
kinds when they are easy to reconstruct from the context.

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket),\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast},\overline{\rho}_{B};\Gamma,a:\llbracket
A,\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\rrbracket^{\ast}\vdash\llbracket
M\rrbracket:B^{\prime}$

Then, by $\mathsf{T\textrm{-}Lam}$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket),\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast},\overline{\rho}_{B};\Gamma\vdash\lambda
a.\llbracket M\rrbracket:\llbracket
A,\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\rrbracket^{\ast}\to
B^{\prime}$

Finally, by $\mathsf{T\textrm{-}Gen}$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket);\Gamma\vdash\lambda
a.\llbracket
M\rrbracket:\forall\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\,\overline{\rho}_{B}.\llbracket
A,\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\rrbracket^{\ast}\to
B^{\prime}$

By definition, we have $\llbracket A\to
B\rrbracket=\forall\overline{\rho}_{1}\overline{\rho}_{2}.\llbracket
A,\overline{\rho}_{1}\rrbracket^{\ast}\to\llbracket
B,\overline{\rho}_{2}\rrbracket$, where
$\overline{\rho}_{1}=\llparenthesis\rho_{1},A\rrparenthesis^{\ast},\
\overline{\rho}_{2}=\llparenthesis\rho_{2},B\rrparenthesis$. It is easy to
check that
$\forall\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\,\overline{\rho}_{B}.\llbracket
A,\llparenthesis\rho_{|\Gamma|},A\rrparenthesis^{\ast}\rrbracket^{\ast}\to
B^{\prime}\preccurlyeq\llbracket A\to B\rrbracket$ under $\alpha$-renaming.

$\mathsf{T\textrm{-}AppSub}$:

Given the derivation of $\Delta;\Gamma\vdash M\,N:B$, by the IH on
$\Delta;\Gamma\vdash M:A\to B$, we have

$\llbracket\Delta;\Gamma\rrbracket\vdash\llbracket M\rrbracket:\tau_{1}$

for some $\tau_{1}\preccurlyeq\llbracket A\to B\rrbracket$. By the IH on
$\Delta;\Gamma\vdash B:A_{2}$, we have

$\llbracket\Delta;\Gamma\rrbracket\vdash\llbracket N\rrbracket:\tau_{2}$

for some $\tau_{2}\preccurlyeq\llbracket A_{2}\rrbracket$. We have
$\mho^{2}(A\to B)$, which implies $\mho^{1}(A)$. Then, $A_{2}\leqslant A$
gives us $\mho^{1}(A_{2})$, which further implies that $\llbracket
A_{2}\rrbracket=A_{2}$ and $\tau_{2}$ is not polymorphic. Thus, we have
$\tau_{2}\preccurlyeq\llbracket A_{2}\rrbracket=A_{2}\leqslant A$. Notice that
given $A\preccurlyeq\\_\leqslant B$ with $\mho^{1}(B)$, we can always
construct $\overline{R}$ with $\llbracket B,\overline{R}\rrbracket^{\ast}=A$,
by $\llparenthesis A\preccurlyeq\leqslant B\rrparenthesis$ defined as follows.

$\begin{array}[]{@{}r@{~}c@{~}l@{}}\llparenthesis-\rrparenthesis~{}&:\hfil~{}&(\mathsf{Type}\preccurlyeq\leqslant\mathsf{Type})\to(\overline{\mathsf{Row}})\\\
\llparenthesis\alpha\preccurlyeq\leqslant\alpha\rrparenthesis~{}&=\hfil~{}&(\cdot,\cdot)\\\
\llparenthesis A\to B\preccurlyeq\leqslant A\to
B^{\prime}\rrparenthesis~{}&=\hfil~{}&\llparenthesis B\preccurlyeq\leqslant
B^{\prime}\rrparenthesis\\\
\llparenthesis\langle(\ell_{i}:A_{i})_{i}\rangle\preccurlyeq\leqslant\langle(\ell_{j}^{\prime}:A_{j}^{\prime})\rangle\rrparenthesis~{}&=\hfil~{}&(\ell_{k}:A_{k})_{k\in\\{\ell_{i}\\}_{i}\backslash\\{\ell_{j}^{\prime}\\}_{j}}\
\llparenthesis A_{i}\preccurlyeq\leqslant
A_{j}^{\prime}\rrparenthesis_{\ell_{i}=\ell_{j}^{\prime}}\\\
\llparenthesis\langle(\ell_{i}:A_{i})_{i};\rho\rangle\preccurlyeq\leqslant\langle(\ell_{j}^{\prime}:A_{j}^{\prime})\rangle\rrparenthesis~{}&=\hfil~{}&((\ell_{k}:A_{k})_{k\in\\{\ell_{i}\\}_{i}\backslash\\{\ell_{j}^{\prime}\\}_{j}};\rho)\
\llparenthesis A_{i}\preccurlyeq\leqslant
A_{j}^{\prime}\rrparenthesis_{\ell_{i}=\ell_{j}^{\prime}}\\\ \end{array}$

Let $\overline{R}=\llparenthesis\tau_{2}\preccurlyeq\leqslant
A\rrparenthesis$. We have $\llbracket
A,\overline{R}\rrbracket^{\ast}=\tau_{2}$. Suppose
$\tau_{1}=\forall\overline{\rho}.A^{\prime}\to B^{\prime}$. By definition, we
have $\llbracket A\to
B\rrbracket=\forall\overline{\rho}_{1}\overline{\rho}_{2}.\llbracket
A,\overline{\rho}_{1}\rrbracket^{\ast}\to\llbracket
B,\overline{\rho}_{2}\rrbracket$, where
$\overline{\rho}_{1}=\llparenthesis\rho_{1},A\rrparenthesis^{\ast},\
\overline{\rho}_{2}=\llparenthesis\rho_{2},B\rrparenthesis$. By
$\tau_{1}\preccurlyeq\llbracket A\to B\rrbracket$, we have
$A^{\prime}=\llbracket A,\overline{\rho}_{1}\rrbracket^{\ast}$,
$B^{\prime}\preccurlyeq\llbracket B,\overline{\rho}_{2}\rrbracket$ and
$\overline{\rho}=\overline{\rho}_{1}\overline{\rho}_{2}$ after
$\alpha$-renaming. By $\mathsf{T\textrm{-}Inst}$ and environment weakening, we
have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket),\overline{\rho}_{2};\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\llbracket A,\overline{R}\rrbracket^{\ast}\to B^{\prime}$

Notice that $\llbracket A,\overline{R}\rrbracket^{\ast}=\tau_{2}$. We can then
apply $\mathsf{T\textrm{-}App}$ and environment weakening, which gives us

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket),\overline{\rho}_{2};\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket\,\llbracket N\rrbracket:B^{\prime}$

Finally, by $\mathsf{T\textrm{-}Gen}$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket);\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket\,\llbracket N\rrbracket:\forall\overline{\rho}_{2}.B^{\prime}$

The condition $\forall\overline{\rho}_{2}.B^{\prime}\preccurlyeq\llbracket
B\rrbracket$ holds obviously.

$\mathsf{T\textrm{-}Record}$:

Our goal follows from the IH and a sequence of applications of
$\mathsf{T\textrm{-}Inst}$, $\mathsf{T\textrm{-}Record}$, and
$\mathsf{T\textrm{-}Gen}$ similar to the previous cases.

$\mathsf{T\textrm{-}Project}$:

Our goal follows from the IH and a sequence of applications of
$\mathsf{T\textrm{-}Inst}$, $\mathsf{T\textrm{-}Project}$, and
$\mathsf{T\textrm{-}Gen}$ similar to the previous cases.

$\mathsf{T\textrm{-}Let}$:

Given the derivation of
$\Delta;\Gamma\vdash\mathbf{let}\,x=M\,\mathbf{in}\,N$, by the IH on
$\Delta;\Gamma\vdash M:A$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket);\llbracket\Gamma\rrbracket\vdash\llbracket
M\rrbracket:\tau_{1}$

for some $\tau_{1}\preccurlyeq\llbracket A\rrbracket$. By the IH on
$\Delta;\Gamma,x:A\vdash N:B$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket);\llbracket\Gamma\rrbracket,x:\llbracket
A\rrbracket\vdash\llbracket N\rrbracket:\tau_{2}$

for some $\tau_{2}\preccurlyeq\llbracket B\rrbracket$. By another
straightforward induction on the typing derivations, we can show that
$\Delta;\Gamma,x:\tau_{1}\vdash M:\tau_{2}$ implies
$\Delta;\Gamma,x:\tau_{1}^{\prime}\vdash M:\tau_{2}^{\prime}$ for
$\tau_{1}^{\prime}\preccurlyeq\tau_{1}$ and
$\tau_{2}^{\prime}\preccurlyeq\tau_{2}$. Thus, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket);\llbracket\Gamma\rrbracket,x:\tau_{1}\vdash\llbracket
N\rrbracket:\tau_{2}^{\prime}$

for some $\tau_{2}^{\prime}\preccurlyeq\tau_{2}\preccurlyeq\llbracket
B\rrbracket$. Then, by $\mathsf{T\textrm{-}Let}$, we have

$\Delta,\mathsf{ftv}(\llbracket\Gamma\rrbracket);\llbracket\Gamma\rrbracket\vdash\mathbf{let}\,x=\llbracket
M\rrbracket\,\mathbf{in}\,\llbracket N\rrbracket:\tau_{2}^{\prime}$

with $\tau_{2}^{\prime}\preccurlyeq\llbracket B\rrbracket$.

∎

##  Appendix E Proofs of Non-existence Results

In this section, we give the proofs of the non-existence results of Section 4
and Section 5.

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

See 4.9

###### Proof.

We provide three proofs of this theorem, the first one is based on the type
preservation property, the second one is based on the compositionality of
translations, and the third one carefully avoids using the type preservation
and compositionality. The point of multiple proofs is to show that the non-
existence of the encoding of
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\leqslant}$ in
$\lambda_{\text{\scalebox{1.0}[0.8]{$\langle\rangle$}}}^{\rho}$ is still true
even if we relax the condition of type preservation and compositionality,
which emphasises the necessity of the restrictions in Section 6.

Proof 1:

We assume that $\Delta=\alpha_{0}$ and $\Gamma=y:\alpha_{0}$ when environments
are omitted.

Consider $\langle\rangle$ and
$\langle\ell=y\rangle\vartriangleright\langle\rangle$. By the fact that
$\llbracket-\rrbracket$ is type-only, we have
$\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{\gamma}.\langle\ell=\Lambda\overline{\gamma}^{\prime}.y\rangle)\
\overline{B}$. Thus,
$\llbracket\langle\ell=y\rangle\vartriangleright\langle\rangle\rrbracket$ has
type
$\forall\overline{\alpha}^{\prime}.\langle\ell:\forall\overline{\gamma}^{\prime}.\alpha_{0}\rangle$
for some $\overline{\alpha}^{\prime}$.

By type preservation, the translated results should have the same type, which
implies
$\forall\overline{\alpha}.\langle\rangle=\forall\overline{\alpha}^{\prime}.\langle\ell:\forall\overline{\gamma}^{\prime}.\alpha_{0}\rangle$.
Thus, we have the equation
$\langle\rangle=\langle\ell:\forall\overline{\gamma}^{\prime}.\alpha_{0}\rangle$,
which leads to a contradiction as the right-hand side has an extra label
$\ell$ and we do not have presence types to remove labels.

Similarly, we can prove the theorem for variants by considering
$(\ell_{1}\,y)^{[\ell_{1}:\alpha_{0};\ell_{2}:\alpha_{0}]}$ and
$(\ell_{1}\,y)^{[\ell_{1}:\alpha_{0}]}\vartriangleright[\ell_{1}:\alpha_{0};\ell_{2}:\alpha_{0}]$.
The key point is that $\ell_{2}$ is arbitrarily chosen, so for the translation
of $(\ell_{1}\,y)^{[\ell_{1}:\alpha_{0}]}$ we cannot guarantee that $\ell_{2}$
appears in its type, and presence polymorphism does not give us the ability to
add new labels to row types.

Proof 2:

We assume that $\Delta=\alpha_{0}$ and $\Gamma=y:\alpha_{0}$ when environments
are omitted.

Consider the function application $M\ N$ where $M=\lambda
x^{\langle\rangle}.\langle\rangle$ and
$N=\langle\ell=y\rangle\vartriangleright\langle\rangle$. By the type-only
property, we have

$\llbracket\lambda
x^{\langle\rangle}.\langle\rangle\rrbracket=\Lambda\overline{\alpha}_{1}.\lambda
x^{A_{1}}.\Lambda\overline{\beta}_{1}.\langle\rangle\ B_{1}$

for some $\overline{\alpha}_{1},\overline{\beta}_{1},A_{1}$ and $B_{1}$. By
Proof 1, we have

$\llbracket\langle\ell=y\rangle\vartriangleright\langle\rangle\rrbracket=\Lambda\overline{\alpha}_{2}.\langle\ell=\Lambda\overline{\beta}_{2}.y\rangle$

for some $\overline{\alpha}_{2}$ and $\overline{\beta}_{2}$. Then, by the
type-only property, we have

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

for some $\overline{\alpha},\overline{\beta},\overline{A},\overline{B}$ and
$\overline{C}$. As we only have row polymorphism, the type application of
$\overline{B}$ cannot remove the label $\ell$ from the type of $\llbracket
N\rrbracket$. Since $\ell$ is arbitrarily chosen, it can neither be already in
the type of $\llbracket M\rrbracket$. By definition, a compositional
translation can only use the type information of $M$ and $N$, which contains
nothing about the label $\ell$. Thus, the label $\ell$ can neither be in
$\overline{A}$, which further implies that the $\llbracket M\ N\rrbracket$ is
not well-typed as the $\mathsf{T\textrm{-}App}$ must fail. Contradiction.

Proof 3:

Consider three functions $f_{1}=\lambda x^{\langle\rangle}.x$, $f_{2}=\lambda
x^{\langle\rangle}.\langle\rangle$, and $g=\lambda
f^{\langle\rangle\to\langle\rangle}.\langle\rangle$. By the type-only
property, we have

$\begin{array}[]{lll}\llbracket
f_{1}\rrbracket&=\Lambda\overline{\alpha}_{1}.\lambda
x^{A_{1}}.\Lambda\overline{\beta}_{1}.x\
\overline{B}_{1}&:\forall\overline{\alpha}_{1}.A_{1}\to\forall\overline{\beta}_{1}.A_{1}^{\prime}\\\
\llbracket f_{2}\rrbracket&=\Lambda\overline{\alpha}_{2}.\lambda
x^{A_{2}}.\Lambda\overline{\beta}_{2}.\langle\rangle&:\forall\overline{\alpha}_{2}.A_{2}\to\forall\overline{\beta}_{2}.\langle\rangle\\\
\llbracket g\rrbracket&=\Lambda\overline{\alpha}_{3}.\lambda
f^{A_{3}}.\Lambda\overline{\beta}_{3}.\langle\rangle&:\forall\overline{\alpha}_{3}.A_{3}\to\forall\overline{\beta}_{3}.\langle\rangle\end{array}$

where
$A_{1}^{\prime}=A_{1}^{\prime\prime}[\overline{B}_{1}/\overline{\alpha}_{1}^{\prime}]$
and $A_{1}=\forall\overline{\alpha}_{1}^{\prime}.A_{1}^{\prime\prime}$.

If there is some variable $\alpha_{1}^{\prime}\in\overline{\alpha}_{1}$
appears in $A_{1}$, then it must also appear in $A_{1}^{\prime}$ as we have no
way to remove it by the substitution
$[\overline{B}_{1}/\overline{\alpha}^{\prime}]$. Thus, $A_{3}$ should be of
shape $\forall\overline{\alpha}.A\to\forall\overline{\beta}.A^{\prime}$ where
$A^{\prime}$ contains some variable $\alpha^{\prime}\in\overline{\alpha}$.
However, this contradicts with the fact that $g$ can be applied to $f_{2}$,
because the type $\langle\rangle$ in the type of $\llbracket f_{2}\rrbracket$
cannot contain any variable in $\overline{\alpha}_{2}$. Hence, we can conclude
that $A_{1}$ cannot contain any variable in $\overline{\alpha}_{1}$, which
will lead to contradiction when we consider the translation of $f_{1}\
(\langle\ell=1\rangle\vartriangleright\langle\rangle)$ because we can neither
add the label $\ell$ in the type $A_{1}$, nor remove it in the type of
$\llbracket\langle\ell=1\rangle\vartriangleright\langle\rangle\rrbracket$.

∎

###  E.2. 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}$

See 5.3

###### Proof.

We assume that $\Delta=\alpha_{0}$ and $\Gamma=y:\alpha_{0}$ when environments
are omitted. For simplicity, we omit the type of labels in variant types if it
is $\alpha_{0}$.

By the fact that $\llbracket-\rrbracket$ is type-only, we have:

  * •

$(\ell\ y)^{[\ell]}$ is translated to $\Lambda\overline{\alpha}.(\ell\
(\Lambda\overline{\beta}.y))^{[R]}$ where
$(\ell:\forall\overline{\beta}.\alpha_{0})\in R$. By type preservation, we
have $\llbracket[\ell]\rrbracket=\forall\overline{\alpha}.[R]$.

  * •

$(\ell\ y)^{[\ell]}\vartriangleright[\ell;\ell^{\prime}]$ is translated to
$\Lambda\overline{\tau}.\llbracket(\ell\ y)^{[\ell]}\rrbracket\
\overline{T}=\Lambda\overline{\tau}.(\Lambda\overline{\alpha}.(\ell\
(\Lambda\overline{\beta}.y))^{[R]})\ \overline{T}$ where
$(\ell:\forall\beta.\alpha_{0})\in R$. By type preservation, we have
$\llbracket[\ell;\ell^{\prime}]\rrbracket={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(1){\forall\overline{\tau}\
\overline{\alpha}_{2}^{\prime}.[R][\overline{T}/\overline{\alpha}_{1}^{\prime}]}}$
where $\overline{\alpha}=\overline{\alpha}_{1}^{\prime}\
\overline{\alpha}_{2}^{\prime}$.

  * •

$(\ell^{\prime}\ y)^{[\ell;\ell^{\prime}]}$ is translated to
$\Lambda\overline{\alpha}^{\prime\prime}.(\ell^{\prime}\
(\Lambda\overline{\beta}^{\prime\prime}.y))^{[R^{\prime\prime}]}$ where
$\ell^{\prime}\in R^{\prime\prime}$. By symmetry, we also have $\ell\in
R^{\prime\prime}$. By type preservation, we have
$\llbracket[\ell;\ell^{\prime}]\rrbracket={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(2){\forall\overline{\alpha}^{\prime\prime}.[R^{\prime\prime}]}}$.

By the fact that
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(1){}}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(2){}}$
and $\ell^{\prime}$ can be an arbitrary label, we can conclude that $R$ has a
row variable $\rho_{R}$ bound in $\overline{\alpha}_{1}^{\prime}$ which is
instantiated to the $\ell^{\prime}$ label in $R^{\prime}$ by the substitution
$[\overline{A}/\overline{\alpha}_{1}^{\prime}]$. Thus, we have
(3)$R=(\ell:\forall\overline{\beta}.\alpha_{0});\dots;\rho_{R}$ where
$\rho_{R}\in\overline{\alpha}$.

Then, consider a nested variant
$M=(\ell\,(\ell\,y)^{[\ell]})^{[\ell:[\ell]]}$. Because
$\llbracket-\rrbracket$ is type-only, we have

$\llbracket M\rrbracket=\Lambda\overline{\alpha}^{\prime}.(\ell\
(\Lambda\overline{\beta}^{\prime}.(\Lambda\overline{\alpha}.(\ell\
(\Lambda\overline{\beta}.y))^{[R]})\ \overline{A}))^{[R^{\prime}]}$

By  (3), $\llbracket M\rrbracket$ has type
$\forall\overline{\alpha}^{\prime}.[R^{\prime}]=\forall\overline{\alpha}^{\prime}.[(\ell:\forall\overline{\beta}^{\prime}\
\overline{\alpha}_{2}.[R][\overline{A}/\overline{\alpha}_{1}]);\dots]$, where
$\overline{\alpha}=\overline{\alpha}_{1}\ \overline{\alpha}_{2}$ and
$\rho_{R}\in\overline{\alpha}$.

We proceed by showing the contradiction that $\rho_{R}$ can neither be in
$\alpha_{1}$ nor $\alpha_{2}$.

  * •

$\rho_{R}\in\overline{\alpha}_{2}$. Consider
$M^{\prime}=(\ell\,(\ell\,y)^{[\ell;\ell^{\prime}]})^{[\ell:[\ell;\ell^{\prime}]]}$
of type $[\ell:[\ell;\ell^{\prime}]]$. By an analysis similar to $M$, it is
easy to show that $\llbracket M^{\prime}\rrbracket$ has type
$\forall\overline{\mu}.[(\ell:\forall\overline{\nu}.[R_{1}]);\dots]$ where
$\ell\in R_{1}$ and $\ell^{\prime}\in R_{1}$.

Then, consider $M\vartriangleright[\ell:[\ell;\ell^{\prime}]]$ of the same
type $[\ell:[\ell;\ell^{\prime}]]$ as $M^{\prime}$ which is translated to
$\Lambda\overline{\gamma}.\llbracket M\rrbracket\ \overline{B}$. By type
preservation, the translation of $M^{\prime}$ and
$M\vartriangleright[\ell:[\ell;\ell^{\prime}]]$ should have the same type,
which means $R$ should contain label $\ell^{\prime}$ after the type
application of $B$. However, because $\rho_{R}\in\overline{\alpha}_{2}$, we
cannot instantiate $\rho_{R}$ to contain $\ell^{\prime}$. Besides, because
$\ell^{\prime}$ is arbitrarily chosen, it cannot already exist in $R$. Hence,
$\rho_{R}\not\in\overline{\alpha}_{2}$.

  * •

$\rho_{R}\in\overline{\alpha}_{1}$. Consider $\mathbf{case}\ M\ \\{\ell\
x\mapsto x\vartriangleright[\ell;\ell^{\prime}]\\}$ of type
$[\ell;\ell^{\prime}]$. By the type-only condition, it is translated to
(4)$\Lambda\overline{\gamma}.\mathbf{case}\ (\llbracket M\rrbracket\
\overline{C})\\{\ell\ x\mapsto\Lambda\overline{\delta}.x\ \overline{D}\\}$. By
(2) we have
$\llbracket[\ell;\ell^{\prime}]\rrbracket=\forall\overline{\alpha}^{\prime\prime}.[R^{\prime\prime}]$
where $\ell\in R^{\prime\prime}$ and $\ell^{\prime}\in R^{\prime\prime}$.
However, for  (4), by the fact that $\rho_{R}\in\overline{\alpha}_{1}$ and
$\overline{\alpha}_{1}$ are substituted by $\overline{A}$, the new row
variable of the inner variant of $M$ can only be bound in
$\overline{\alpha}^{\prime}$. Thus, in the case clause of $\ell$, we cannot
extend the variant type to contain $\ell^{\prime}$ by type application of
$\overline{D}$. Besides, because $\ell^{\prime}$ is arbitrarily chosen and the
translation is compositional, it can neither be already in the variant type or
be introduced by the type application of $\overline{C}$. Hence,
$\rho_{R}\not\in\overline{\alpha}_{1}$.

Finally, by contradiction, the translation $\llbracket-\rrbracket$ does not
exist.

∎

###  E.3. Non-Existence of Type-Only Encodings of Full Subtyping

See 5.4

###### Proof.

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$. By the type-only property, we have

$\displaystyle\llbracket f_{1}\rrbracket$
$\displaystyle=\Lambda\overline{\alpha}_{1}.\lambda
x^{A_{1}}.\Lambda\overline{\beta}_{1}.x\ \overline{B}_{1}$
$\displaystyle\llbracket f_{2}\rrbracket$
$\displaystyle=\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}$

By type preservation, they have the same type, which implies $x\
\overline{B}_{1}$ and $(\Lambda\overline{\gamma}.\langle\rangle)\
\overline{B}_{2}$ have the same type. We can further conclude that $A_{1}$
must be able to be instantiated to the empty record type $\langle\rangle$.
Thus, the only way to have type variables bound by
$\Lambda\overline{\alpha}_{1}$ in $A_{1}$ is to put them in the types of
labels which are instantiated to be absent by the type application $x\
\overline{B}_{1}$.

Then, consider another two functions
$g_{1}=f_{1}\vartriangleright(\langle\ell:\langle\rangle\rangle\to\langle\rangle)$
and $g_{2}=\lambda x^{\langle\ell:\langle\rangle\rangle}.(x.\ell)$ of the same
type $\langle\ell:\langle\rangle\rangle\to\langle\rangle$. By the type-only
property, we have

$\displaystyle\llbracket g_{1}\rrbracket$
$\displaystyle=\Lambda\overline{\alpha}.\llbracket f_{1}\rrbracket\
\overline{A}=\Lambda\overline{\alpha}.(\Lambda\overline{\alpha}_{1}.\lambda
x^{A_{1}}.\Lambda\overline{\beta}_{1}.x\ \overline{B}_{1})\ \overline{A}$
$\displaystyle\llbracket g_{2}\rrbracket$
$\displaystyle=\Lambda\overline{\alpha}^{\prime}.\lambda
x^{A^{\prime}}.\Lambda\overline{\beta}^{\prime}.\llbracket x.\ell\rrbracket\
\overline{B}^{\prime}=\Lambda\overline{\alpha}^{\prime}.\lambda
x^{A^{\prime}}.\Lambda\overline{\beta}^{\prime}.(\Lambda\overline{\gamma}^{\prime}.(x\
\overline{C}).\ell\ \overline{D})\ \overline{B}^{\prime}$

By type preservation, $\llbracket g_{1}\rrbracket$ and $\llbracket
g_{2}\rrbracket$ have the same type. The $(x\ \overline{C}).l$ in $\llbracket
g_{2}\rrbracket$ implies that $x$ has a polymorphic record type with label
$\ell$. Because $\ell$ is arbitrarily chosen, the only way to introduce $\ell$
in the parameter type of $\llbracket g_{1}\rrbracket$ is by the type
application of $\overline{A}$. However, we also have that type variables in
$\overline{\alpha}_{1}$ can only appear in the types of labels in $A_{1}$,
which means we cannot instantiate $A_{1}$ to be a polymorphic record type with
the label $\ell$ by the type application of $\overline{A}$. Contradiction.

∎