# Full Iso-recursive Types

Litao Zhou<EMAIL_ADDRESS>1234-5678-9012 The University of Hong
KongPokfulam RoadHong KongChina ,  Qianyong Wan  0009-0005-9894-2462 The
University of Hong KongPokfulam RoadHong KongChina<EMAIL_ADDRESS>and  Bruno
C. d. S. Oliveira  0000-0002-1846-7210 The University of Hong KongPokfulam
RoadHong KongChina<EMAIL_ADDRESS>
(2018; 20 February 2007; 12 March 2009; 5 June 2009)

###### Abstract.

There are two well-known formulations of recursive types: _iso-recursive_ and
_equi-recursive_ types. Abadi and Fiore (1996) have shown that iso- and equi-
recursive types have the same expressive power. However, their encoding of
equi-recursive types in terms of iso-recursive types requires explicit
coercions. These coercions come with significant additional _computational
overhead_ , and complicate reasoning about the equivalence of the two
formulations of recursive types.

This paper proposes a generalization of iso-recursive types called _full_ iso-
recursive types. Full iso-recursive types allow encoding all programs with
equi-recursive types without computational overhead. Instead of explicit term
coercions, all type transformations are captured by _computationally
irrelevant_ casts, which can be erased at runtime without affecting the
semantics of the program. Consequently, reasoning about the equivalence
between the two approaches can be greatly simplified. We present a calculus
called $\lambda^{\mu}_{Fi}$, which extends the simply typed lambda calculus
(STLC) with full iso-recursive types. The $\lambda^{\mu}_{Fi}$ calculus is
proved to be type sound, and shown to have the same expressive power as a
calculus with equi-recursive types. We also extend our results to subtyping,
and show that equi-recursive subtyping can be expressed in terms of iso-
recursive subtyping with cast operators.

Recursive types, Subtyping, Type system

††copyright: acmlicensed††journalyear: 2018††doi: XXXXXXX.XXXXXXX††journal:
JACM††journalvolume: 37††journalnumber: 4††article: 111††publicationmonth:
8††ccs: Theory of computation Type theory††ccs: Software and its engineering
Object oriented languages

##  1\. Introduction

Recursive types are used in many programming languages to express recursive
data structures, or recursive interfaces. There are two well-known
formulations of recursive types: _iso-recursive_ and _equi-recursive_ types.
With equi-recursive types (Morris, 1968), a recursive type $\mu\alpha.~{}A$
and its unfolding $A[\alpha\mapsto\mu\alpha.~{}A]$ are equal, since they
represent the same infinite tree (Amadio and Cardelli, 1993). With iso-
recursive types, a recursive type is only isomorphic to its unfolding (Crary
et al., 1999). To witness the isomorphism, explicit fold and unfold operators
are used.

Because both formulations provide alternative ways to model recursive types,
the relationship between iso- and equi-recursive types has been a topic of
study (Abadi and Fiore, 1996; Patrignani et al., 2021; Urzyczyn, 1995).
Understanding this relationship is important to answer questions such as
whether the expressive power of the two formulations is the same or not.
Urzyczyn proved that these two formulations have the same expressive power
when the types considered are restricted to be positive. Abadi and Fiore
extended Urzyczyn’s result and showed that unrestricted formulations of iso-
and equi-recursive types also have the same expressive power, leading to the
well-known statement that “iso-recursive types have the same expressive power
as equi-recursive types”. In addition, Patrignani et al. showed that the
translation from iso-recursive to equi-recursive types is fully abstract with
respect to contextual equivalence.

However, the encoding proposed by Abadi and Fiore requires explicit coercions,
which are interpreted as functions to be evaluated at runtime. Iso-recursive
types can only encode equi-recursive types with significant additional
_computational overhead_. Moreover, these explicit coercions cannot be easily
erased and therefore complicate the reasoning about _behavioral equivalence_.
To address the latter challenge, Abadi and Fiore defined an axiomatized
program logic and showed that the iso-recursive term obtained by their
encoding behaves in the same way as the original equi-recursive term in the
logic. However, the soundness of their program logic is left as a conjecture,
since they did not consider an operational semantics in their work. Thus,
behavioral equivalence between programs written with equi-recursive and iso-
recursive types lacks a complete proof in the literature. Without introducing
explicit coercions, iso-recursive types are strictly weaker than equi-
recursive types, since the infinite tree view of equi-recursive types equates
more types than isomorphic unfoldings of recursive types.

This paper proposes a _generalization_ of iso-recursive types called _full_
iso-recursive types. Full iso-recursive types overcome the challenges of
traditional iso-recursive types in achieving the typing expressiveness and
behavioral equivalence seen in equi-recursive types. Instead of fold and
unfold operators and explicit coercions, we use a more general notion of
_computationally irrelevant cast operators_ (Sulzmann et al., 2007; Cretin,
2014), which allow transformations on any types that are equivalent in an
equi-recursive setting. Full iso-recursive types can encode _all_ programs
with equi-recursive types _without_ computational overhead, since casts can be
erased at runtime without affecting the semantics of the program.
Consequently, the semantic equivalence between programs written with equi-
recursive and full iso-recursive types is also greatly simplified, and allows
for a complete proof, compared to Abadi and Fiore’s work.

We present a calculus called $\lambda^{\mu}_{Fi}$, which extends the simply
typed lambda calculus (STLC) with full iso-recursive types. The
$\lambda^{\mu}_{Fi}$ calculus is proved to be type sound, and shown to have
the same typing power as a calculus with equi-recursive types. To prove the
latter result, we define a type-directed elaboration from the calculus with
equi-recursive types to $\lambda^{\mu}_{Fi}$, and an erasure function that
removes all casts from full iso-recursive terms to obtain equi-recursive
terms. Moreover, the termination and divergence behavior of programs is
preserved under the elaboration and erasure operations. Therefore,
$\lambda^{\mu}_{Fi}$ is sound and complete w.r.t. the calculus with equi-
recursive types in terms of both typing and dynamic semantics. On the other
hand, traditional iso-recursive types can be seen as a special case of full
iso-recursive types. One can easily recover the traditional unfold and fold
operators by using the corresponding cast operators accordingly. So all the
results for iso-recursive types can be adapted to full iso-recursive types as
well.

We also extend our results to subtyping and show that equi-recursive subtyping
can be expressed in terms of iso-recursive subtyping with cast operators.
Although subtyping between equi-recursive types (Brandt and Henglein, 1998;
Amadio and Cardelli, 1993; Gapeyev et al., 2002) and subtyping between iso-
recursive types (Abadi and Cardelli, 1996; Zhou et al., 2022) has been studied
in depth respectively in the literature, the relationship between the two
approaches has been largely unexplored. We revisit Amadio and Cardelli
(1993)’s seminal work on equi-recursive subtyping and observe that an equi-
recursive subtyping relation can be decomposed into a combination of equi-
recursive equalities and an iso-recursive subtyping relation. Since our cast
operators can capture all the equi-recursive equalities, we can achieve a
simple encoding of equi-recursive subtyping in the setting of full iso-
recursive types with subtyping.

Full iso-recursive types open the path for new applications. For example, in
the design of realistic compilers, it is common to have source languages that
are lightweight in terms of type annotations; and target languages, which are
used internally, that are heavy on annotations, but are simple to type-check.
For instance, the GHC Haskell compiler works in this way: the source language
(Haskell) has a lot of convenience via type inference, and no explicit casts
are needed in source programs. A source program is then elaborated to a
variant of System Fc (Sulzmann et al., 2007), which is a System F like
language with explicit type annotations, type applications and also explicit
casts. Our work enables designing source languages with equi-recursive types,
which are elaborated to target languages with full iso-recursive types. Equi-
recursive types offer convenience because they can avoid explicit folds and
unfolds, but type-checking is complex. With full iso-recursive types we need
to write explicit casts, but type-checking is simple. Thus we can have an
architecture similar to that of GHC. In this scenario it is important that no
computational overhead is introduced during the elaboration, which is why
using standard iso-recursive types would not be practical. In addition, source
languages could also hide explicit casts into language constructs (such as
constructors, method calls and/or pattern matching). This would be another way
to use full iso-recursive types, which is similar to current applications of
iso-recursive types.

The main contributions of this paper are as follows:

  * •

Full iso-recursive types. We propose a novel formulation of recursive types,
called full iso-recursive types, which generalizes the traditional iso-
recursive fold and unfold operators to cast operators.

  * •

The $\lambda^{\mu}_{Fi}$ calculus. We introduce the $\lambda^{\mu}_{Fi}$
calculus, which extends the simply typed lambda calculus with full iso-
recursive types. The calculus is equipped with a type system, a call-by-value
operational semantics, and a type soundness proof.

  * •

Equivalence to equi-recursive types. We show that $\lambda^{\mu}_{Fi}$ is
equivalent to STLC extended with equi-recursive types in terms of typing and
dynamic semantics.

  * •

Extension to subtyping. We present $\lambda^{\mu<:}_{Fi}$, an extension of
$\lambda^{\mu}_{Fi}$ with iso-recursive subtyping, and show the same
metatheory results for $\lambda^{\mu<:}_{Fi}$, namely, type soundness, typing
equivalence and behavioral equivalence to equi-recursive types with subtyping.

  * •

Coq formalization. We provide a mechanical formalization and proofs for all
the new metatheory results of full iso-recursive types in Coq, except for
Theorem 5.5, which is adapted from the literature (Amadio and Cardelli, 1993).

##  2\. Overview

This section provides an overview of our work. We first briefly review the two
main approaches to recursive types, namely iso-recursive types and equi-
recursive types, and the relationship between the two approaches. Then we
introduce our key ideas and results.

###  2.1. Equi-recursive Types

Equi-recursive types treat recursive types and their unfoldings as equal. The
advantage of equi-recursive types is that they are simple to use, since there
is no need to insert explicit annotations in the term language to transform
between equal types, as shown in rule Typ-eq.

Typ-eq $\displaystyle\displaystyle{\hbox{\hskip
43.52415pt\vbox{\hbox{\hskip-43.52415pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:A\qquad A\doteq B$}}}\vbox{}}}\over\hbox{\hskip
19.49641pt\vbox{\vbox{}\hbox{\hskip-19.49641pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:B$}}}}}}$

The metatheory of equi-recursive types has been comprehensively studied by
Amadio and Cardelli (1993). They proposed a tree model for specifying equality
(or subtyping) between equi-recursive types. In essence, two recursive types
are equal (or subtypes) if their infinite unfoldings are equal (or in a
subtyping relation). The tree model provides a clear and solid foundation for
the interpretation of equi-recursive types.

  * $A\doteq B$ _(Equi-recursive Equality)_

Tyeq-contract $\displaystyle\displaystyle{\hbox{\hskip
125.02179pt\vbox{\hbox{\hskip-125.02179pt\hbox{\hbox{$\displaystyle\displaystyle
A[\alpha\mapsto B_{{\mathrm{1}}}]\doteq B_{{\mathrm{1}}}\qquad A[\alpha\mapsto
B_{{\mathrm{2}}}]\doteq B_{{\mathrm{2}}}\qquad A\text{ is contractive in
}\alpha$}}}\vbox{}}}\over\hbox{\hskip
16.02567pt\vbox{\vbox{}\hbox{\hskip-16.02567pt\hbox{\hbox{$\displaystyle\displaystyle
B_{{\mathrm{1}}}\doteq B_{{\mathrm{2}}}$}}}}}}$ Tyeq-unfold
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
46.72859pt\vbox{\vbox{}\hbox{\hskip-46.72858pt\hbox{\hbox{$\displaystyle\displaystyle\mu\alpha.~{}A\doteq
A[\alpha\mapsto\mu\alpha.~{}A]$}}}}}}$ Tyeq-mu-cong
$\displaystyle\displaystyle{\hbox{\hskip
14.32112pt\vbox{\hbox{\hskip-14.32112pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq B$}}}\vbox{}}}\over\hbox{\hskip
34.51796pt\vbox{\vbox{}\hbox{\hskip-34.51796pt\hbox{\hbox{$\displaystyle\displaystyle\mu\alpha.~{}A\doteq\mu\alpha.~{}B$}}}}}}$
Tyeq-trans $\displaystyle\displaystyle{\hbox{\hskip
38.8235pt\vbox{\hbox{\hskip-38.82349pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq B\qquad B\doteq C$}}}\vbox{}}}\over\hbox{\hskip
14.20897pt\vbox{\vbox{}\hbox{\hskip-14.20895pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq C$}}}}}}$ Tyeq-refl
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
14.02773pt\vbox{\vbox{}\hbox{\hskip-14.02773pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq A$}}}}}}$ Tyeq-symm $\displaystyle\displaystyle{\hbox{\hskip
14.32112pt\vbox{\hbox{\hskip-14.32112pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq B$}}}\vbox{}}}\over\hbox{\hskip
14.32112pt\vbox{\vbox{}\hbox{\hskip-14.32112pt\hbox{\hbox{$\displaystyle\displaystyle
B\doteq A$}}}}}}$ Tyeq-arr $\displaystyle\displaystyle{\hbox{\hskip
41.46455pt\vbox{\hbox{\hskip-41.46455pt\hbox{\hbox{$\displaystyle\displaystyle
A_{{\mathrm{1}}}\doteq A_{{\mathrm{2}}}\qquad B_{{\mathrm{1}}}\doteq
B_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
34.10341pt\vbox{\vbox{}\hbox{\hskip-34.10341pt\hbox{\hbox{$\displaystyle\displaystyle
A_{{\mathrm{1}}}\rightarrow B_{{\mathrm{1}}}\doteq A_{{\mathrm{2}}}\rightarrow
B_{{\mathrm{2}}}$}}}}}}$

Figure 1. Amadio and Cardelli’s equi-recursive type equality.

Amadio and Cardelli also provided a rule-based axiomatization to compare equi-
recursive types, as shown in Figure 1. They proved the soundness and
completeness of the rules to the tree-based interpretation. For example, rule
Tyeq-unfold states that a recursive type is equal to its unfolding, and rule
Tyeq-mu-cong states that the equality is congruent with respect to the
recursive type operator. Rule Tyeq-contract states that two types are equal if
they are the fixpoints of the same type function $A[\alpha]$. Note that $A$
needs to be contractive in $\alpha$, i.e. either $\alpha$ is not free in $A$
or $A$ can be unfolded to a type of the form $A_{1}\rightarrow A_{2}$. This is
to prevent equating arbitrary types using non-contractive type functions, such
as when $A$ is $\alpha$. Rule Tyeq-contract allows recursive types that have
equal infinite unfoldings, but are not directly related by finite unfoldings,
to be equal. For example, let
$A[\alpha]=\texttt{Int}\to\texttt{Int}\to\alpha$, then
$B_{1}=\mu\alpha.\texttt{Int}\to\alpha$ and
$B_{2}=\mu\alpha.\texttt{Int}\to\texttt{Int}\to\alpha$ are equal according to
rule Tyeq-contract:

… $B_{1}\doteq A[\alpha\mapsto B_{1}]$ Tyeq-unfold $B_{2}\doteq
A[\alpha\mapsto B_{2}]$ $A\text{ is contractive in }\alpha$ Tyeq-contract
$\mu\alpha.\texttt{Int}\to\alpha\doteq\mu\alpha.\texttt{Int}\to\texttt{Int}\to\alpha$

Here, the missing derivation is:

Tyeq-refl $\texttt{Int}\doteq\texttt{Int}$ Tyeq-unfold
$\mu\alpha.~{}\texttt{Int}\to\alpha\doteq\texttt{Int}\to\mu\alpha.~{}\texttt{Int}\to\alpha$
Tyeq-arrow $\texttt{Int}\to B_{1}\doteq\texttt{Int}\to\texttt{Int}\to B_{1}$
Tyeq-trans and Tyeq-unfold $B_{1}\doteq A[\alpha\mapsto B_{1}]$

Despite its equivalence to the tree model, Amadio and Cardelli’s
axiomatization is not easy to use in practice. In particular one needs to find
a generating type function $A[\alpha]$ in rule Tyeq-contract. Later on, there
have been a few alternative axiomatizations of equi-recursive types (Brandt
and Henglein, 1998; Danielsson and Altenkirch, 2010; Gapeyev et al., 2002),
which are all proved to be equivalent to the tree model. Among them, Brandt
and Henglein proposed an inductively defined relation $H\vdash A\doteq B$ for
equi-recursive type equality, shown in Figure 2. $H$ is a list of type
equality assumptions that can be used to derive the equality $A\doteq B$. New
equalities are added to $H$ every time function types are compared, as shown
in rule Tye-arrfix. Compared to rule Tyeq-contract, rule Tye-arrfix encodes
the coinductive essence of equi-recursive types in a simpler way. Therefore,
we choose Brandt and Henglein’s axiomatization as the basis for our work.

  * $H\vdash A\doteq B$ _(Inductive Equi-recursive Equality)_

Tye-assump $\displaystyle\displaystyle{\hbox{\hskip
25.13356pt\vbox{\hbox{\hskip-25.13356pt\hbox{\hbox{$\displaystyle\displaystyle
A=B\in H$}}}\vbox{}}}\over\hbox{\hskip
24.71687pt\vbox{\vbox{}\hbox{\hskip-24.71687pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash A\doteq B$}}}}}}$ Tye-refl
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
24.42348pt\vbox{\vbox{}\hbox{\hskip-24.42348pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash A\doteq A$}}}}}}$ Tye-trans $\displaystyle\displaystyle{\hbox{\hskip
59.615pt\vbox{\hbox{\hskip-59.61499pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash A\doteq B\qquad H\vdash B\doteq C$}}}\vbox{}}}\over\hbox{\hskip
24.60472pt\vbox{\vbox{}\hbox{\hskip-24.6047pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash A\doteq C$}}}}}}$ Tye-unfold
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
57.12434pt\vbox{\vbox{}\hbox{\hskip-57.12433pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash\mu\alpha.~{}A\doteq A[\alpha\mapsto\mu\alpha.~{}A]$}}}}}}$ Tye-symm
$\displaystyle\displaystyle{\hbox{\hskip
24.71687pt\vbox{\hbox{\hskip-24.71687pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash A\doteq B$}}}\vbox{}}}\over\hbox{\hskip
24.71687pt\vbox{\vbox{}\hbox{\hskip-24.71687pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash B\doteq A$}}}}}}$ Tye-arrfix $\displaystyle\displaystyle{\hbox{\hskip
131.85184pt\vbox{\hbox{\hskip-131.85182pt\hbox{\hbox{$\displaystyle\displaystyle
H,A_{{\mathrm{1}}}\rightarrow B_{{\mathrm{1}}}=A_{{\mathrm{2}}}\rightarrow
B_{{\mathrm{2}}}\vdash A_{{\mathrm{1}}}\doteq A_{{\mathrm{2}}}\qquad
H,A_{{\mathrm{1}}}\rightarrow B_{{\mathrm{1}}}=A_{{\mathrm{2}}}\rightarrow
B_{{\mathrm{2}}}\vdash B_{{\mathrm{1}}}\doteq
B_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
44.49916pt\vbox{\vbox{}\hbox{\hskip-44.49916pt\hbox{\hbox{$\displaystyle\displaystyle
H\vdash A_{{\mathrm{1}}}\rightarrow B_{{\mathrm{1}}}\doteq
A_{{\mathrm{2}}}\rightarrow B_{{\mathrm{2}}}$}}}}}}$

Figure 2. Brandt and Henglein’s inductively defined equi-recursive type
equality.

###  2.2. Iso-recursive Types

Iso-recursive types (Crary et al., 1999) are a different approach that treats
recursive types and their unfoldings as different, but isomorphic up to an
unfold/fold operator. With iso-recursive types foldings and unfoldings of the
recursive types must be explicitly triggered, and there is no typing rule Typ-
eq to implicitly convert between equivalent types. Rule Typ-unfold and rule
Typ-fold show the typing rules for unfolding and folding a term of recursive
types. A fold expression constructs a recursive type, while an unfold
expression opens a recursive type to its unfolding.

Typ-unfold $\displaystyle\displaystyle{\hbox{\hskip
29.30144pt\vbox{\hbox{\hskip-29.30144pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:\mu\alpha.~{}A$}}}\vbox{}}}\over\hbox{\hskip
72.45949pt\vbox{\vbox{}\hbox{\hskip-72.45949pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{unfold}\,[\mu\alpha.~{}A]\,e:A[\alpha\mapsto\mu\alpha.~{}A]$}}}}}}$
Typ-fold $\displaystyle\displaystyle{\hbox{\hskip
41.80547pt\vbox{\hbox{\hskip-41.80545pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:A[\alpha\mapsto\mu\alpha.~{}A]$}}}\vbox{}}}\over\hbox{\hskip
54.3999pt\vbox{\vbox{}\hbox{\hskip-54.39989pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{fold}\,[\mu\alpha.~{}A]\,e:\mu\alpha.~{}A$}}}}}}$

One advantage of iso-recursive types is that they are easier to extend to more
complex type systems, which may easily make the type equality relation
undecidable. Instead, iso-recursive types provide explicit control over
folding and unfolding, avoiding issues with undecidability. One disadvantage
of iso-recursive types is their inconvenience in use due to the explicit fold
and unfold operators. However, this disadvantage can be mitigated by hiding
folding and unfolding under other language constructs, such as pattern
matching, constructors or method calls (Crary et al., 1999; Lee et al., 2015;
Zhou et al., 2022; Pierce, 2002; Harper and Stone, 2000; Vanderwaart et al.,
2003; Yang and Oliveira, 2019). As we shall see in Section 2.3, a further
disadvantage of iso-recursive types is that folding and unfolding alone is not
enough to provide all of the expressive power of the type equality rules. In
some cases, explicit, computationally relevant, term coercions are necessary.

###  2.3. Relating Iso-recursive and Equi-recursive Types

The relationship between iso-recursive types and equi-recursive types has been
a subject of study for a long time on the literature of recursive types (Abadi
and Fiore, 1996; Patrignani et al., 2021; Urzyczyn, 1995). This subsection
reviews the existing approaches to relate the two approaches and their issues.

#### Encoding iso-recursive types.

The encoding of iso-recursive types in equi-recursive types is
straightforward, simply by erasing the fold and unfold operators (Abadi and
Fiore, 1996). Since the rule Tyeq-unfold states that a recursive type is equal
to its unfolding, it is easy to see that the encoding is type preserving. The
encoding is also behavior preserving, since the reduction rules with fold and
unfold operators will become no-ops when erased, as shown below:

Red-fld $\displaystyle\displaystyle{\hbox{\hskip
11.95398pt\vbox{\hbox{\hskip-11.95396pt\hbox{\hbox{$\displaystyle\displaystyle
e\hookrightarrow e^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
43.34291pt\vbox{\vbox{}\hbox{\hskip-43.3429pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{fold}\,[A]\,e\hookrightarrow\textsf{fold}\,[A]\,e^{\prime}$}}}}}}$
Red-ufd $\displaystyle\displaystyle{\hbox{\hskip
11.95398pt\vbox{\hbox{\hskip-11.95396pt\hbox{\hbox{$\displaystyle\displaystyle
e\hookrightarrow e^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
54.45406pt\vbox{\vbox{}\hbox{\hskip-54.45404pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{unfold}\,[A]\,e\hookrightarrow\textsf{unfold}\,[A]\,e^{\prime}$}}}}}}$
Red-elim $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
54.24937pt\vbox{\vbox{}\hbox{\hskip-54.24937pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{unfold}\,[A]\,(\textsf{fold}\,[B]\,v)\hookrightarrow
v$}}}}}}$

Notice that in the process of reducing folded and unfolded expression $e$, we
merely reduce $e$. The type $A$ does not influence the reduction of $e$.
Eventually, when $e$ reaches a value $v$, an unfold cancels a fold and we
simply obtain $v$. In other words, folding and unfolding are _computationally
irrelevant_ : they do not influence the runtime result, and can be erased, to
avoid runtime costs. Moreover, Patrignani et al. (2021) proved that the
erasure operation is fully abstract, i.e. two terms that cannot be
distinguished by any program contexts in the iso-recursive setting are also
indistinguishable in the equi-recursive setting.

#### Encoding equi-recursive types via fold and unfold

It takes more effort to encode equi-recursive types in terms of iso-recursive
types. Since equi-recursive types treat recursive types and their unfoldings
as equal, we need to insert explicit fold and unfold operators in the iso-
recursive setting to transform between equal types. For example, let $e$ be a
function that keeps taking integer arguments and returning itself, which can
be typed as a recursive type $\mu\alpha.~{}\texttt{Int}\to\alpha$. In an equi-
recursive setting, $(e\,1)$ can be typed as
$\mu\alpha.~{}\texttt{Int}\to\alpha$, by using the rule Typ-eq and rule Tyeq-
unfold to unfold the recursive type to
$\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$ so that it can be
applied to the argument $1$. However, in the iso-recursive setting, we need to
insert an unfold operator to make the transformation explicit, as shown in the
following derivation:

$\vdash e:\mu\alpha.~{}\texttt{Int}\to\alpha$ Typ-unfold
$\vdash\textsf{unfold}\,[\mu\alpha.~{}\texttt{Int}\to\alpha]\,e:\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$
$\vdash 1:\texttt{Int}$ Typ-app
$\vdash(\textsf{unfold}\,[\mu\alpha.~{}\texttt{Int}\to\alpha]\,e)\,1:\mu\alpha.~{}\texttt{Int}\to\alpha$

#### Fold/unfold is not enough: computationally relevant explicit coercions

The above example shows that, for some equi-recursive terms, inserting fold
and unfold operators within the term language can achieve an encoding in terms
of iso-recursive types. However, this is not always the case. Recall that
$\mu\alpha.~{}\texttt{Int}\to\alpha$ and
$\mu\alpha.~{}\texttt{Int}\to\texttt{Int}\to\alpha$ are also equal in the
equi-recursive setting, but they are not directly related by fold and unfold
operators. To address this issue, Abadi and Fiore (1996) proposed an approach
to insert _explicit coercion functions_. They showed that, for any two equi-
recursive types $A$ and $B$ considered to be equal following the derivation in
Figure 1, there exists a coercion function $f:A\to B$ that can be applied to
terms of type $A$ to obtain terms of type $B$. With the coercion function,
terms that are well typed by rule Typ-tyeq can now have an encoding in terms
of iso-recursive types, possibly with the help of explicit coercion functions.

One issue is that the insertion of coercion functions affects the
computational structure of the terms. For example, assume that $e$ has a
function type
$\texttt{Int}\to\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$. This
type can be partially folded to
$\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$. In an equi-recursive
setting, due to the rule Typ-eq, the term $e$ can also be assigned the type
$\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$, without any changes. In
an iso-recursive setting, in addition to folding and unfolding, we need
explicit coercions. The coercion function for this transformation is

$\lambda(x:\texttt{Int}\to\texttt{Int}\to\mu\alpha.~{}\texttt{Int}\to\alpha).~{}\lambda(y:\texttt{Int}).~{}\textsf{fold}\,[\mu\alpha.~{}\texttt{Int}\to\alpha]\,(x\,y)$

Now, applying the coercion function to $e$ results in a term of type
$\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$. Unfortunately, such
explicit coercion functions are computationally relevant. Thus, an encoding of
equi-recursive types in terms of iso-recursive types can introduce non-trivial
computational overhead. The issue is particularly problematic because some
coercions need to essentially be _recursive_ functions. Therefore, it is
impractical to use such an encoding in a language implementation.

#### Issues with reasoning

Explicit coercions also bring new challenges in terms of reasoning, and in
particular in proving the behavioral preservation of the encoding. Continuing
with the previous example, if we transform this resulting term back to an
equi-recursive setting, by erasing the fold and unfold operators, we will get
a term:

(1)
$(\lambda(x:\texttt{Int}\to\texttt{Int}\to\mu\alpha.~{}\texttt{Int}\to\alpha).~{}\lambda(y:\texttt{Int}).~{}(x\,y))\,e$

This term is equivalent to $e$ under $\beta-$ and $\eta-$reduction, but it is
not the same as $e$ anymore. In more complicated cases, especially for
derivations involving the use of rule Tyeq-contract, the insertion of coercion
functions can lead to a significant change in the syntactic structure of the
terms, which makes it difficult to reason about the behavior preservation of
the encoding. In essence, with the rule Tyeq-contract, one needs to encode
special iterating functions to model the fixpoint of a type function. Abadi
and Fiore proved that the encoding is equivalent to the original term in an
axiomatized program logic, but the soundness of the program logic is
conjectured to be sound, and the authors did not consider an operational
semantics. Thus, while it is expected that the behavioral equivalence result
holds (assuming the conjecture and a suitable operational semantics), there is
no complete proof in the literature for this result.

###  2.4. Subtyping

#### Equi-recursive subtyping

It is common to extend recursive types with subtyping. For equi-recursive
types, Amadio and Cardelli proposed a set of rules, which relies on the
equality relation in Figure 1. We show some selected rules below:

ACSub-eq $\displaystyle\displaystyle{\hbox{\hskip
14.32112pt\vbox{\hbox{\hskip-14.32112pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq B$}}}\vbox{}}}\over\hbox{\hskip
23.9044pt\vbox{\vbox{}\hbox{\hskip-23.9044pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A\leq B$}}}}}}$ ACSub-arrow $\displaystyle\displaystyle{\hbox{\hskip
60.63112pt\vbox{\hbox{\hskip-60.63112pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
B_{{\mathrm{1}}}\leq A_{{\mathrm{1}}}\qquad\Sigma\vdash A_{{\mathrm{2}}}\leq
B_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
43.68669pt\vbox{\vbox{}\hbox{\hskip-43.68669pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A_{{\mathrm{1}}}\rightarrow A_{{\mathrm{2}}}\leq B_{{\mathrm{1}}}\rightarrow
B_{{\mathrm{2}}}$}}}}}}$ ACSub-rec $\displaystyle\displaystyle{\hbox{\hskip
38.81985pt\vbox{\hbox{\hskip-38.81985pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma,\alpha\leq\beta\vdash
A\leq B$}}}\vbox{}}}\over\hbox{\hskip
43.73087pt\vbox{\vbox{}\hbox{\hskip-43.73085pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\mu\alpha.~{}A\leq\mu\beta.~{}B$}}}}}}$
ACSub-var $\displaystyle\displaystyle{\hbox{\hskip
22.41542pt\vbox{\hbox{\hskip-22.4154pt\hbox{\hbox{$\displaystyle\displaystyle\alpha\leq\beta\in\Sigma$}}}\vbox{}}}\over\hbox{\hskip
22.13763pt\vbox{\vbox{}\hbox{\hskip-22.13762pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\alpha\leq\beta$}}}}}}$

Two types are in a subtyping relation if their infinite unfoldings are equal,
as shown in rule ACSub-eq. The subtyping relation is structural, as can be
seen in rule ACSub-arrow. For dealing with recursive types, rule ACSub-rec
states that two recursive types are in a subtyping relation if their recursive
bodies are subtypes, when assuming that the recursive variable of the two
types are in a subtyping relation. The subtyping rules are also referred to as
the Amber rules, since rule ACSub-rec is adopted by the implementation of the
Amber programming language (Cardelli, 1985). The Amber rules are proved to be
sound and complete to the tree model interpretation of equi-recursive
subtyping (Amadio and Cardelli, 1993).

#### Iso-recursive subtyping

For iso-recursive types, one can replace the equi-recursive equality relation
in rule ACSub-eq with the syntactic equality relation to obtain the iso-
recursive style Amber rules. The iso-recursive Amber rules are well-known and
widely used for subtyping iso-recursive types (Abadi and Cardelli, 1996;
Bengtson et al., 2011; Chugh, 2015; Lee et al., 2015; Swamy et al., 2011;
Duggan, 2002). However, the metatheory for the iso-recursive Amber rules has
not been well studied until recently (Zhou et al., 2022, 2020). Zhou et al.
provided a new specification for iso-recursive subtyping and proved a number
of metatheory results, including type soundness, transitivity of the subtyping
relation, and equivalence to the iso-recursive Amber rules.

However, unlike type equality, the relation between equi-recursive and iso-
recursive subtyping has been less studied. One attempt that we are aware of is
the work by Ligatti et al. (2017). They provided an extension of the iso-
recursive subtyping rules to allow for subtyping between recursive types and
their unfoldings, but their rules cannot account for the full expressiveness
of equi-recursive subtyping. For example,
$\mu\alpha.~{}\texttt{Int}\to\alpha\leq\mu\alpha.~{}\texttt{Int}\to\texttt{Int}\to\alpha$
is a valid subtyping relation in the equi-recursive Amber rules using rule
ACSub-eq, but it is not derivable in Ligatti et al.’s rules.

###  2.5. Key Ideas and Results

As we have shown, encoding iso-recursive types with equi-recursive types is
simple. As for the other direction, Abadi and Fiore showed that iso-recursive
types can be encoded with equi-recursive types, which leads to a well-known
statement that “iso-recursive types have the same expressive power as equi-
recursive types”. However, their encoding involves the insertion of explicit
coercion functions, and lacks a complete proof of correctness. In our work, we
present a novel approach to iso-recursive types, full iso-recursive types,
which extends the unfold and fold operators to a more general form. We show
that full iso-recursive types and equi-recursive types can be mutually encoded
and the encoding preserves the semantic behavior. Compared to the previous
work, the correctness proof of our encoding is straightforward and
foundational, without relying on any a priori assumptions.

#### Type Casting.

The key idea of our approach is the introduction of a type casting relation
that generalizes the unfold and fold operators. Instead of allowing only the
unfold and fold operators to transform between recursive types and their
unfoldings, we allow terms of any type to be transformed to their equivalent
type using the type casting relation. The rules Typ-unfold and Typ-fold are
now replaced by the following rule:

Typ-cast $\displaystyle\displaystyle{\hbox{\hskip
59.57672pt\vbox{\hbox{\hskip-59.5767pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:A\qquad\cdot;\cdot\vdash A\hookrightarrow B:c$}}}\vbox{}}}\over\hbox{\hskip
33.35466pt\vbox{\vbox{}\hbox{\hskip-33.35464pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{cast}\,[c]\,e:B$}}}}}}$

The type casting relation $A\hookrightarrow B:c$ states that type $A$ can be
cast to type $B$ using the casting operator $c$. Essentially, the type casting
relation is an equivalent form of Brandt and Henglein’s type equality
relation, augmented with a casting operator $c$, a new syntactic construct to
witness the proof of the type casting relation. As we will show in the
following sections, the type casting relation is not a simple extension of
Figure 2. For example, we remove the rule Tye-symm from the type casting
relation, which is hard to interpret in the operational semantics, and proved
that it is admissible from the remaining rules. After resolving these issues,
it is easy to encode the equi-recursive rule Typ-eq using the type casting
relation in rule Typ-cast. For instance, the encoding in (1) can now be
replaced by the following term:

$\textsf{cast}\,[\textsf{id}\to\textsf{fold}_{(\mu\alpha.~{}\texttt{Int}\to\alpha)}]\,e$

Here id is the identity casting operator, and
$\textsf{fold}_{\mu\alpha.~{}\texttt{Int}\to\alpha}$ is the casting operator
that witnesses the proof of a folding from
$\texttt{Int}\to(\mu\alpha.~{}\texttt{Int}\to\alpha)$ to
$\mu\alpha.~{}\texttt{Int}\to\alpha$. Thus, the full iso-recursive typing
rules are equivalent to the equi-recursive typing rules.

On the other hand, the unfolding and folding operators in standard iso-
recursive types can be recovered from our type casting relation. For example,
the term $(\textsf{cast}\,[\textsf{fold}_{A}]\,e)$ is essentially equivalent
to $(\textsf{fold}\,[A]\,e)$, and the term
$(\textsf{cast}\,[\textsf{unfold}_{A}]\,e)$ is equivalent to
$(\textsf{unfold}\,[A]\,e)$ in terms of typing and dynamic semantics, as we
will show in the following sections. Therefore, full iso-recursive types are a
generalization of standard iso-recursive types.

#### Push Rules.

The extension of the typing rules brings new challenges to the design of
semantics and the proof of type soundness. With the casting operator, there
can be terms that are not simple unfoldings or foldings of recursive types,
and the operational semantics needs to be extended to handle these terms. For
example, terms such as
$(\textsf{cast}\,[\textsf{id}\to\textsf{fold}_{(\mu\alpha.~{}\texttt{Int}\to\alpha)}]\,e)$,
which have no analogous representation in calculi with standard iso-recursive
types, need to be considered during reduction. To address this issue, we
introduce a set of new reduction rules to handle casting operators:

$\begin{array}[]{c}\text{$\raise
0.0pt\hbox{${\vbox{\hbox{\hbox{\small\small{{\hypertarget{ottalt:rule:ott:Red-
cast}{{{Red-cast}}} }{}}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
11.95398pt\vbox{\hbox{\hskip-11.95396pt\hbox{\hbox{$\displaystyle\displaystyle
e\hookrightarrow e^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
41.05931pt\vbox{\vbox{}\hbox{\hskip-41.0593pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[c]\,e\hookrightarrow\textsf{cast}\,[c]\,e^{\prime}$}}}}}}$}}}\hbox{}$
}$ }\quad\text{$\raise
0.0pt\hbox{${\vbox{\hbox{\hbox{\small\small{{\hypertarget{ottalt:rule:ott:Red-
cast-id}{{{Red-cast-id}}}
}{}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
28.98372pt\vbox{\vbox{}\hbox{\hskip-28.9837pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[\textsf{id}]\,v\hookrightarrow
v$}}}}}}$}}}\hbox{}$ }$ }\\\ \\\ \text{$\raise
0.0pt\hbox{${\vbox{\hbox{\hbox{\small\small{{\hypertarget{ottalt:rule:ott:Red-
cast-arr}{{{Red-cast-arr}}}
}{}}}}\hbox{$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
94.65594pt\vbox{\vbox{}\hbox{\hskip-94.65593pt\hbox{\hbox{$\displaystyle\displaystyle(\textsf{cast}\,[c_{{\mathrm{1}}}\rightarrow
c_{{\mathrm{2}}}]\,v_{{\mathrm{1}}})\,v_{{\mathrm{2}}}\hookrightarrow\textsf{cast}\,[c_{{\mathrm{2}}}]\,(v_{{\mathrm{1}}}\,(\textsf{cast}\,[\neg
c_{{\mathrm{1}}}]\,v_{{\mathrm{2}}}))$}}}}}}$}}}\hbox{}$ }$ }\\\ \end{array}$

The reduction rules are designed in a call-by-value fashion, and we also
define the cast of values of function types (i.e. $\textsf{cast}\,[c_{1}\to
c_{2}]\,v$) as values. The new reduction rules in our system are referred to
as _push_ rules, since they push the casting operators inside the terms to
make the terms more reducible, as shown in rule Red-Cast-Arr. Our design is
inspired by the homonymous push rules in the design of calculi with coercions
(Cretin, 2014; Sulzmann et al., 2007). Note that the casting operator $\neg
c_{1}$ computes the dual of the casting operator $c_{1}$, which is used to
indicate the reverse transformation that $c_{1}$ represents. This operation is
necessary to ensure that the reduction is type preserving, since applying a
casting operator to the expected input type of a function is essentially
equivalent to applying the reverse casting to the actual input argument. A
running example of a reduction using the push rules is shown as follows:

$\begin{array}[]{rll}&(\textsf{cast}\,[\textsf{id}\to\textsf{fold}_{(\mu\alpha.~{}\texttt{Int}\to\alpha)}]\,v)\,1\\\
\hookrightarrow&\textsf{cast}\,[\textsf{fold}_{(\mu\alpha.~{}\texttt{Int}\to\alpha)}]\,(v\,(\textsf{cast}\,[\textsf{id}]\,1))&(\text{{\hyperlink{ottalt:rule:ott:Red-
cast-arr}{{{{Red-cast-arr}}}}}})\\\
\hookrightarrow&\textsf{cast}\,[\textsf{fold}_{(\mu\alpha.~{}\texttt{Int}\to\alpha)}]\,(v\,1)&(\text{{\hyperlink{ottalt:rule:ott:Red-
cast-id}{{{{Red-cast-id}}}}} and {\hyperlink{ottalt:rule:ott:Red-cast}{{{{Red-
cast}}}}}})\end{array}$

One of the key results of our work is the type soundness of the full iso-
recursive calculus, which is proved by showing that the push rules preserve
the type of the terms and the type casting relation. This is one step beyond
Brandt and Henglein’s work, in which a coercion typing rule similar to our
casting rules was introduced, but no results about the dynamic semantics were
studied. Another contribution of our work is that with full iso-recursive
types, we retain the computational structure of the terms when encoding equi-
recursive types. In other words, erasing the casting operators from the terms
will result in the original terms, which is not the case for the previous work
(Abadi and Fiore, 1996). Our casts are _computationally irrelevant_ , and
unlike regular iso-recursive types, which require computationally relevant
term coercions for some type conversions, no such coercions are needed in our
approach. For example, all the reduction steps in the example above are erased
to the original term $(v\,1)$. This round-tripping property simplifies the
correctness reasoning of the encoding.

We show that all the terms that are well-typed in the equi-recursive setting
can be encoded in the full iso-recursive setting. Furthermore, the encoding is
behavior preserving, i.e. evaluating the encoded terms will result in a value
that is equal to the value of the original equi-recursive term up to erasure.
In this sense, we get back a fully verified statement that _“full iso-
recursive types have the same expressive power as equi-recursive types”_.

#### Subtyping

Our results extend to subtyping. Our main observation for subtyping is to show
that the equi-recursive subtyping relation can be defined by a combination of
equi-recursive equality and the iso-recursive subtyping relation (Cardelli,
1985; Abadi and Cardelli, 1996; Zhou et al., 2022), as shown below:

$A\leq_{e}B\triangleq\exists\,C_{1}\,C_{2}.~{}(A\doteq
C_{1})\land(C_{1}\leq_{i}C_{2})\land(C_{2}\doteq B)$

Here $\leq_{e}$ denotes an equi-recursive subtyping relation, and $\leq_{i}$
denotes an iso-recursive subtyping relation. This alternative definition of
equi-recursive subtyping is implicitly implied from Amadio and Cardelli’s
work, but it is somewhat hidden behind their proofs and definitions. We
reinterpret their proofs and definitions to highlight that this alternative
definition is equivalent to existing equi-recursive subtyping definitions in
the literature.

This alternative definition of equi-recursive subtyping is important because
we can reuse the existing type casting relation in the full iso-recursive
setting with subtyping. For example, given an equi-recursive term $e$ that has
the type $A$ with $A\leq_{e}B$, we can encode $e:B$ in the full iso-recursive
setting as
$((\textsf{cast}\,[c_{2}]\,(\textsf{cast}\,[c_{1}]\,e^{\prime})):B)$, in which
$c_{1}$ and $c_{2}$ are casts encoding the equality relation $A\doteq C_{1}$
and $C_{2}\doteq B$, and $e^{\prime}$ is the encoding of $(e:A)$. This term
type checks with the iso-recursive subtyping relation.

Our encoding is still computationally irrelevant in the presence of subtyping.
Thus, all the results – including type soundness, well-typed encoding, and
behavior preservation – are also applicable to the system with subtyping. This
is a significant improvement over previous work (Abadi and Fiore, 1996), which
has not studied the relationship between equi-recursive and iso-recursive
subtyping.

##  3\. A calculus with full iso-recursive types

In this section we will introduce a calculus with full iso-recursive types,
called $\lambda^{\mu}_{Fi}$. Our calculus is based on the simply typed lambda
calculus extended with recursive types and type cast operators.

###  3.1. Syntax and Well-formedness

The syntax of $\lambda^{\mu}_{Fi}$ is shown at the top of Figure 3.

Types | $A,B$ | $\Coloneqq$ | $\texttt{Int}\mid A_{1}\to A_{2}\mid\alpha\mid\mu\alpha.~{}A$
---|---|---|---
Expressions | $e$ | $\Coloneqq$ | $x\mid\textsf{n}\mid e_{1}~{}e_{2}\mid\lambda x:A.~{}e\mid\textsf{cast}\,[c]\,e$
Values | $v$ | $\Coloneqq$ | $\textsf{n}\mid\lambda x:A.~{}e\mid\textsf{cast}\,[\textsf{fold}_{A}]\,v\mid\textsf{cast}\,[c_{1}\to c_{2}]\,v$
Cast Operators | $c$ | $\Coloneqq$ | $\iota\mid\textsf{id}\mid\textsf{fold}_{A}\mid\textsf{unfold}_{A}\mid c_{1}\to c_{2}\mid c_{1};c_{2}\mid\textsf{fix}\,{\iota}.~{}c$
Type Contexts | $\Delta$ | $\Coloneqq$ | $\cdot\mid\Delta,\alpha$
Typing Contexts | $\Gamma$ | $\Coloneqq$ | $\cdot\mid\Gamma,x:A$
Type Cast Contexts | $\mathbb{E}$ | $\Coloneqq$ | $\cdot\mid\mathbb{E},\iota:A\hookrightarrow B$

  * $\Delta\vdash\textit{A}$ _(Well-formed Type)_

WFT-int $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
15.0pt\vbox{\vbox{}\hbox{\hskip-14.99998pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mathsf{Int}$}}}}}}$
WFT-var $\displaystyle\displaystyle{\hbox{\hskip
13.47624pt\vbox{\hbox{\hskip-13.47624pt\hbox{\hbox{$\displaystyle\displaystyle\alpha\in\Delta$}}}\vbox{}}}\over\hbox{\hskip
13.19846pt\vbox{\vbox{}\hbox{\hskip-13.19846pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\alpha$}}}}}}$
WFT-arrow $\displaystyle\displaystyle{\hbox{\hskip
37.79332pt\vbox{\hbox{\hskip-37.79332pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
A\qquad\Delta\vdash B$}}}\vbox{}}}\over\hbox{\hskip
23.07108pt\vbox{\vbox{}\hbox{\hskip-23.07108pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
A\rightarrow B$}}}}}}$ WFT-rec $\displaystyle\displaystyle{\hbox{\hskip
19.17067pt\vbox{\hbox{\hskip-19.17067pt\hbox{\hbox{$\displaystyle\displaystyle\Delta,\alpha\vdash
A$}}}\vbox{}}}\over\hbox{\hskip
23.84837pt\vbox{\vbox{}\hbox{\hskip-23.84837pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mu\alpha.~{}A$}}}}}}$

Figure 3. Syntax and type well-formedness of $\lambda^{\mu}_{Fi}$.

#### Types.

Meta-variables $A,B$ range over types. Types include base types (Int),
function types ($A_{1}\to A_{2}$), type variables ($\alpha$), and recursive
types ($\mu\alpha.~{}A$).

#### Expressions.

Meta-variables $e$ range over expressions. Most of the expressions are
standard, including: variables ($x$), integers (n), applications
($e_{1}~{}e_{2}$) and lambda abstractions ($\lambda x:A.~{}e$). We also have a
type cast operator ($\textsf{cast}\,[c]\,e$) that transforms the type of the
expression $e$ to an equivalent type using the cast operator $c$. The cast
operators $c$ include cast variables ($\iota$), the identity cast (id), the
fold and unfold casts ($\textsf{fold}_{A}$ and $\textsf{unfold}_{A}$), the
arrow cast ($c_{1}\to c_{2}$), the sequential cast ($c_{1};c_{2}$), and the
fixpoint cast ($\textsf{fix}\,{\iota}.~{}c$). We will define the type cast
rules for these operators in §3.2.

#### Values.

Meta-variables $v$ range over values. Integers (n) and lambda abstractions
($\lambda x:A.~{}e$), are considered as values, which are standard for a
simply typed lambda calculus. In standard iso-recursive types, the folding of
a value ($\textsf{fold}\,[A]\,v$) is a value. Therefore in our calculus its
corresponding encoding ($\textsf{cast}\,[\textsf{fold}_{A}]\,v$) is also
considered a value. We also consider arrow casts of a value
($\textsf{cast}\,[c_{1}\to c_{2}]\,v$) to be values, since they cannot be
reduced further.

#### Contexts and Well-formedness

Type contexts $\Delta$ track the bound type variables $\alpha$. A type is
well-formed if all of its free variables are in the context. The well-
formedness rules for types are standard, and shown at the bottom Figure 3.
Typing contexts $\Gamma$ track the bound variables $x$ with their types. A
typing context is well-formed ($\vdash\Gamma$) if there are no duplicate
variables and all the types are well-formed. We also define a type cast
context $\mathbb{E}$ to keep track of the cast variables $\iota$ and the cast
operators that they are associated with. This will be used in the type cast
rules, which we will define in §3.2.

For type variables and term variables, we assume the usual notions of free and
bound variables, and the usual capture-avoiding substitution function, denoted
by $A[\alpha\mapsto B]$, that replaces the free occurrences of variable
$\alpha$ in $A$ by $B$, while avoiding the capture of any bound variable in
$A$. When needed, we assume that $\alpha$-equivalence is applied at will to
avoid the clashing of free variables.

  * $\Gamma\vdash e:\textit{A}$ _(Typing)_

Typ-int $\displaystyle\displaystyle{\hbox{\hskip
8.95828pt\vbox{\hbox{\hskip-8.95827pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
21.1261pt\vbox{\vbox{}\hbox{\hskip-21.1261pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
n:\mathsf{Int}$}}}}}}$ Typ-var $\displaystyle\displaystyle{\hbox{\hskip
39.02763pt\vbox{\hbox{\hskip-39.02763pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma\qquad\mathit{x}:A\,\in\,\Gamma$}}}\vbox{}}}\over\hbox{\hskip
16.73608pt\vbox{\vbox{}\hbox{\hskip-16.73607pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{x}:A$}}}}}}$
Typ-abs $\displaystyle\displaystyle{\hbox{\hskip
30.61417pt\vbox{\hbox{\hskip-30.61415pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\mathit{x}:A_{{\mathrm{1}}}\vdash
e:A_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
46.18076pt\vbox{\vbox{}\hbox{\hskip-46.18074pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\lambda\mathit{x}:A_{{\mathrm{1}}}.\,e:A_{{\mathrm{1}}}\rightarrow
A_{{\mathrm{2}}}$}}}}}}$ Typ-app $\displaystyle\displaystyle{\hbox{\hskip
60.26723pt\vbox{\hbox{\hskip-60.26721pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e_{{\mathrm{1}}}:A_{{\mathrm{1}}}\rightarrow
A_{{\mathrm{2}}}\qquad\Gamma\vdash
e_{{\mathrm{2}}}:A_{{\mathrm{1}}}$}}}\vbox{}}}\over\hbox{\hskip
25.17561pt\vbox{\vbox{}\hbox{\hskip-25.17561pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}:A_{{\mathrm{2}}}$}}}}}}$ Typ-cast
$\displaystyle\displaystyle{\hbox{\hskip
59.57672pt\vbox{\hbox{\hskip-59.5767pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:A\qquad\cdot;\cdot\vdash A\hookrightarrow B:c$}}}\vbox{}}}\over\hbox{\hskip
33.35466pt\vbox{\vbox{}\hbox{\hskip-33.35464pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\textsf{cast}\,[c]\,e:B$}}}}}}$

  * $\Delta;\mathbb{E}\vdash\textit{A}\hookrightarrow\textit{B}:c$ _(Type Casting)_

Cast-id $\displaystyle\displaystyle{\hbox{\hskip
31.59717pt\vbox{\hbox{\hskip-31.59717pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
A\qquad\vdash\mathbb{E}$}}}\vbox{}}}\over\hbox{\hskip
34.37492pt\vbox{\vbox{}\hbox{\hskip-34.37492pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A\hookrightarrow A:\textsf{id}$}}}}}}$ Cast-arrow
$\displaystyle\displaystyle{\hbox{\hskip
80.95316pt\vbox{\hbox{\hskip-80.95316pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A_{{\mathrm{1}}}\hookrightarrow
A_{{\mathrm{2}}}:c_{{\mathrm{1}}}\qquad\Delta;\mathbb{E}\vdash
B_{{\mathrm{1}}}\hookrightarrow
B_{{\mathrm{2}}}:c_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
61.30035pt\vbox{\vbox{}\hbox{\hskip-61.30035pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A_{{\mathrm{1}}}\rightarrow B_{{\mathrm{1}}}\hookrightarrow
A_{{\mathrm{2}}}\rightarrow B_{{\mathrm{2}}}:c_{{\mathrm{1}}}\rightarrow
c_{{\mathrm{2}}}$}}}}}}$ Cast-unfold $\displaystyle\displaystyle{\hbox{\hskip
41.69559pt\vbox{\hbox{\hskip-41.69559pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mu\alpha.~{}A\qquad\vdash\mathbb{E}$}}}\vbox{}}}\over\hbox{\hskip
83.9476pt\vbox{\vbox{}\hbox{\hskip-83.9476pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash\mu\alpha.~{}A\hookrightarrow
A[\alpha\mapsto\mu\alpha.~{}A]:\textsf{unfold}_{\mu\alpha.~{}A}$}}}}}}$ Cast-
fold $\displaystyle\displaystyle{\hbox{\hskip
41.69559pt\vbox{\hbox{\hskip-41.69559pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash\mu\alpha.~{}A\qquad\vdash\mathbb{E}$}}}\vbox{}}}\over\hbox{\hskip
78.39203pt\vbox{\vbox{}\hbox{\hskip-78.39203pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A[\alpha\mapsto\mu\alpha.~{}A]\hookrightarrow\mu\alpha.~{}A:\textsf{fold}_{\mu\alpha.~{}A}$}}}}}}$
Cast-seq $\displaystyle\displaystyle{\hbox{\hskip
81.08981pt\vbox{\hbox{\hskip-81.0898pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A\hookrightarrow B:c_{{\mathrm{1}}}\qquad\Delta;\mathbb{E}\vdash
B\hookrightarrow C:c_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
41.12811pt\vbox{\vbox{}\hbox{\hskip-41.1281pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A\hookrightarrow C:c_{{\mathrm{1}}};c_{{\mathrm{2}}}$}}}}}}$ Cast-var
$\displaystyle\displaystyle{\hbox{\hskip
94.02295pt\vbox{\hbox{\hskip-94.02293pt\hbox{\hbox{$\displaystyle\displaystyle\Delta\vdash
A\qquad\Delta\vdash B\qquad\vdash\mathbb{E}\qquad\iota:A\hookrightarrow
B\in\mathbb{E}$}}}\vbox{}}}\over\hbox{\hskip
33.66019pt\vbox{\vbox{}\hbox{\hskip-33.66017pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A\hookrightarrow B:\iota$}}}}}}$ Cast-fix
$\displaystyle\displaystyle{\hbox{\hskip
165.47696pt\vbox{\hbox{\hskip-165.47696pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E},\iota:A_{{\mathrm{1}}}\rightarrow
B_{{\mathrm{1}}}\hookrightarrow A_{{\mathrm{2}}}\rightarrow
B_{{\mathrm{2}}}\vdash A_{{\mathrm{1}}}\hookrightarrow
A_{{\mathrm{2}}}:c_{{\mathrm{1}}}\qquad\Delta;\mathbb{E},\iota:A_{{\mathrm{1}}}\rightarrow
B_{{\mathrm{1}}}\hookrightarrow A_{{\mathrm{2}}}\rightarrow
B_{{\mathrm{2}}}\vdash B_{{\mathrm{1}}}\hookrightarrow
B_{{\mathrm{2}}}:c_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
75.84615pt\vbox{\vbox{}\hbox{\hskip-75.84615pt\hbox{\hbox{$\displaystyle\displaystyle\Delta;\mathbb{E}\vdash
A_{{\mathrm{1}}}\rightarrow B_{{\mathrm{1}}}\hookrightarrow
A_{{\mathrm{2}}}\rightarrow
B_{{\mathrm{2}}}:\textsf{fix}\,{\iota}.~{}(c_{{\mathrm{1}}}\rightarrow
c_{{\mathrm{2}}})$}}}}}}$

Figure 4. Typing and type cast rules for $\lambda^{\mu}_{Fi}$.

###  3.2. Typing

The top of Figure 4 shows the typing rules for $\lambda^{\mu}_{Fi}$. Most
rules are standard except for the typing rule for type casting (rule Typ-
cast). This rule replaces the standard folding and unfolding rules for iso-
recursive types, as we explained in §2.5. Rule Typ-cast relies on the type
casting rules shown at the bottom of Figure 4. In the type casting judgment
$\Delta;\mathbb{E}\vdash\textit{A}\hookrightarrow\textit{B}:c$, $\Delta$ is
the type context used to ensure that all the types in the cast derivation are
well-formed. $\mathbb{E}$ tracks of the cast variables $\iota$ that appear in
$c$ and the cast operator that they are associated with. New cast variables
are introduced when a fixpoint cast is encountered, as shown in rule Cast-fix,
which gives us the ability to encode the coinductive reasoning in equi-
recursive equalities. The cast operator $c$ in the type casting relation
essentially describes the derivation of a judgment. Our type casting rules,
ignoring the cast variables and operators, are very similar to the type
equality rules in Brandt and Henglein’s axiomatization of type equality.
Despite some subtle differences, which we will discuss in §4.2, our type
casting rules are sound and complete with respect to their type equality
rules.

###### Theorem 3.1 (Soundness and completeness of type casting).

For any types $A$ and $B$, $\cdot\vdash A\doteq B$ if and only if there exists
a cast operator $c$ such that $\cdot;\cdot\vdash A\hookrightarrow B:c$.

#### Equivalence to a calculus with equi-recursive typing.

The only difference between the equi-recursive typing rules and
$\lambda^{\mu}_{Fi}$’s typing rules is replacing type casting in rule Typ-cast
with a type equality relation. Therefore, we can give an alternative
definition of the equi-recursive typing rules in Figure 5. The gray parts are
used to generate a term in $\lambda^{\mu}_{Fi}$, and can be ignored for
understanding the equi-recursive typing rules. The standard equi-recursive
type equality relation in rule Typ-eq is replaced by the type casting relation
in rule ETyp-eq. Since the two relations are equivalent by Theorem 3.1, the
typing rules in Figure 5 are equivalent to the standard equi-recursive typing
rules.

  * $\Gamma\vdash_{e}e:A\text{ \hbox{\pagecolor{gray!20}$\rhd\,e^{\prime}$}}$ _(Equi-recursive typing and full iso-recursive elaboration)_

ETyp-int $\displaystyle\displaystyle{\hbox{\hskip
8.95828pt\vbox{\hbox{\hskip-8.95827pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
32.65323pt\vbox{\vbox{}\hbox{\hskip-32.65321pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}n:\mathsf{Int}\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,n$}}$}}}}}}$ ETyp-var
$\displaystyle\displaystyle{\hbox{\hskip
39.02763pt\vbox{\hbox{\hskip-39.02763pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma\qquad\mathit{x}:A\,\in\,\Gamma$}}}\vbox{}}}\over\hbox{\hskip
29.28978pt\vbox{\vbox{}\hbox{\hskip-29.28978pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}\mathit{x}:A\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,\mathit{x}$}}$}}}}}}$ ETyp-abs
$\displaystyle\displaystyle{\hbox{\hskip
42.23824pt\vbox{\hbox{\hskip-42.23824pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,\mathit{x}:A_{{\mathrm{1}}}\vdash_{e}e:A_{{\mathrm{2}}}\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}$}}$}}}\vbox{}}}\over\hbox{\hskip
74.34369pt\vbox{\vbox{}\hbox{\hskip-74.34367pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}\lambda\mathit{x}:A_{{\mathrm{1}}}.\,e:A_{{\mathrm{1}}}\rightarrow
A_{{\mathrm{2}}}\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,\lambda\mathit{x}:A_{{\mathrm{1}}}.\,e^{\prime}$}}$}}}}}}$
ETyp-app $\displaystyle\displaystyle{\hbox{\hskip
83.51538pt\vbox{\hbox{\hskip-83.51537pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e_{{\mathrm{1}}}:A_{{\mathrm{1}}}\rightarrow
A_{{\mathrm{2}}}\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}_{{\mathrm{1}}}$}}\qquad\Gamma\vdash_{e}e_{{\mathrm{2}}}:A_{{\mathrm{1}}}\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}_{{\mathrm{2}}}$}}$}}}\vbox{}}}\over\hbox{\hskip
40.73114pt\vbox{\vbox{}\hbox{\hskip-40.73112pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}:A_{{\mathrm{2}}}\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}_{{\mathrm{1}}}\,e^{\prime}_{{\mathrm{2}}}$}}$}}}}}}$
ETyp-eq $\displaystyle\displaystyle{\hbox{\hskip
71.20079pt\vbox{\hbox{\hskip-71.20079pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:A\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}$}}\qquad\cdot;\cdot\vdash
A\hookrightarrow B:c$}}}\vbox{}}}\over\hbox{\hskip
46.36758pt\vbox{\vbox{}\hbox{\hskip-46.36758pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:B\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,\textsf{cast}\,[c]\,e^{\prime}$}}$}}}}}}$

Figure 5. An equivalent equi-recursive typing system and elaboration rules to
$\lambda^{\mu}_{Fi}$.

###### Theorem 3.2 (Equivalence of alternative equi-recursive typing).

For any expression $e$ and type $A$, $\Gamma\vdash_{e}e:A$ in the standard
equi-recursive typing with rule Typ-eq if and only if there exists a full iso-
recursive term $e^{\prime}$ such that $\Gamma\vdash_{e}e:A\rhd e^{\prime}$
using the rules in Figure 5.

Our alternative formulation of equi-recursive typing also provides a way to
elaborate equi-recursive terms into full iso-recursive terms, as shown by the
gray colored parts in Figure 5. The elaboration is type-directed, by inserting
the appropriate casts where a type equality is needed following the typing
derivation of the equi-recursive terms. The interesting point here is that, by
replacing Brandt and Henglein’s type equality relation with our type casting
relation, we obtain a cast $c$, which can be viewed as evidence of the type
transformation from type $A$ into type $B$. Then, we use $c$ in an explicit
cast in the elaborated $\lambda^{\mu}_{Fi}$ term, which will trigger the type
transformation in $\lambda^{\mu}_{Fi}$. Every well-typed equi-recursive term
can be elaborated into a full iso-recursive term, and every full iso-recursive
term can be erased to an equi-recursive term that has the same type. It
follows that the full iso-recursive typing rules are sound and complete with
respect to equi-recursive types:

###### Theorem 3.3 (Equi-recursive to full iso-recursive typing).

For any expressions $e$, $e^{\prime}$ and type $A$, if
$\Gamma\vdash_{e}e:A\rhd e^{\prime}$ then $\Gamma\vdash e^{\prime}:A$.

###### Theorem 3.4 (Full iso-recursive to equi-recursive typing).

For any expressions $e$ and type $A$, if $\Gamma\vdash e:A$ then
$\Gamma\vdash_{e}|e|:A\rhd e$.

In the theorem above, the full iso-recursive expressions can be erased to the
equi-recursive expressions by removing the casts. The erasure operation $|e|$
is defined as follows:

$\begin{array}[]{llcll}|\textsf{n}|&=\textsf{n}&&|x|&=x\\\
|e_{1}~{}e_{2}|&=|e_{1}|~{}|e_{2}|&&|\lambda x:A.~{}e|&=\lambda x:A.~{}|e|\\\
|\textsf{cast}\,[c]\,e|&=|e|\end{array}$

Moreover, our elaboration achieves the round-tripping property – elaborating
an equi-recursive term into a full iso-recursive term and then erasing the
casts will get back the original equi-recursive term. This is not the case for
previous work in relating recursive types (Abadi and Fiore, 1996), in which
computationally relevant coercions are inserted as term-level functions and
erasing the unfold/fold annotations do not recover the original term. The
round-tripping property is crucial for a simple proof of the behavioral
equivalence between the two systems, which we discuss next.

###### Theorem 3.5 (Round-tripping of the encoding).

For any expression $e$, $e^{\prime}$ and type $A$, if $\Gamma\vdash_{e}e:A\rhd
e^{\prime}$, then $|e^{\prime}|=e$.

###  3.3. Semantics

Figure 6 shows the reduction rules for $\lambda^{\mu}_{Fi}$. In addition to
the standard reduction rules for the simply typed lambda calculus, we add the
reduction rules for the cast operators. Our reduction rules are call-by-value.
The inner expressions of the cast operators are reduced first (rule Red-cast).
Then, based on different cast operators, the cast operator is pushed into the
expression in various ways. For identity casts, the cast operator is simply
erased (rule Red-cast-id). Arrow casts are values, but when they are applied
to an argument, the cast operator is pushed into the argument (rule Red-cast-
arr). Note that the cast operator needs to be reversed when pushed into the
function argument in order to ensure type preservation after the reduction.
The reverse operation is defined by analyzing the structure of $c$ as follows:

$\begin{array}[]{llll}\neg\,\iota&=\iota&\neg\,\textsf{id}&=\textsf{id}\\\
\neg\,\textsf{fold}_{A}&=\textsf{unfold}_{A}&\neg\,\textsf{unfold}_{A}&=\textsf{fold}_{A}\\\
\neg\,(c_{1}\to
c_{2})&=(\neg\,c_{1})\to(\neg\,c_{2})&\neg\,(c_{1};c_{2})&=(\neg\,c_{2});(\neg\,c_{1})\\\
\neg\,(\textsf{fix}\,{\iota}.~{}c)&=\textsf{fix}\,{\iota}.~{}\neg\,c\end{array}$

A single sequential cast is split into two separate casts (rule Red-cast-seq),
so that the sub-components can be reduced independently. Fold casts are
values, but can be eliminated by an outer unfold cast (rule Red-cast-elim).
Thus, rule Red-cast-elim corresponds to the traditional fold/unfold
cancellation rule used in calculi with conventional iso-recursive types.
Finally, fixpoint casts are reduced by unrolling the fixpoint (rule Red-cast-
fix).

  * $e\hookrightarrow e^{\prime}$ _(Reduction)_

Red-beta $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
43.20775pt\vbox{\vbox{}\hbox{\hskip-43.20773pt\hbox{\hbox{$\displaystyle\displaystyle(\lambda\mathit{x}:A.\,e)\,v^{\prime}\hookrightarrow
e[\mathit{x}\mapsto v^{\prime}]$}}}}}}$ Red-appl
$\displaystyle\displaystyle{\hbox{\hskip
11.96512pt\vbox{\hbox{\hskip-11.96512pt\hbox{\hbox{$\displaystyle\displaystyle
e_{{\mathrm{1}}}\hookrightarrow
e^{\prime}_{{\mathrm{1}}}$}}}\vbox{}}}\over\hbox{\hskip
21.08801pt\vbox{\vbox{}\hbox{\hskip-21.08801pt\hbox{\hbox{$\displaystyle\displaystyle
e_{{\mathrm{1}}}\,e_{{\mathrm{2}}}\hookrightarrow
e^{\prime}_{{\mathrm{1}}}\,e_{{\mathrm{2}}}$}}}}}}$ Red-appr
$\displaystyle\displaystyle{\hbox{\hskip
11.96512pt\vbox{\hbox{\hskip-11.96512pt\hbox{\hbox{$\displaystyle\displaystyle
e_{{\mathrm{2}}}\hookrightarrow
e^{\prime}_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
21.63776pt\vbox{\vbox{}\hbox{\hskip-21.63776pt\hbox{\hbox{$\displaystyle\displaystyle
v_{{\mathrm{1}}}\,e_{{\mathrm{2}}}\hookrightarrow
v_{{\mathrm{1}}}\,e^{\prime}_{{\mathrm{2}}}$}}}}}}$ Red-cast
$\displaystyle\displaystyle{\hbox{\hskip
11.95398pt\vbox{\hbox{\hskip-11.95396pt\hbox{\hbox{$\displaystyle\displaystyle
e\hookrightarrow e^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
41.05931pt\vbox{\vbox{}\hbox{\hskip-41.0593pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[c]\,e\hookrightarrow\textsf{cast}\,[c]\,e^{\prime}$}}}}}}$
Red-cast-id $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
28.98372pt\vbox{\vbox{}\hbox{\hskip-28.9837pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[\textsf{id}]\,v\hookrightarrow
v$}}}}}}$ Red-cast-arr $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
94.65594pt\vbox{\vbox{}\hbox{\hskip-94.65593pt\hbox{\hbox{$\displaystyle\displaystyle(\textsf{cast}\,[c_{{\mathrm{1}}}\rightarrow
c_{{\mathrm{2}}}]\,v_{{\mathrm{1}}})\,v_{{\mathrm{2}}}\hookrightarrow\textsf{cast}\,[c_{{\mathrm{2}}}]\,(v_{{\mathrm{1}}}\,(\textsf{cast}\,[\neg
c_{{\mathrm{1}}}]\,v_{{\mathrm{2}}}))$}}}}}}$ Red-cast-seq
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
69.96104pt\vbox{\vbox{}\hbox{\hskip-69.96103pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[c_{{\mathrm{1}}};c_{{\mathrm{2}}}]\,v\hookrightarrow\textsf{cast}\,[c_{{\mathrm{2}}}]\,(\textsf{cast}\,[c_{{\mathrm{1}}}]\,v)$}}}}}}$
Red-castelim $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
68.09807pt\vbox{\vbox{}\hbox{\hskip-68.09805pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[\textsf{unfold}_{A}]\,(\textsf{cast}\,[\textsf{fold}_{B}]\,v)\hookrightarrow
v$}}}}}}$ Red-cast-fix $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
73.03065pt\vbox{\vbox{}\hbox{\hskip-73.03065pt\hbox{\hbox{$\displaystyle\displaystyle\textsf{cast}\,[\textsf{fix}\,{\iota}.~{}c]\,v\hookrightarrow\textsf{cast}\,[c[\iota\mapsto\textsf{fix}\,{\iota}.~{}c]]\,v$}}}}}}$

Figure 6. Reduction rules.

The addition of the push rules for the cast operators is necessary for the
type soundness of $\lambda^{\mu}_{Fi}$, since the cast rules are necessary to
preserve types. $\lambda^{\mu}_{Fi}$ is type sound, proved with the usual
preservation and progress theorems:

###### Theorem 3.6 (Progress).

For any expression $e$ and type $A$, if $\cdot\vdash e:A$ then either $e$ is a
value or there exists an expression $e^{\prime}$ such that $e\hookrightarrow
e^{\prime}$.

###### Theorem 3.7 (Preservation).

For any expression $e$ and type $A$, if $\cdot\vdash e:A$ and
$e\hookrightarrow e^{\prime}$ then $\cdot\vdash e^{\prime}:A$.

#### Equivalence to the equi-recursive dynamic semantics

As explained in §2.5, the reduction rules for the cast operators are
computationally irrelevant. Therefore, they can be erased from expressions
without affecting the behavior of the expressions. We can obtain the following
theorem easily:

###### Theorem 3.8 (Full iso-recursive to equi-recursive behavioral
preservation).

For any expression $e$, if $e\hookrightarrow^{*}v$ then
$|e|\hookrightarrow_{e}^{*}|v|$.

Here $\hookrightarrow_{e}$ is the reduction relation in the equi-recursive
setting, which is basically defined by a subset of the reduction rules in
Figure 6 (rules Red-beta, Red-appl, and Red-appr). We use
$\hookrightarrow^{*}$ to denote the reflexive, transitive closure of the
reduction relation. The other direction of the behavioral preservation also
holds, but only applies to well-typed expressions and relies on the
elaboration process defined in Figure 5. The proof of this direction is also
more involved, and we will detail it in §4.3. To summarize, the two systems
are behaviorally equivalent, in terms of both termination and divergence
behavior:

###### Theorem 3.9 (Behavioral equivalence).

For any expression $e$, $e^{\prime}$ and type $A$, if $\cdot\vdash_{e}e:A\rhd
e^{\prime}$, then

  1. (1)

$e\hookrightarrow^{*}_{e}v$ if and only if there exists $v^{\prime}$ such that
$e^{\prime}\hookrightarrow^{*}v^{\prime}$ and $|v^{\prime}|=v$.

  2. (2)

$e$ diverges if and only if $e^{\prime}$ diverges.

##  4\. Metatheory of full iso-recursive types

In this section we discuss the key proof techniques and results in the
metatheory of $\lambda^{\mu}_{Fi}$. The metatheory covers three components:
type soundness of $\lambda^{\mu}_{Fi}$ (Theorem 3.6 and 3.7), the typing
equivalence between $\lambda^{\mu}_{Fi}$ and equi-recursive types (Theorem
3.2, 3.3 and 3.4), and the behavioral equivalence between $\lambda^{\mu}_{Fi}$
and equi-recursive types (Theorem 3.9).

###  4.1. Type Soundness

#### Progress

For $\lambda^{\mu}_{Fi}$ we need to ensure that the definition of value and
the reduction rules, in particular the push rules for type casting, are
complementary to each other, i.e. a cast expression is either a value or can
be further reduced. The definition of value has been discussed in §3.1. In
$\lambda^{\mu}_{Fi}$ now there are two canonical forms for a value with
function types ($A_{1}\to A_{2}$): lambda abstractions $(\lambda x:A.~{}e)$
and arrow casts $(\textsf{cast}\,[c_{1}\to c_{2}]\,v)$. Therefore in the
progress proof for function applications ($e_{1}~{}e_{2}$), we need to
consider one extra case when $e_{1}$ is an arrow cast. We push the cast
operator further by rule Red-cast-arr as a reduction step in this case to
complete the proof.

#### Preservation

The preservation proof is standard by first doing induction on the typing
derivation $\cdot\vdash e:A$ and then induction on the reduction relation
$e\hookrightarrow e^{\prime}$. The interesting cases are when the reduction
rule is a push rule. Most cases of the push rules are straightforward, by
inversion on the type casting relation and then reconstructing the casting
derivation for the reduced expression. Two tricky cases require extra care:
the push rules for arrow cast (rule Red-cast-arr) and the fixpoint cast (rule
Red-cast-fix).

In the Red-cast-arr case, by inversion on the typing derivation of
$\cdot\vdash(\textsf{cast}\,[c_{1}\to c_{2}]\,v_{1})~{}v_{2}:A_{2}$ we know
that $v_{1}$ has a function type $B_{1}\to B_{2}$, $v_{2}$ has type $A_{1}$,
and $B_{1}\to B_{2}$ can be cast to $A_{1}\to A_{2}$ by $c_{1}\to c_{2}$,
which in turn implies that $B_{1}\hookrightarrow A_{1}:c_{1}$ and
$B_{2}\hookrightarrow A_{2}:c_{2}$. In order to show that the type of the
reduced expression $(\textsf{cast}\,[c_{2}]\,(v_{1}~{}(\textsf{cast}\,[\neg
c_{1}]\,v_{2})))$ is still $A_{2}$, we need to prove $A_{1}\hookrightarrow
B_{1}:\neg c_{1}$. This goal can be achieved by Lemma 4.1 below, which is
proved by induction on the type casting relation. The analysis of rule Red-
cast-arr also shows that it is necessary to insert the reverse operation on
the cast operator $c_{1}$ to ensure the preservation of $\lambda^{\mu}_{Fi}$.

###### Lemma 4.1 (Reverse of casting).

For any types $A$ and $B$, and casting operators $c$, if $\cdot;\cdot\vdash
A\hookrightarrow B:c$ then $\cdot;\cdot\vdash B\hookrightarrow A:\neg\,c$.

As for the Red-cast-fix case, the reduction rule unfolds the fixpoint cast
$(\textsf{fix}\,{\iota}.~{}c)$ to
$(c[\iota\mapsto(\textsf{fix}\,{\iota}.~{}c)])$. By inversion on the type
casting relation $\cdot;\cdot\vdash A\hookrightarrow
B:\textsf{fix}\,{\iota}.~{}c$, we know that

(2) $\cdot;\iota:A\hookrightarrow B\vdash A\hookrightarrow B:c$

Essentially the cast operator $(\textsf{fix}\,{\iota}.~{}c)$ and its unrolling
$(c[\iota\mapsto(\textsf{fix}\,{\iota}.~{}c)])$ should represent the same
proof. The type casting judgement (2) can be interpreted as: if we know that
there is a cast variable $\iota$ that can cast $A$ to $B$, then we can cast
$A$ to $B$ by $c$, using the cast variable $\iota$. Since we already know that
$\textsf{fix}\,{\iota}.~{}c$ can do the same job as $\iota$ in casting $A$ to
$B$, it should be safe to replace $\iota$ with $\textsf{fix}\,{\iota}.~{}c$ in
the cast operator $c$, and show that $\cdot;\cdot\vdash A\hookrightarrow
B:c[\iota\mapsto(\textsf{fix}\,{\iota}.~{}c)]$. This idea can be formalized by
the following cast substitution lemma, which is proved by induction on the
type casting relation of $c_{1}$.

###### Lemma 4.2 (Cast substitution).

For any contexts $\Gamma$, $\mathbb{E}$, types $A$, $B$, $C$, $D$, cast
operators $c_{1}$, $c_{2}$ and cast variable $\iota$, if
$\Gamma;\mathbb{E}\vdash A\hookrightarrow B:c_{1}$, and
$\Gamma;\mathbb{E},\iota:A\hookrightarrow B\vdash C\hookrightarrow D:c_{2}$
then $\Gamma;\mathbb{E}\vdash C\hookrightarrow D:c_{2}[\iota\mapsto c_{1}]$.

###  4.2. Typing Equivalence

As discussed in Section 3.2, the key to the typing equivalence between full
iso-recursive types and equi-recursive types is to show our type casting rules
are equivalent to Brandt and Henglein’s type equality rules (Theorem 3.1).
This section focuses on the proof of this theorem.

Most of our type casting rules, ignoring the cast variables and operators, are
very similar to their type equality rules, so the proof for these cases is
straightforward. For instance, the treatment of coinductive reasoning by
introducing new premises for function types in our rule Cast-fix is exactly
the same treatment as their rule Tye-arrfix. We discuss the only two
differences below.

#### Arrow cast for type soundness

In addition to transforming function types with a fixpoint cast using rule
Cast-fix as Brandt and Henglein did in rule Tye-arrfix, we also allow function
types to be cast without a fixpoint cast as well, as shown in rule Cast-arr.
This is a harmless extension, since one can always wrap an arrow cast with a
dummy fixpoint, which does not use the fixpoint variable in the body. However,
having this rule is essential to the type soundness of $\lambda^{\mu}_{Fi}$.
By rule Cast-fix, all the fixpoint casts in well-typed expressions are in the
form of $\textsf{fix}\,{\iota}.~{}c_{1}\to c_{2}$. During the reduction, we
need to unroll those fixpoint casts using rule Red-cast-fix to a bare arrow
cast in the form of $c^{\prime}_{1}\to c^{\prime}_{2}$, which cannot be typed
without the rule Cast-arr. In other words, while casts of arrows are values,
casts of fixpoints are not values. Due to this difference we separate the two
rules and prove that the extension does not affect the soundness and
completeness of our type casting rules.

#### Removing the symmetry rule from equality

The other difference is that our rules do not include a symmetry rule for type
casting, since it is hard to interpret symmetry in the operational semantics.
As a result, changing the type cast context from $\cdot$ to a universally
quantified $\mathbb{E}$ in Lemma 4.1 will not work, i.e. rule Tye-symm in its
general form, with the same list of assumptions $H$ in both the premise and
conclusion, is not admissible in our type casting relation. The reason is that
invalid assumptions may exist in the list $H$, which are not derivable by the
type casting rules. For example,
$\texttt{Int}\doteq\texttt{Int}\to\texttt{Int}\vdash\texttt{Int}\to\texttt{Int}\doteq\texttt{Int}$
is a valid judgement using rules Tye-symm and Tye-assump, but cannot be
derived from our type casting rules.

Nevertheless we can still prove that our system is complete to Brandt and
Henglein’s equality, when the initial environment is empty. The idea is that
starting from an empty assumption list, one can always replace the use of rule
Tye-symm in the derivation with a complete derivation that redoes the proof
goal in the symmetry way to obtain a derivation without using rule Tye-symm.
The replacement is feasible since when the initial environment is empty, all
the type equalities introduced to the environment are guaranteed to be
derivable from an empty assumption list by the type casting rules. Interested
readers can refer to our Coq formalization for the details of the proof.

###  4.3. Behavioral Equivalence

To prove Theorem 3.9 it suffices to show one of the two propositions in the
theorem. Since the type soundness of $\lambda^{\mu}_{Fi}$ ensures that a well-
typed term does not get stuck – it can either diverge or reduce to a value, we
only need to show the preservation of termination behavior and the
preservation of divergence behavior can then be proved by contradiction. The
“if” direction of the theorem (from full-iso recursive reduction to equi-
recursive reduction) is easy, directly from the behavioral preservation
property of the erasure function (Theorem 3.8). The “only if” direction (from
equi-recursive reduction to full-iso recursive reduction) is more involved,
and we prove it by induction on the length of reduction steps. It suffices to
show the following lemma, which states that one step of equi-recursive
reduction can be simulated by several steps of full iso-recursive reduction.

###### Lemma 4.3 (Simulation of equi-recursive reduction).

For any expressions $e_{1}$, $e^{\prime}_{1}$, $e_{2}$ and type $A$, if
$\cdot\vdash_{e}e_{1}:A\rhd e_{1}^{\prime}$ and
$e_{1}\hookrightarrow_{e}e_{2}$, then there exists $e_{2}^{\prime}$ such that
$e_{1}^{\prime}\hookrightarrow^{*}e_{2}^{\prime}$ and
$\cdot\vdash_{e}e_{2}:A\rhd e_{2}^{\prime}$.

The proof of Lemma 4.3 is done by first induction on the equi-recursive
reduction relation $e_{1}\hookrightarrow_{e}e_{2}$, and then induction on the
elaboration relation $\cdot\vdash_{e}e_{1}:A\rhd e_{1}^{\prime}$. Most of the
cases are straightforward, by applying the induction hypothesis and using the
congruence lemmas below to construct the reduction steps.

###### Lemma 4.4 (Congruence lemma of full iso-recursive reduction).

  1. (1)

If $e_{1}\hookrightarrow^{*}e_{1}^{\prime}$, then
$e_{1}~{}e_{2}\hookrightarrow^{*}e_{1}^{\prime}~{}e_{2}$.

  2. (2)

If $e_{2}\hookrightarrow^{*}e_{2}^{\prime}$, then
$v_{1}~{}e_{2}\hookrightarrow^{*}v_{1}~{}e_{2}^{\prime}$.

  3. (3)

If $e\hookrightarrow^{*}e^{\prime}$, then
$\textsf{cast}\,[c]\,e\hookrightarrow^{*}\textsf{cast}\,[c]\,e^{\prime}$.

The tricky case is when $e_{1}\hookrightarrow_{e}e_{2}$ is a beta reduction
(case Red-beta). By inversion on the reduction relation, we know that $e_{1}$
is a function application ($e_{1}=(\lambda x:A_{1}.e_{0})~{}v_{1}$) and
$e_{2}$ is ($e_{0}[x\mapsto v_{1}]$). By induction on the elaboration relation
$\cdot\vdash_{e}e_{1}:A\rhd e_{1}^{\prime}$, case ETyp-eq can be proved using
the induction hypothesis. We consider case ETyp-app, where

(3) $\cdot\vdash\lambda x:A_{1}.e_{0}:A_{1}\to A\rhd e_{3}^{\prime}\quad\text{
and }\quad\cdot\vdash v_{1}:A_{1}\rhd e_{4}^{\prime}$

However, we do not know the exact form of $e_{3}^{\prime}$ and
$e_{4}^{\prime}$, since many different casts can be inserted in the
elaboration derivation using rule ETyp-eq, and the current induction
hypothesis cannot deal with this. To address this issue, we first prove a
lemma showing that any full iso-recursive terms elaborated from an equi-
recursive _value_ can always be further reduced to a value in the full iso-
recursive setting.

###### Lemma 4.5 (Reductions of full iso-recursive terms from equi-recursive
values).

For any expression $e$ and type $A$, if $\cdot\vdash_{e}v:A\rhd e^{\prime}$,
then there exists $v^{\prime}$ such that
$e^{\prime}\hookrightarrow^{*}v^{\prime}$ and $\cdot\vdash_{e}v:A\rhd
v^{\prime}$.

Lemma 4.5 can be proved by induction on the typing derivation
$\cdot\vdash_{e}v:A\rhd e^{\prime}$ and using the congruence lemma (Lemma
4.4). By applying Lemma 4.5 to (3) in the tricky case of Lemma 4.3, we can
first show that both $e_{3}^{\prime}$ and $e_{4}^{\prime}$ can be further
reduced to a value. Moreover, the value of evaluating $e_{3}^{\prime}$
preserves the function type, so it must be one of the two canonical forms: a
lambda abstraction $(\lambda x:A_{1}.e^{\prime}_{0})$ or an arrow cast
$(\textsf{cast}\,[c_{1}\to c_{2}]\,v^{\prime}_{1})$, and then we can construct
the reduction steps for $(e^{\prime}_{3}~{}e^{\prime}_{4})$ as shown below:

$\begin{array}[]{ll@{}l@{}ll}&e^{\prime}_{3}~{}e^{\prime}_{4}\\\
\hookrightarrow^{*}&(\lambda
x:A_{1}.e^{\prime}_{0})~{}e^{\prime}_{4}&\text{\quad
or\quad}&(\textsf{cast}\,[c_{1}\to
c_{2}]\,v^{\prime}_{1})~{}e^{\prime}_{4}&\text{(Lemma~{}\ref{lem:equi-to-full-
iso-value} and \ref{lem:cong-red}(\ref{lem:cong-red1}))}\\\
\hookrightarrow^{*}&(\lambda
x:A_{1}.e^{\prime}_{0})~{}v^{\prime}_{2}&\text{\quad
or\quad}&(\textsf{cast}\,[c_{1}\to
c_{2}]\,v^{\prime}_{1})~{}v^{\prime}_{2}&\text{(Lemma~{}\ref{lem:equi-to-full-
iso-value} and \ref{lem:cong-red}(\ref{lem:cong-red2}))}\\\
\hookrightarrow&e^{\prime}_{0}[x\mapsto v^{\prime}_{2}]&\text{\quad
or\quad}&(\textsf{cast}\,[c_{2}]\,(v^{\prime}_{1}~{}(\textsf{cast}\,[\neg
c_{1}]\,v^{\prime}_{2})))&\text{({{R}ule~{}\hyperlink{ottalt:rule:ott:Red-
beta}{{{{Red-beta}}}}} or {\hyperlink{ottalt:rule:ott:Red-cast-arr}{{{{Red-
cast-arr}}}}}) }\\\ \end{array}$

Now we are left to prove the second goal of Lemma 4.3, that is, the result of
the reduction constructed above can be derived from the elaboration relation,
i.e.

$\cdot\vdash_{e}e_{0}[x\mapsto v_{1}]:A\rhd e^{\prime}_{0}[x\mapsto
v^{\prime}_{2}]\quad\text{or}\quad\cdot\vdash_{e}e_{0}[x\mapsto
v_{1}]:A\rhd(\textsf{cast}\,[c_{2}]\,(v^{\prime}_{1}~{}(\textsf{cast}\,[\neg
c_{1}]\,v^{\prime}_{2})))$

The latter case for rule Red-cast-arr follows from the induction hypothesis.
The first case for rule Red-beta can be proved by the following substitution
lemma for the elaboration relation.

###### Lemma 4.6 (Substitution lemma for elaboration).

For any typing context $\Gamma$, expressions $e_{1}$, $e_{1}^{\prime}$,
$e_{2}$, $e_{2}^{\prime}$ and types $A$, $B$, if
$\Gamma,x:A\vdash_{e}e_{1}:B\rhd e_{1}^{\prime}$ and
$\Gamma\vdash_{e}e_{2}:A\rhd e_{2}^{\prime}$, then
$\Gamma\vdash_{e}e_{1}[x\mapsto e_{2}]:B\rhd e_{1}^{\prime}[x\mapsto
e_{2}^{\prime}]$.

With Lemma 4.4, 4.5 and 4.6, we complete the proof of Lemma 4.3, and the
behavioral preservation theorem (Theorem 3.9) follows. Compared to the
behavioral equivalence proof in Abadi and Fiore’s work, we show that it is
much more straightforward to prove the behavioral equivalence between full
iso-recursive types and equi-recursive types, and our proof for
$\lambda^{\mu}_{Fi}$ is completely mechanized in Coq, without relying on any
conjectures or axioms.

##  5\. Recursive Subtyping

In this section we show that our results in the previous sections can be
extended to a calculus with subtyping called $\lambda^{\mu<:}_{Fi}$.

###  5.1. A Calculus with Subtyping

Adapting the results in Section 3 to a calculus with subtyping requires only a
few changes. In terms of types, we add a top type ($\top$). Expressions and
values remain the same.

  * $\Sigma\vdash A\leq_{\oplus}B$ _(Equi-recursive/Iso-recursive Subtyping)_

Sub-top $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
24.53883pt\vbox{\vbox{}\hbox{\hskip-24.53882pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A\leq_{\oplus}\top$}}}}}}$ Sub-int
$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
25.68687pt\vbox{\vbox{}\hbox{\hskip-25.68686pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\mathsf{Int}\leq_{i}\mathsf{Int}$}}}}}}$
Sub-eq $\displaystyle\displaystyle{\hbox{\hskip
14.32112pt\vbox{\hbox{\hskip-14.32112pt\hbox{\hbox{$\displaystyle\displaystyle
A\doteq B$}}}\vbox{}}}\over\hbox{\hskip
23.8193pt\vbox{\vbox{}\hbox{\hskip-23.8193pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A\leq_{e}B$}}}}}}$ Sub-var $\displaystyle\displaystyle{\hbox{\hskip
22.41542pt\vbox{\hbox{\hskip-22.4154pt\hbox{\hbox{$\displaystyle\displaystyle\alpha\leq\beta\in\Sigma$}}}\vbox{}}}\over\hbox{\hskip
22.92656pt\vbox{\vbox{}\hbox{\hskip-22.92654pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\alpha\leq_{\oplus}\beta$}}}}}}$
Sub-self $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
43.38364pt\vbox{\vbox{}\hbox{\hskip-43.38362pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\mu\alpha.~{}A\leq_{i}\mu\alpha.~{}A$}}}}}}$
Sub-trans $\displaystyle\displaystyle{\hbox{\hskip
57.81987pt\vbox{\hbox{\hskip-57.81985pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A\leq_{e}B\qquad\Sigma\vdash B\leq_{e}C$}}}\vbox{}}}\over\hbox{\hskip
23.70715pt\vbox{\vbox{}\hbox{\hskip-23.70714pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A\leq_{e}C$}}}}}}$ Sub-arrow $\displaystyle\displaystyle{\hbox{\hskip
62.20897pt\vbox{\hbox{\hskip-62.20897pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
B_{{\mathrm{1}}}\leq_{\oplus}A_{{\mathrm{1}}}\qquad\Sigma\vdash
A_{{\mathrm{2}}}\leq_{\oplus}B_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
44.47562pt\vbox{\vbox{}\hbox{\hskip-44.47562pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash
A_{{\mathrm{1}}}\rightarrow
A_{{\mathrm{2}}}\leq_{\oplus}B_{{\mathrm{1}}}\rightarrow
B_{{\mathrm{2}}}$}}}}}}$ Sub-rec $\displaystyle\displaystyle{\hbox{\hskip
39.60878pt\vbox{\hbox{\hskip-39.60878pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma,\alpha\leq\beta\vdash
A\leq_{\oplus}B$}}}\vbox{}}}\over\hbox{\hskip
44.51979pt\vbox{\vbox{}\hbox{\hskip-44.51978pt\hbox{\hbox{$\displaystyle\displaystyle\Sigma\vdash\mu\alpha.~{}A\leq_{\oplus}\mu\beta.~{}B$}}}}}}$

Figure 7. Amadio and Cardelli’s equi-recursive and iso-recursive subtyping
rules.

#### Subtyping

The equi-recursive and iso-recursive subtyping rules that we use in this
section are based on the Amber rules (Amadio and Cardelli, 1993), as shown in
Figure 7. The subtyping rules use a special environment $\Sigma$, which tracks
a set of pairs of type variables that are assumed in the subtyping relation,
as explained in §2.4. We use $\leq_{\oplus}$ parameterized by a metavariable
$\oplus\in\\{i,e\\}$ to denote the subtyping rules for both relations: $i$
denotes iso-recursive subtyping, and $e$ denotes equi-recursive subtyping. We
use $\leq_{e}$ to denote the subtyping rules (rules Sub-eq and Sub-trans) that
only apply to equi-recursive types, and $\leq_{i}$ to denote the subtyping
rules (rules Sub-int and Sub-self) that only apply to iso-recursive types.
Rule Sub-eq embeds the equi-recursive equality relation in Figure 1 into the
subtyping relation, so is only present in equi-recursive subtyping. For the
iso-recursive subtyping relation, we choose the variant of the Amber rules
presented by Zhou et al. (2022), which replaces the built-in reflexivity with
the more primitive rules Sub-int and Sub-self and removes transitivity rule
Sub-trans from the original Amber rules. Zhou et al. discussed the technical
challenges of having reflexivity and transitivity built-in in the iso-
recursive subtyping relation, and showed that they are admissible from the
other rules.

###### Lemma 5.1 (Reflexivity of iso-recursive subtyping).

If $A$ is a closed type, then $\Sigma\vdash A\leq_{i}A$.

###### Lemma 5.2 (Transitivity of iso-recursive subtyping).

If $\cdot\vdash A\leq_{i}B$ and $\cdot\vdash B\leq_{i}C$, then $\cdot\vdash
A\leq_{i}C$.

In Lemma 5.1, the assumption that $A$ is a closed type can be implied by the
fact that the free variable sets of $A$ and $B$ in the subtyping relation
$\Sigma\vdash A\leq_{i}B$ are disjoint, which is also a side condition in
Amadio and Cardelli’s equi-recursive Amber rules. As for the transitivity,
Lemma 5.2 only holds when the environment is empty. Otherwise, one may also
get into problematic subtyping relations, as discussed by Zhou et al.. For the
reasons above, we choose to use the variant of iso-recursive Amber rules
without built-in reflexivity and transitivity in this section.

#### Typing and Reduction

As for the typing rules, we extend the full iso-recursive type system in
Figure 4 with rule Typ-sub, and the equi-recursive type system in Figure 5
with rules ETyp-isub and ETyp-bare-sub, respectively. Rule ETyp-isub allows
the elaboration rule to consider iso-recursive subtyping subsumptions, as rule
Typ-sub does in the typing rules for $\lambda^{\mu<:}_{Fi}$. Rule ETyp-bare-
sub is required for the calculus with equi-recursive subtyping. Note that rule
ETyp-bare-sub only exists in the equi-recursive type system. The elaboration
rule for this case will be discussed later in this section. There are no
changes to the reduction rules.

Typ-sub $\displaystyle\displaystyle{\hbox{\hskip
50.18323pt\vbox{\hbox{\hskip-50.18323pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:A\qquad\cdot\vdash A\leq_{i}B$}}}\vbox{}}}\over\hbox{\hskip
19.49641pt\vbox{\vbox{}\hbox{\hskip-19.49641pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
e:B$}}}}}}$ ETyp-isub $\displaystyle\displaystyle{\hbox{\hskip
61.80731pt\vbox{\hbox{\hskip-61.8073pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:A\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}$}}\qquad\cdot\vdash
A\leq_{i}B$}}}\vbox{}}}\over\hbox{\hskip
31.1205pt\vbox{\vbox{}\hbox{\hskip-31.12048pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:B\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}$}}$}}}}}}$ ETyp-bare-
sub $\displaystyle\displaystyle{\hbox{\hskip
50.43726pt\vbox{\hbox{\hskip-50.43724pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:A\qquad\cdot\vdash
A\leq_{e}B$}}}\vbox{}}}\over\hbox{\hskip
19.41132pt\vbox{\vbox{}\hbox{\hskip-19.41132pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:B$}}}}}}$

###  5.2. Type Soundness

There are no significant technical challenges in extending the type soundness
proof to $\lambda^{\mu<:}_{Fi}$. The only part that requires extra care is the
preservation lemma, in which we need to show that rule Red-castelim preserves
the typing in the presence of subtyping. Let us consider an expression
$\textsf{cast}\,[\textsf{unfold}_{\mu\alpha.~{}A}]\,(\textsf{cast}\,[\textsf{fold}_{\mu\alpha.~{}B}]\,v)$.
The derivation below shows the typing of this expression.

$\cdot\vdash v:B[\alpha\mapsto\mu\alpha.~{}B]$ $\ldots$ Typ-cast
$\cdot\vdash\textsf{cast}\,[\textsf{fold}_{\mu\alpha.~{}B}]\,v:\mu\alpha.~{}B$
$\cdot\vdash\mu\alpha.~{}B\leq_{i}\mu\alpha.~{}A$ Typ-sub
$\cdot\vdash\textsf{cast}\,[\textsf{fold}_{\mu\alpha.~{}B}]\,v:\mu\alpha.~{}A$
$\ldots$ Typ-cast
$\cdot\vdash\textsf{cast}\,[\textsf{unfold}_{\mu\alpha.~{}A}]\,(\textsf{cast}\,[\textsf{fold}_{\mu\alpha.~{}B}]\,v):A[\alpha\mapsto\mu\alpha.~{}A]$

By inversion we know that after reduction using rule Red-castelim, the result
$v$ has the type $B[\alpha\mapsto\mu\alpha.~{}B]$, and that
$\mu\alpha.~{}B\leq_{i}\mu\alpha.~{}A$. The preservation proof goal for this
case can be expressed as the following lemma:

###### Lemma 5.3 (Unfolding lemma).

If $\cdot\vdash\mu\alpha.~{}B\leq_{i}\mu\alpha.~{}A$, then $\cdot\vdash
B[\alpha\mapsto\mu\alpha.~{}B]\leq_{i}A[\alpha\mapsto\mu\alpha.~{}A]$.

The proof of this lemma has been shown by Zhou et al. (2022, Corollary 59).
They proposed an alternative formulation of the iso-recursive subtyping rules,
which is equivalent to the iso-recursive Amber rules. Therefore, by adopting
their results, we complete the type soundness proof for
$\lambda^{\mu<:}_{Fi}$.

###### Theorem 5.4 (Type soundness of $\lambda^{\mu<:}_{Fi}$).

For any term $e$ and type $A$ in $\lambda^{\mu<:}_{Fi}$,

  1. (1)

(Progress) if $\cdot\vdash e:A$ then either $e$ is a value or there exists a
term $e^{\prime}$ such that $e\hookrightarrow e^{\prime}$.

  2. (2)

(Preservation) if $\cdot\vdash e:A$ and $e\hookrightarrow e^{\prime}$ then
$\cdot\vdash e^{\prime}:A$.

###  5.3. Typing equivalence

Similarly to $\lambda^{\mu}_{Fi}$ with equality, we can prove that
$\lambda^{\mu<:}_{Fi}$ with iso-recursive subtyping is sound and complete with
respect to a calculus with equi-recursive subtyping. The key idea is to encode
the equi-recursive subtyping relation using a combination of equi-recursive
equality and the iso-recursive subtyping relation, as explained in §2.5. The
encoding can be justified by the following theorem:

###### Theorem 5.5 (Equi-recursive subtyping decomposition).

$\cdot\vdash A\leq_{e}B$ if and only if there exist types $C_{1}$ and $C_{2}$
such that $A\doteq C_{1}$, $\cdot\vdash C_{1}\leq_{i}C_{2}$, and $C_{2}\doteq
B$.

The soundness direction (i.e. the “if” direction) of this lemma is
straightforward by rules Sub-eq and Sub-trans and the fact that $\leq_{i}$ is
a sub-relation of $\leq_{e}$. The completeness direction can be derived from
Amadio and Cardelli’s proof of completeness with respect to the tree model for
the equi-recursive Amber rules. They proved that for any types $A$, $B$ that
are in the tree model interpretation of the equi-recursive subtyping relation,
one can find types $C_{1}$ and $C_{2}$ such that $A\doteq C_{1}$,
$C_{1}\leq_{e}C_{2}$, and $C_{2}\doteq B$ hold (Amadio and Cardelli, 1993,
Lemma 5.4.1, Lemma 5.4.3). Moreover, the derivation of $C_{1}\leq_{e}C_{2}$
satisfies the _one-expansion property_ , which means that in the derivation
each recursive type is unfolded at most once, informally speaking. Although
this result is expressed as an equi-recursive subtyping relation in their
conclusion, we can rewrite all the occurrences of $C_{1}\leq_{e}C_{2}$ with
one-expansion property in their proof to an iso-recursive subtyping relation
$C_{1}\leq_{i}C_{2}$. Every application of rules Sub-eq and Sub-trans in their
proofs can either be replaced by rule Sub-rec, in which the recursive type
body does not involve the type variable and unfolds to itself, or by rule Sub-
self for two recursive types that are syntactically equal up to
$\alpha$-renaming. In other words, Amadio and Cardelli’s proof of their Lemma
5.4.3 can be seen as a proof that the iso-recursive subtyping relation is
complete with respect to the equi-recursive subtyping relation with the one-
expansion property, because they never use the power of the rules Sub-eq and
Sub-trans.

$\vdash\texttt{Int}\leq_{e}\texttt{Int}$ Tyeq-unfold Tyeq-contract
$A_{1}\doteq\top\to A_{2}$ $\vdash\top\leq_{e}\top$ $\mathcal{P}_{1}$ Sub-rec
$\vdash A_{2}\leq_{e}B$ Sub-arrow $\vdash\top\to A_{2}\leq_{e}\top\to B$ Sub-
eq and Sub-trans $\vdash A_{1}\leq_{e}\top\to B$ Sub-arrow $\vdash
A\leq_{e}\texttt{Int}\to\top\to B$ Tyeq-unfold $\vdash\texttt{Int}\to\top\to
B\doteq B$ $\begin{array}[]{@{}l@{}}\text{{\hyperlink{ottalt:rule:ott:Sub-
trans}{{{{Sub-trans}}}}}}\\\\[-2.0pt] \text{and
{\hyperlink{ottalt:rule:ott:Sub-eq}{{{{Sub-eq}}}}}}\end{array}$ $\vdash
A\leq_{e}B$

$\vdash\texttt{Int}\leq_{i}\texttt{Int}$ Lemma 5.1 $\vdash\top\to
A_{2}\leq_{i}\top\to A_{2}$ $\vdash\top\leq_{i}\top$ $\mathcal{P}_{2}$ Sub-rec
$\vdash A_{2}\leq_{i}B$ Sub-arrow $\vdash\top\to A_{2}\leq_{i}\top\to B$ Lemma
5.2 $\vdash\top\to A_{2}\leq_{i}\top\to B$ Sub-arrow $\vdash C\leq_{i}D$ Lemma
5.1 $\vdash D\leq_{i}D$ Lemma 5.2 $\vdash C\leq_{i}D$

$\begin{array}[]{l}\begin{array}[]{ll}A=\texttt{Int}\to(\mu\alpha.~{}\top\to\alpha)&B=\mu\alpha.~{}\texttt{Int}\to\top\to\alpha\\\
C=\texttt{Int}\to\top\to(\mu\alpha.~{}\top\to\top\to\alpha)&D=\texttt{Int}\to\top\to(\mu\alpha.~{}\texttt{Int}\to\top\to\alpha)\\\
A_{1}=\mu\alpha.~{}\top\to\alpha&A_{2}=\mu\alpha.~{}\top\to\top\to\alpha\end{array}\\\
\,\,\,\mathcal{P}_{1}\text{ is the judgement
}\alpha\leq\beta\vdash\top\to\top\to\alpha\leq_{e}\texttt{Int}\to\top\to\beta\\\
\,\,\,\mathcal{P}_{2}\text{ is the judgement
}\alpha\leq\beta\vdash\top\to\top\to\alpha\leq_{i}\texttt{Int}\to\top\to\beta\end{array}$

Figure 8. Illustration of decomposing an equi-recursive subtyping derivation.

The idea of this decomposition can be illustrated by an example in Figure 8.
The upper part of the figure shows a derivation by following Amadio and
Cardelli’s subtyping algorithm for equi-recursive subtyping. Note that there
are two applications of rule Sub-eq in the derivation, one for expanding the
type $\mu\alpha.~{}\top\to\alpha$ to
$\top\to\mu\alpha.~{}\top\to\top\to\alpha$ and the other for expanding the
type $B$ to its unfolding $\texttt{Int}\to\top\to B$. Although rule Sub-eq is
applied in the middle of the derivation, we can always lift these uses of rule
Sub-eq to the top of the derivation, by replacing two types in the conclusion
with their more expanded forms. The lower part of the figure shows such a
derivation, in which we use $C$ and $D$ to denote (a simplified form of) the
expanded types obtained from Amadio and Cardelli’s proof. A key observation
here is that the original structure of the derivation is preserved in the new
derivation. To highlight this, we use a dummy application of the reflexivity
and transitivity lemma to show the correspondence between the two derivations.

With the decomposition theorem, we can use the following rule to encode the
equi-recursive subtyping relation:

ETyp-sub $\displaystyle\displaystyle{\hbox{\hskip
146.9263pt\vbox{\hbox{\hskip-146.92628pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:A\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,e^{\prime}$}}\qquad\cdot;\cdot\vdash
A\hookrightarrow C_{{\mathrm{1}}}:c_{{\mathrm{1}}}\qquad\cdot\vdash
C_{{\mathrm{1}}}\leq_{i}C_{{\mathrm{2}}}\qquad\cdot;\cdot\vdash
C_{{\mathrm{2}}}\hookrightarrow
B:c_{{\mathrm{2}}}$}}}\vbox{}}}\over\hbox{\hskip
68.30359pt\vbox{\vbox{}\hbox{\hskip-68.30357pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash_{e}e:B\text{
\hbox{\pagecolor{gray!20}$\displaystyle\rhd\,\textsf{cast}\,[c_{{\mathrm{2}}}]\,(\textsf{cast}\,[c_{{\mathrm{1}}}]\,e^{\prime})$}}$}}}}}}$

If one ignores the gray parts in the rule, rule ETyp-sub is equivalent to rule
ETyp-bare-sub. We can first apply Theorem 3.1 to rewrite our type casting
rules to equi-recursive equalities and then use Theorem 5.5 to show the
equivalence to the equi-recursive subtyping relation. On the other hand, rule
ETyp-sub can be derived from the primitive rules ETyp-eq and ETyp-isub in
$\lambda^{\mu<:}_{Fi}$. Therefore, we can conclude that $\lambda^{\mu<:}_{Fi}$
with iso-recursive subtyping is sound and complete with respect to a calculus
with equi-recursive subtyping in terms of typing.

###### Theorem 5.6 (Typing equivalence for $\lambda^{\mu<:}_{Fi}$).

For any expressions $e$, $e^{\prime}$ and type $A$,

  1. (1)

(Soundness) if $\Gamma\vdash e:A$ then $\Gamma\vdash_{e}|e|:A\rhd e$.

  2. (2)

(Completeness) if $\Gamma\vdash_{e}e:A\rhd e^{\prime}$ then $\Gamma\vdash
e^{\prime}:A$.

  3. (3)

(Round-tripping) if $\Gamma\vdash_{e}e:A\rhd e^{\prime}$, then
$|e^{\prime}|=e$.

###  5.4. Behavioral equivalence

We also show that $\lambda^{\mu<:}_{Fi}$ with iso-recursive subtyping is sound
and complete with respect to a calculus with equi-recursive subtyping in terms
of dynamic semantics. Since there are no changes to the reduction rules, the
proof of $\lambda^{\mu<:}_{Fi}$ to equi-recursive behavioral equivalence by
erasure of cast operators remains the same as Theorem 3.8. The proof of the
other direction comes almost for free as well. We simply follow the same steps
as described in §4.3 and use the same lemmas and theorems to show the
completeness of $\lambda^{\mu<:}_{Fi}$ in preserving the equi-recursive
reductions, except that during the proof of Lemma 4.3, we may need to insert
an application of rule ETyp-isub at certain points to prove that the encoding
is well-typed. In terms of dynamic semantics, $\lambda^{\mu<:}_{Fi}$ is
equivalent to a calculus with equi-recursive subtyping.

###### Theorem 5.7 (Behavioral equivalence of $\lambda^{\mu<:}_{Fi}$).

For any expression $e$, $e^{\prime}$ and type $A$ in $\lambda^{\mu<:}_{Fi}$,
if $\cdot\vdash_{e}e:A\rhd e^{\prime}$, then

  1. (1)

$e\hookrightarrow^{*}_{e}v$ if and only if there exists $v^{\prime}$ such that
$e^{\prime}\hookrightarrow^{*}v^{\prime}$ and $|v^{\prime}|=v$.

  2. (2)

$e$ diverges if and only if $e^{\prime}$ diverges.

##  6\. Related Work

Throughout the paper, we have discussed some of the closest related work in
detail. This section covers additional related work.

#### Relating iso-recursive and equi-recursive types

Recursive types were first introduced by Morris, who presented equi-recursive
types to model recursive definitions. Later on, iso-recursive types were
introduced (Harper and Mitchell, 1993; Gunter, 1992; Crary et al., 1999). The
terms for these two types of recursive formulations were coined by Crary et
al..

Both equi-recursive and iso-recursive types have been applied in various
programming language areas. Equi-recursive types are used in several contexts,
including: session types (Castagna et al., 2009; Chen et al., 2014; Gay and
Hole, 2005; Gay and Vasconcelos, 2010), gradual typing (Siek and Tobin-
Hochstadt, 2016), and the foundation of Scala through Dependent object types
(DOT) (Amin et al., 2016; Rompf and Amin, 2016), among others. Iso-recursive
types have also been utilized in different calculi and language designs due to
their ease of use in type checking (Abadi and Cardelli, 1996; Bengtson et al.,
2011; Chugh, 2015; Duggan, 2002; Lee et al., 2015; Swamy et al., 2011).

Urzyczyn (1995) studied the relationship between positive iso- and equi-
recursive types, showing their equivalence in typing power. Closer to our
work, Abadi and Fiore (1996) explored translating equi-recursive terms to iso-
recursive terms using explicit coercion functions but did not address the
operational semantics. Moreover, their behavioral equivalence argument relies
on a program logic which was conjectured to be sound. As we have argued in
Section 2.3, the use of explicit coercions has important drawbacks. Firstly,
it adds significant computational overhead to the encoding, making the
encoding impractical. Secondly, it introduces major complications to
reasoning, and also prevents a round-tripping property. By using casts, we
avoid both of these issues, leading to an easier, and fully formalized, way to
establish behavioral equivalence.

Recently, Patrignani et al. (2021) examined the contextual equivalence between
iso- and equi-recursive types, providing a mechanized proof in Coq for fully
abstract compilers. Their focus was on the compilation from iso-recursive to
equi-recursive types. They proved that the translation from iso-recursive to
equi-recursive types, by erasing unfold/fold operations, is fully abstract
with respect to contextual equivalence. The work also covered the compiler
from term-level fixpoints to equi-recursive types, but did not explore the
translation from equi-recursive to iso-recursive types. In our work, we
establish the bidirectional equivalence between full iso-recursive and equi-
recursive types, taking into account both typing and operational semantics.
Furthermore, in addition to type equality, we also study calculi with
subtyping, which have not been covered in previous work studying the
relationship between iso- and equi-recursive typing.

#### Subtyping recursive types

Amadio and Cardelli (1993) were the first to present a comprehensive formal
study of subtyping with equi-recursive types. This work inspired further
research that refined and simplified the original study (Brandt and Henglein,
1998; Gapeyev et al., 2002; Danielsson and Altenkirch, 2010; Komendantsky,
2011). In particular, Brandt and Henglein (1998) introduced a fixpoint rule
for a coinductive relation within an inductive framework. Their rules give
rise to a natural operational interpretation of proofs as coercions, as they
indicated as future work in their paper. Our work is inspired by their work,
and we formally present an operational interpretation of equi-recursive
equalities in our paper. However, instead of using coercions to model the
subtyping relation as they suggested, we use cast operators to model the
equalities between equi-recursive types. Furthermore, we show that our
computationally irrelevant cast operators simplify the metatheory and extend
to subtyping as well.

Iso-recursive subtyping, notably through the Amber rules introduced by
Cardelli (Cardelli, 1985), has long been used in practice. The iso-recursive
Amber rules, while easy to implement, are difficult to reason with formally.
The only known direct proof for transitivity of subtyping for an algorithmic
version of the Amber rules was given by Bengtson et al. (2011). However this
proof relies on a complex inductive argument and was found difficult to
formalize in theorem provers (Backes et al., 2014; Zhou et al., 2022). Zhou et
al., proposed alternative formulations of iso-recursive subtyping, which are
equivalent to the Amber rules and are also easier to reason with. Their work
comes with a comprehensive formalization of the metatheory of iso-recursive
subtyping. Our work is based on some of their findings. In particular we reuse
their mechanized proof of the unfolding lemma to show the type soundness of
iso-recursive subtyping, but instead apply it in a setting with full iso-
recursive types. Thus, we extend their work to a more general setting, in
terms of typing and operational semantics.

To address the complexities of iso-recursive subtyping, several alternative
formulations of iso-recursive subtyping have been proposed. Hofmann and Pierce
(1995) introduced a subtyping relation that limits recursive subtyping to
covariant types only, making the rules more restrictive than the Amber rules.
Ligatti et al. (2017) offered a broader subtyping relation for iso-recursive
types, allowing a recursive type and its unfolded version to be considered
subtypes of each other. This approach extends the iso-recursive Amber rules
but is still not complete with respect to the equi-recursive subtyping, since
it does not consider types not directly related by unfolding or folding as
subtypes. Additionally, Rossberg (2023) developed a calculus for higher-order
iso-recursive subtyping, to handle mutually recursive types more effectively.

#### Mechanizing recursive types

Danielsson and Altenkirch (2010); Jones and Pearce (2016) formalized equi-
recursive subtyping relations in Agda using a mixed coinduction and induction
technique. Jones and Pearce presented a semantic interpretation of subtyping
and proved that their semantic interpretation is sound with respect to an
inductive interpretation of types, but they did not lift their results to
cover function types. Instead, they focused on other constructs like product
and sum types. Danielsson and Altenkirch are closer to our work since they
also did not consider semantic interpretations, but formalized in Agda an
alternative equi-recursive subtyping relation that allows an explicit
transitivity rule to be included. They formally proved that this relation is
equivalent to the tree model of subtyping as well as Brandt and Henglein’s
subtyping relation. In a similar vein, Komendantsky (2011) showed how to
implement mixed coinduction and induction within Coq, formalizing rules that
closely resemble those introduced by Danielsson and Altenkirch (2010). They
also validated their approach against Amadio and Cardelli’s tree model of
subtyping. Zhou et al. (2022) focused on formalizing Amber-style iso-recursive
subtyping in Coq, adding to the understanding of iso-recursive subtyping.
Patrignani et al. (2021), which we have discussed earlier, formalized three
calculi in Coq: a simply typed lambda calculus extended with iso-recursive
types, equi-recursive types, and term-level fixpoints. Their work is focused
on the translation from iso-recursive to equi-recursive types, by erasing
unfold/fold operations, and the translation from a calculus with term-level
fixpoints to a calculus with equi-recursive types. All of our results are
mechanized in Coq, with the exception of the decomposition lemma (Theorem
5.5). This lemma is implied from Amadio and Cardelli’s work, but relies on a
significant amount of technical machinery, which we have not formalized in
Coq. Thus we assume it as an axiom in our Coq formalization.

#### Casts for type-level computation

In this paper, we employ explicit cast operators to represent the
transformations between types related by equi-recursive equalities. Several
studies (Stump et al., 2009; Sjöberg et al., 2012; Kimmell et al., 2012;
Sjöberg and Weirich, 2015; Cretin, 2014; Sulzmann et al., 2007; Gundry, 2013;
Weirich et al., 2017; Yang and Oliveira, 2019) have also used explicit casts
for managed type-level computation. However, casts in those approaches
primarily address type-level computations within contexts such as dependent
types or type-level programming, rather than the operational interpretation of
recursive type equalities. When considering the dynamic semantics of cast-like
operations, there have been two major approaches. One approach is to use an
elaboration semantics, used in works like (Sjöberg et al., 2012; Sjöberg and
Weirich, 2015; Stump et al., 2009), where the semantics are only defined for a
cast-free language and the casts need to be erased before execution. Another
approach is to use push rules as seen in (Sulzmann et al., 2007; Yorgey et
al., 2012; Weirich et al., 2013, 2017), which is the approach that we adopt in
our work. Pure Iso-type Systems (PITS) (Yang and Oliveira, 2019) provides a
generalization of iso-recursive types with explicit casts, but their focus is
on unifying the syntax of terms and types while retaining decidable type
checking, instead of subsuming equi-recursive type casting as we do. Also, the
form of casts is different from ours. For example, they do not have a fixpoint
cast, to enable coinductive reasoning.

##  7\. Conclusion

This paper proposes full iso-recursive types, a generalization of iso-
recursive types that can be used to encode the full power of equi-recursive
types. The key idea is to introduce a computationally irrelevant cast operator
in the term language that captures all the equi-recursive type equalities. We
present $\lambda^{\mu}_{Fi}$, a calculus that extends simply typed lambda
calculus with full iso-recursive types. $\lambda^{\mu}_{Fi}$ is proved to be
type sound and has the same expressive power as a calculus with equi-recursive
types, in terms of typing and dynamic semantics. Our results can also be
extended to subtyping, by encoding equi-recursive subtyping using iso-
recursive subtyping with cast operators.

As future work, we plan to extend $\lambda^{\mu}_{Fi}$ with other programming
language features, such as polymorphism and intersection and union types. It
is also interesting to see whether our results can scale to real world
languages (e.g. Haskell). In particular, it would be interesting to employ
full iso-recursive types in an internal target language with explicit cast
operators for a source language using equi-recursive types.

## References

  * (1)
  * Abadi and Cardelli (1996) Martin Abadi and Luca Cardelli. 1996.  _A theory of objects_.  Springer Science & Business Media.
  * Abadi and Fiore (1996) Martin Abadi and Marcelo P Fiore. 1996.  Syntactic considerations on recursive types. In _Proceedings 11th Annual IEEE Symposium on Logic in Computer Science_. IEEE, 242–252.
  * Amadio and Cardelli (1993) Roberto M Amadio and Luca Cardelli. 1993.  Subtyping recursive types.  _ACM Transactions on Programming Languages and Systems (TOPLAS)_ 15, 4 (1993), 575–631.
  * Amin et al. (2016) Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016.  The essence of dependent object types.  _A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday_ (2016), 249–272.
  * Backes et al. (2014) Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2014.  Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations.  _J. Comput. Secur._ 22, 2 (mar 2014), 301–353.
  * Bengtson et al. (2011) Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D Gordon, and Sergio Maffeis. 2011.  Refinement types for secure implementations.  _ACM Transactions on Programming Languages and Systems (TOPLAS)_ 33, 2 (2011), 1–45.
  * Brandt and Henglein (1998) Michael Brandt and Fritz Henglein. 1998.  Coinductive axiomatization of recursive type equality and subtyping.  _Fundamenta Informaticae_ 33, 4 (1998), 309–338.
  * Cardelli (1985) Luca Cardelli. 1985.  Amber, Combinators and Functional Programming Languages.  _Proc. of the 13th Summer School of the LITP, Le Val D’Ajol, Vosges (France)_ (1985).
  * Castagna et al. (2009) Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. 2009.  Foundations of session types. In _Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming_. 219–230.
  * Chen et al. (2014) Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2014.  On the preciseness of subtyping in session types. In _Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming_. 135–146.
  * Chugh (2015) Ravi Chugh. 2015.  IsoLATE: A type system for self-recursion. In _Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 24_. Springer, 257–282.
  * Crary et al. (1999) Karl Crary, Robert Harper, and Sidd Puri. 1999.  What is a recursive module?. In _Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation_. 50–63.
  * Cretin (2014) Julien Cretin. 2014.  _Erasable coercions: a unified approach to type systems_.  Ph. D. Dissertation. Université Paris-Diderot-Paris VII.
  * Danielsson and Altenkirch (2010) Nils Anders Danielsson and Thorsten Altenkirch. 2010.  Subtyping, declaratively: An exercise in mixed induction and coinduction. In _Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings 10_. Springer, 100–118.
  * Duggan (2002) Dominic Duggan. 2002.  Type-safe linking with recursive DLLs and shared libraries.  _ACM Transactions on Programming Languages and Systems (TOPLAS)_ 24, 6 (2002), 711–804.
  * Gapeyev et al. (2002) Vladimir Gapeyev, Michael Y Levin, and Benjamin C Pierce. 2002.  Recursive subtyping revealed.  _Journal of Functional Programming_ 12, 6 (2002), 511–548.
  * Gay and Hole (2005) Simon Gay and Malcolm Hole. 2005.  Subtyping for session types in the pi calculus.  _Acta Informatica_ 42 (2005), 191–225.
  * Gay and Vasconcelos (2010) Simon J Gay and Vasco T Vasconcelos. 2010.  Linear type theory for asynchronous session types.  _Journal of Functional Programming_ 20, 1 (2010), 19–50.
  * Gundry (2013) Adam Michael Gundry. 2013.  Type inference, Haskell and dependent types.  (2013).
  * Gunter (1992) Carl A Gunter. 1992.  _Semantics of programming languages: structures and techniques_.  MIT press.
  * Harper and Mitchell (1993) Robert Harper and John C Mitchell. 1993.  On the type structure of Standard ML.  _Acm transactions on programming languages and systems (TOPLAS)_ 15, 2 (1993), 211–252.
  * Harper and Stone (2000) Robert Harper and Christopher Stone. 2000.  A type-theoretic interpretation of Standard ML.  (2000).
  * Hofmann and Pierce (1995) Martin Hofmann and Benjamin Pierce. 1995.  Positive subtyping. In _Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages_. 186–197.
  * Jones and Pearce (2016) Timothy Jones and David J Pearce. 2016.  A mechanical soundness proof for subtyping over recursive types. In _Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs_. 1–6.
  * Kimmell et al. (2012) Garrin Kimmell, Aaron Stump, Harley D Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and Ki Yung Ahn. 2012.  Equational reasoning about programs with general recursion and call-by-value semantics. In _Proceedings of the sixth workshop on Programming languages meets program verification_. 15–26.
  * Komendantsky (2011) Vladimir Komendantsky. 2011.  Subtyping by folding an inductive relation into a coinductive one. In _International Symposium on Trends in Functional Programming_. Springer, 17–32.
  * Lee et al. (2015) Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. 2015.  A theory of tagged objects. In _29th European Conference on Object-Oriented Programming (ECOOP 2015)_. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
  * Ligatti et al. (2017) Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. 2017.  On subtyping-relation completeness, with an application to iso-recursive types.  _ACM Transactions on Programming Languages and Systems (TOPLAS)_ 39, 1 (2017), 1–36.
  * Morris (1968) James H Morris. 1968.  Lambda calculus models of programming languages.  (1968).
  * Patrignani et al. (2021) Marco Patrignani, Eric Mark Martin, and Dominique Devriese. 2021.  On the semantic expressiveness of recursive types.  _Proceedings of the ACM on Programming Languages_ 5, POPL (2021), 1–29.
  * Pierce (2002) Benjamin C Pierce. 2002.  _Types and programming languages_.  MIT press.
  * Rompf and Amin (2016) Tiark Rompf and Nada Amin. 2016.  Type soundness for dependent object types (DOT). In _Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications_. 624–641.
  * Rossberg (2023) Andreas Rossberg. 2023.  Mutually Iso-Recursive Subtyping.  _Proceedings of the ACM on Programming Languages_ 7, OOPSLA2 (2023), 347–373.
  * Siek and Tobin-Hochstadt (2016) Jeremy G Siek and Sam Tobin-Hochstadt. 2016.  The recursive union of some gradual types.  In _A List of Successes that can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday_. Springer, 388–410.
  * Sjöberg et al. (2012) Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich. 2012.  Irrelevance, heterogeneous equality, and call-by-value dependent type systems.  _arXiv preprint arXiv:1202.2923_ (2012).
  * Sjöberg and Weirich (2015) Vilhelm Sjöberg and Stephanie Weirich. 2015.  Programming up to congruence. In _Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_. 369–382.
  * Stump et al. (2009) Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, and Timothy Simpson. 2009.  Verified programming in Guru. In _Proceedings of the 3rd workshop on Programming languages meets program verification_. 49–58.
  * Sulzmann et al. (2007) Martin Sulzmann, Manuel MT Chakravarty, Simon Peyton Jones, and Kevin Donnelly. 2007.  System F with type equality coercions. In _Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation_. 53–66.
  * Swamy et al. (2011) Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011.  Secure distributed programming with value-dependent types.  _ACM SIGPLAN Notices_ 46, 9 (2011), 266–278.
  * Urzyczyn (1995) Pawel Urzyczyn. 1995.  Positive recursive type assignment. In _International Symposium on Mathematical Foundations of Computer Science_. Springer, 382–391.
  * Vanderwaart et al. (2003) Joseph C Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, and Perry Cheng. 2003.  Typed compilation of recursive datatypes.  _ACM SIGPLAN Notices_ 38, 3 (2003), 98–108.
  * Weirich et al. (2013) Stephanie Weirich, Justin Hsu, and Richard A Eisenberg. 2013.  System FC with explicit kind equality.  _ACM SIGPLAN Notices_ 48, 9 (2013), 275–286.
  * Weirich et al. (2017) Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A Eisenberg. 2017.  A specification for dependent types in Haskell.  _Proceedings of the ACM on Programming Languages_ 1, ICFP (2017), 1–29.
  * Yang and Oliveira (2019) Yanpeng Yang and Bruno CDS Oliveira. 2019.  Pure iso-type systems.  _Journal of Functional Programming_ 29 (2019), e14.
  * Yorgey et al. (2012) Brent A Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, Dimitrios Vytiniotis, and José Pedro Magalhães. 2012.  Giving Haskell a promotion. In _Proceedings of the 8th ACM SIGPLAN Workshop on Types in Language Design and Implementation_. 53–66.
  * Zhou et al. (2020) Yaoda Zhou, Bruno C d S Oliveira, and Jinxu Zhao. 2020.  Revisiting iso-recursive subtyping.  _Proceedings of the ACM on Programming Languages_ 4, OOPSLA (2020), 1–28.
  * Zhou et al. (2022) Yaoda Zhou, Jinxu Zhao, and Bruno CDS Oliveira. 2022.  Revisiting Iso-recursive subtyping.  _ACM Transactions on Programming Languages and Systems (TOPLAS)_ 44, 4 (2022), 1–54.