Full Iso-Recursive Types
LITAO ZHOU, University of Hong Kong, China
QIANYONG WAN, University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, University of Hong Kong, China
There are two well-known formulations of recursive types: iso-recursive and equi-recursive types. Abadi andFiore [1996] have shown that iso- and equi-recursive types have the same expressive power. However, theirencoding 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 ofthe 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 canbe 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 𝜆𝐹𝑖 , which𝜇extends the simply typed lambda calculus (STLC) with full iso-recursive types. The 𝜆𝐹𝑖 calculus is proved tobe 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.
CCS Concepts: • Theory of computation → Type theory; • Software and its engineering → Object
oriented languages.
Additional Key Words and Phrases: Recursive types, Subtyping, Type system
ACM Reference Format:
Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira. 2024. Full Iso-Recursive Types. Proc. ACM Program.
Lang. 8, OOPSLA2, Article 278 (October 2024), 30 pages. https://doi.org/10.1145/3689718

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-recursiveand equi-recursive types. With equi-recursive types [Morris 1968], a recursive type 𝜇𝛼 . 𝐴 and its
unfolding 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴] 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 relationshipbetween 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 suchas whether the expressive power of the two formulations is the same or not. Urzyczyn proved thatthese two formulations have the same expressive power when the types considered are restricted to
Authors’ Contact Information: Litao Zhou, University of Hong Kong, Hong Kong, China, ltzhou@cs.hku.hk; Qianyong Wan,
University of Hong Kong, Hong Kong, China, qywan@cs.hku.hk; Bruno C. d. S. Oliveira, University of Hong Kong, Hong
Kong, China, bruno@cs.hku.hk.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/10-ART278
https://doi.org/10.1145/3689718

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:2

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

be positive. Abadi and Fiore extended Urzyczyn’s result and showed that unrestricted formulationsof 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 isfully 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 isorecursive 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 thetyping expressiveness and behavioral equivalence seen in equi-recursive types. Instead of fold andunfold operators and explicit coercions, we use a more general notion of computationally irrelevant
cast operators [Cretin 2014; Sulzmann et al. 2007], which allow transformations on any types thatare equivalent in an equi-recursive setting. Full iso-recursive types can encode all programs withequi-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 acomplete proof, compared to Abadi and Fiore’s work.
𝜇
We present a calculus called 𝜆𝐹𝑖 , which extends the simply typed lambda calculus (STLC) with full𝜇
iso-recursive types. The 𝜆𝐹𝑖 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 𝜆𝐹𝑖 , and an erasure function that removes
all casts from full iso-recursive terms to obtain equi-recursive terms. Moreover, the terminationand divergence behavior of programs is preserved under the elaboration and erasure operations.
𝜇Therefore, 𝜆𝐹𝑖 is sound and complete w.r.t. the calculus with equi-recursive types in terms of bothtyping and dynamic semantics. On the other hand, traditional iso-recursive types can be seen asa special case of full iso-recursive types. One can easily recover the traditional unfold and foldoperators 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.
Our results extend to subtyping: equi-recursive subtyping can be expressed in terms of isorecursive subtyping with cast operators. Although subtyping between equi-recursive types [Amadio
and Cardelli 1993; Brandt and Henglein 1998; Gapeyev et al. 2002] and subtyping between isorecursive types [Abadi and Cardelli 1996; Zhou et al. 2022] has been studied in depth, the relationshipbetween the two approaches has been largely unexplored. We revisit Amadio and Cardelli [1993]’s
seminal work on equi-recursive subtyping and observe that equi-recursive subtyping can be
decomposed into a combination of equi-recursive equalities and iso-recursive subtyping. Since𝜇<:our cast operators can capture all the equi-recursive equalities, in the calculus 𝜆𝐹𝑖 extended with
subtyping, we can achieve a simple encoding of equi-recursive subtyping.

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:3

The implications of full iso-recursive types are two-fold: theoretical and practical. Theoretically,full iso-recursive types offer the expressive power of equi-recursive types but with a more manageable metatheory. This allows for future extensions with more advanced type system features.
Complex type system features, such as type-level lambdas found in System 𝐹𝜔 [Cai et al. 2016],
can lead to undecidable type equivalence relations with equi-recursive types. Iso-recursive types
provide explicit control over folding and unfolding, avoiding issues with undecidability. This advantage is underscored in work on recursive modules [Crary et al. 1999], which adopted iso-recursive
types to obtain more practical module systems with decidable type equivalence [Dreyer 2005;
Dreyer et al. 2001; Russo 2001] in settings similar to System 𝐹𝜔 . Rossberg [2023] also pointed outthat iso-recursive types enjoy efficient meta operations, such as type equivalence checking. Full
iso-recursive types enhance these benefits by retaining the expressive power of equi-recursive
types without adding runtime computational overhead. Beyond avoiding decidability limitations,(full) iso-recursive types also simplify other theoretical challenges seen in equi-recursive types,
particularly in the presence of subtyping. For example, the integration of bounded quantification
with equi-recursive subtyping introduces substantial complexity [Colazzo and Ghelli 2005; Ghelli
1993; Jeffrey 2001]. In contrast, with iso-recursive types these extensions are natural and straight𝜇<:
forward [Zhou et al. 2023]. Since the subtyping rules we adopt in 𝜆𝐹𝑖 are standard, previous results
on iso-recursive subtyping can potentially be extended to full iso-recursive types too.
Full iso-recursive types also open the path for new applications. In the design of realistic compilers,
it is common to have source languages that are lightweight in terms of type annotations; andtarget languages, which are used internally, that are heavy on annotations, but are simple to typecheck [Crary 2000]. 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 GHC. In this scenario it is important that no computational overhead is introduced during
the elaboration, which is why using standard iso-recursive types is not practical. In addition, source
languages could also use full iso-recursive types directly, and explicit casts could be hidden into
language constructs (such as constructors, method calls and/or pattern matching) or inferred by
the type system to reduce the overhead of writing annotations. This is 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: a novel formulation of recursive types, which generalizes the
traditional iso-recursive fold and unfold operators to cast operators.
𝜇• The 𝜆𝐹𝑖 calculus, which extends the STLC with full iso-recursive types. We present a typesystem, a call-by-value operational semantics, and a type soundness proof.
𝜇• Equivalence to equi-recursive types. We show that 𝜆𝐹𝑖 is equivalent to STLC extended
with equi-recursive types in terms of typing and dynamic semantics.
𝜇<:𝜇• Extension to subtyping. We present 𝜆𝐹𝑖 , an extension of 𝜆𝐹𝑖 with iso-recursive subtyping,𝜇<:and show the same metatheory results for 𝜆𝐹𝑖 , namely, type soundness, typing equivalenceand behavioral equivalence to equi-recursive types with subtyping.
• Coq formalization and proofs for all the new metatheory results of full iso-recursive types,
except for Theorem 5.5, which is adapted from the literature [Amadio and Cardelli 1993].
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:4

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira(Equi-recursive Equality)

𝐴𝐵
Tyeq-contract

𝐴[𝛼 ↦→ 𝐵 1 ]  𝐵 1

𝐴[𝛼 ↦→ 𝐵 2 ]  𝐵 2

𝐴 is contractive in 𝛼

𝜇𝛼 . 𝐴  𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴]

𝐵1  𝐵2
Tyeq-mu-cong𝐴𝐵
𝜇𝛼 . 𝐴  𝜇𝛼 . 𝐵

Tyeq-trans

𝐴𝐵

𝐵 𝐶

𝐴 𝐶

Tyeq-unfold

Tyeq-symm

Tyeq-arr

Tyeq-refl𝐴𝐵

𝐴1  𝐴2𝐴𝐴

𝐵𝐴

𝐴1 → 𝐵 1  𝐴2 → 𝐵 2

𝐵1  𝐵2

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

2

Overview

This section provides an overview of our work. We first briefly review the two main approaches torecursive 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 equirecursive 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Γ ⊢𝑒 :𝐴𝐴𝐵

Γ ⊢𝑒 :𝐵
The metatheory of equi-recursive types has been studied by Amadio and Cardelli [1993]. They
proposed a tree model for specifying equality (or subtyping). In essence, two recursive types areequal (or subtypes) if their infinite unfoldings are equal (or subtypes). The tree model provides aclear and solid foundation for the interpretation of equi-recursive types.
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 𝐴[𝛼]. Note that 𝐴 needs to be contractive in 𝛼, i.e. either 𝛼 is not free in 𝐴 or 𝐴
can be unfolded to a type of the form 𝐴1 → 𝐴2 . This is to prevent equating arbitrary types using
non-contractive type functions, such as when 𝐴 is 𝛼. 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 𝐴[𝛼] = Int → Int → 𝛼, then 𝐵 1 = 𝜇𝛼 . Int → Int → 𝛼 and 𝐵 2 = 𝜇𝛼 . Int → 𝛼 areequal according to rule Tyeq-contract:
𝐵 1  𝐴[𝛼 ↦→ 𝐵 1 ]...
𝐵 2  𝐴[𝛼 ↦→ 𝐵 2 ]𝐴 is contractive in 𝛼
Tyeq-contract
𝜇𝛼 . Int → Int → 𝛼  𝜇𝛼 . Int → 𝛼

Tyeq-unfold

Here, the missing derivation is:
Tyeq-refl
Tyeq-unfold
Int  Int𝜇𝛼 . Int → 𝛼  Int → 𝜇𝛼 . Int → 𝛼
Tyeq-arrow
Int → 𝐵 2  Int → Int → 𝐵 2
Tyeq-trans and Tyeq-unfold
𝐵 2  𝐴[𝛼 ↦→ 𝐵 2 ]Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:5

𝐻 ⊢𝐴 𝐵

(Inductive Equi-recursive Equality)

Tye-assump

Tye-trans

𝐴=𝐵∈𝐻

Tye-refl

𝐻 ⊢𝐴 𝐵

𝐻 ⊢𝐴 𝐴

𝐻 ⊢𝐴 𝐵

𝐻 ⊢𝐵 𝐶

𝐻 ⊢𝐴 𝐶

Tye-symm

Tye-arrfix

𝐻 ⊢𝐴 𝐵

𝐻, 𝐴1 → 𝐵 1 = 𝐴2 → 𝐵 2 ⊢ 𝐴1  𝐴2

𝐻 ⊢𝐵 𝐴

Tye-unfold

𝐻 ⊢ 𝜇𝛼 . 𝐴  𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴]
𝐻, 𝐴1 → 𝐵 1 = 𝐴2 → 𝐵 2 ⊢ 𝐵 1  𝐵 2

𝐻 ⊢ 𝐴1 → 𝐵 1  𝐴2 → 𝐵 2

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

Despite its equivalence to the tree model, Amadio and Cardelli’s axiomatization is not easy to use
in practice. The type function 𝐴 in rule Tyeq-contract and the intermediate type 𝐵 in rule Tyeqtrans are not directly derivable from the equality conclusion. Thus, Amadio and Cardelli’s rule
does not form an algorithm for equi-recursive equality, but rather it is a declarative specification.
Later on, there have been a few alternative axiomatizations of equi-recursive types [Brandt andHenglein 1998; Danielsson and Altenkirch 2010; Gapeyev et al. 2002], which are all proved to beequivalent to the tree model. Among them, Brandt and Henglein proposed an inductively defined
relation 𝐻 ⊢ 𝐴  𝐵 for equi-recursive type equality, shown in Figure 2. 𝐻 is a list of type equality
assumptions that is used to derive the equality 𝐴  𝐵. New equalities are added to 𝐻 every timefunction 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. Moreover,Brandt and Henglein showed a terminating algorithm for checking type equality using their rules.
Therefore, we choose Brandt and Henglein’s axiomatization as the basis for our work.
2.2

Iso-Recursive Types

Iso-recursive types [Crary et al. 1999] are a different approach that treats recursive types and theirunfoldings 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-foldshow 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

Typ-foldΓ ⊢ 𝑒 : 𝜇𝛼 . 𝐴Γ ⊢ 𝑒 : 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴]Γ ⊢ unfold [𝜇𝛼 . 𝐴] 𝑒 : 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴]Γ ⊢ fold [𝜇𝛼 . 𝐴] 𝑒 : 𝜇𝛼 . 𝐴

One advantage of iso-recursive types, as we discussed in §1, is that they are easier to extend to
more complex type systems, which may easily make the type equality relation undecidable orcomplicate the metatheory. Instead, iso-recursive types utilize explicit fold/unfold annotations
to control type-level conversions, thus avoiding these issues. One disadvantage of iso-recursive
types is their inconvenience in use due to the explicit fold and unfold operators. However, thisdisadvantage can be mitigated by hiding folding and unfolding under other language constructs,
such as pattern matching, constructors or method calls [Crary et al. 1999; Harper and Stone 2000;
Lee et al. 2015; Pierce 2002; Vanderwaart et al. 2003; Yang and Oliveira 2019; Zhou et al. 2022]. As
we shall see in §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.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:6

2.3

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

Relating Iso-Recursive and Equi-Recursive Types

The relationship between iso-recursive types and equi-recursive types has been a subject of study
in the literature [Abadi and Fiore 1996; Patrignani et al. 2021; Urzyczyn 1995]. This subsection
reviews existing approaches to relate the two approaches and their issues.
Encoding iso-recursive types. Encoding of iso-recursive types in terms of equi-recursive types isstraightforward, simply by erasing the fold and unfold operators [Abadi and Fiore 1996]. Since therule Tyeq-unfold states that a recursive type is equal to its unfolding, it is easy to see that theencoding is type preserving. The encoding is also behavior preserving, since the reduction ruleswith fold and unfold operators will become no-ops when erased, as shown below:
Red-fld

Red-ufd𝑒 ↩→ 𝑒 ′𝑒 ↩→ 𝑒 ′fold [𝐴] 𝑒 ↩→ fold [𝐴] 𝑒 ′unfold [𝐴] 𝑒 ↩→ unfold [𝐴] 𝑒 ′Red-elim

unfold [𝐴] (fold [𝐵] 𝑣) ↩→ 𝑣

Notice that in the process of reducing folded and unfolded expression 𝑒, we merely reduce 𝑒. The
type 𝐴 does not influence the reduction of 𝑒. Eventually, when 𝑒 reaches a value 𝑣, an unfold cancels
a fold and we simply obtain 𝑣. The two type annotations in rule Red-elim can be arbitrary. In a well
typed term, 𝐴 and 𝐵 must be recursive types that are equal or in a subtyping relation, depending on
the whether recursive subtyping is considered, but the reduction rule in its general form does not
require this, and the type annotations do not affect the result 𝑣 either. In other words, folding andunfolding 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 theirunfoldings as equal, we need to insert explicit fold and unfold operators in the iso-recursive setting totransform between equal types. For example, let 𝑒 be a function that keeps taking integer arguments
and returning itself, which can be typed as a recursive type 𝜇𝛼 . Int → 𝛼. In an equi-recursive
setting, (𝑒 1) can be typed as 𝜇𝛼 . Int → 𝛼, by using the rule Typ-eq and rule Tyeq-unfold to unfold
the recursive type to Int → (𝜇𝛼 . Int → 𝛼) so that 𝑒 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:⊢ 𝑒 : 𝜇𝛼 . Int → 𝛼
Typ-unfold⊢ unfold [𝜇𝛼 . Int → 𝛼] 𝑒 : Int → (𝜇𝛼 . Int → 𝛼)
⊢ 1 : Int
Typ-app⊢ (unfold [𝜇𝛼 . Int → 𝛼] 𝑒) 1 : 𝜇𝛼 . Int → 𝛼
Fold/unfold is not enough: computationally relevant explicit coercions. The above example showsthat, 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 𝜇𝛼 . Int → Int → 𝛼 and 𝜇𝛼 . Int → 𝛼 are also equal in the equi-recursive setting, but they are
not directly related by fold and unfold operators. The two types have different arities of function
arguments in the recursive body, while fold and unfold operators only transform between different
views of the same recursive structure. Thus, fold and unfold operations alone cannot achieve thistransformation. More sophisticated operations are needed to fully encode equi-recursive equalities.
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 𝐴 and 𝐵 considered to be equal
following the derivation in Figure 1, there exists a coercion function 𝑓 : 𝐴 → 𝐵 that can be applied
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:7

to terms of type 𝐴 to obtain terms of type 𝐵. 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 helpof explicit coercion functions.
One issue is that the insertion of coercion functions affects the computational structure of theterms. For example, assume that 𝑒 has a function type Int → Int → (𝜇𝛼 . Int → 𝛼). This type canbe partially folded to Int → (𝜇𝛼 . Int → 𝛼). In an equi-recursive setting, due to the rule Typ-eq,
the term 𝑒 can be assigned the type Int → (𝜇𝛼 . Int → 𝛼) directly 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𝜆(𝑥 : Int → Int → 𝜇𝛼 . Int → 𝛼). 𝜆(𝑦 : Int). fold [𝜇𝛼 . Int → 𝛼] (𝑥 𝑦)Now, applying the coercion function to 𝑒 results in a term of type Int → (𝜇𝛼 . Int → 𝛼). Unfortunately, such explicit coercion functions are computationally relevant. They introduce an extra
function application. Thus, an encoding of equi-recursive types in terms of iso-recursive types canintroduce non-trivial computational overhead. The issue is particularly problematic because somecoercions need to essentially be recursive functions, which is the case for 𝜇𝛼 . Int → 𝛼  𝜇𝛼 . Int →Int → 𝛼. 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 inparticular 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:(𝜆(𝑥 : Int → Int → 𝜇𝛼 . Int → 𝛼). 𝜆(𝑦 : Int). (𝑥 𝑦)) 𝑒(1)This term is equivalent to 𝑒 under 𝛽− and 𝜂−reduction, but it is not the same as 𝑒 anymore. In
more complicated cases, especially for derivations involving the use of rule Tyeq-contract, one
needs to use complex coercion function combinators to achieve the encoding. In turn, this leads toa more significant change in the syntactic structure of the terms, making it difficult to reason about
the behavior preservation of the encoding. 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 isconjectured to be sound, and the authors did not consider an operational semantics. Thus, while itis 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

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

ACSub-arrow

𝐴𝐵Σ ⊢ 𝐵 1 ≤ 𝐴1

Σ⊢𝐴 ≤𝐵Σ ⊢ 𝐴2 ≤ 𝐵 2

Σ ⊢ 𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2

ACSub-var

ACSub-rec𝛼≤𝛽∈ΣΣ, 𝛼 ≤ 𝛽 ⊢ 𝐴 ≤ 𝐵Σ⊢𝛼 ≤𝛽Σ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵

Two types are in a subtyping relation if their infinite unfoldings are equal, or equivalently, if they
can be proved by the Brandt and Henglein or Amadio and Cardelli’s axiomatization, as shown inrule 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, sincerule ACSub-rec was adopted by the implementation of the Amber programming language [Cardelli
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:8

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira1985]. The Amber rules are proved to be sound and complete to the tree model interpretation ofequi-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 isorecursive types [Abadi and Cardelli 1996; Bengtson et al. 2011; Chugh 2015; Duggan 2002; Lee et al.
2015; Swamy et al. 2011]. However, the metatheory for the iso-recursive Amber rules has not been
well studied until recently [Zhou et al. 2020, 2022]. 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.
Unlike type equality, the relation between equi-recursive and iso-recursive subtyping has beenless 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, 𝜇𝛼 . Int → 𝛼 ≤ 𝜇𝛼 . Int → Int → 𝛼 is a valid subtyping relation in theequi-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 theother 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 amore 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, thecorrectness 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 thatgeneralizes 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 betransformed to their equivalent type using the type casting relation. The rules Typ-unfold andTyp-fold are now replaced by the following rule:Typ-castΓ ⊢𝑒 :𝐴·; · ⊢ 𝐴 ↩→ 𝐵 : 𝑐Γ ⊢ cast [𝑐] 𝑒 : 𝐵
The type casting relation 𝐴 ↩→ 𝐵 : 𝑐 states that type 𝐴 can be cast to type 𝐵 using the casting
operator 𝑐. Essentially, the type casting relation is an equivalent form of Brandt and Henglein’s
type equality relation, augmented with a casting operator 𝑐, a new syntactic construct to witness
the proof of the type casting relation. There are a few different designs in our type casting relationcompared to the type equality relation in Figure 2 though. For example, we remove the rule Tyesymm from the type casting relation, for reasons that we will discuss in §4.2, and proved thatrule Tye-symm 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:
cast [id → fold (𝜇𝛼 . Int→𝛼 ) ] 𝑒
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:9

Here id is the identity casting operator, and fold𝜇𝛼 . Int→𝛼 is the casting operator that witnesses
the proof of a folding from Int → (𝜇𝛼 . Int → 𝛼) to 𝜇𝛼 . Int → 𝛼. Thus, the full iso-recursive
typing rules are equivalent to the equi-recursive typing rules. Moreover, the cast operators canbe automatically inferred and inserted into the terms. Brandt and Henglein present an algorithm
for finding equi-recursive subtyping derivations [Brandt and Henglein 1998, Figure 5], prove its
termination, and argue that their results also hold for type equality derivations. Since the algorithm
does not use the changed rules in our type casting relation, we can still use the same algorithm to𝜇automatically elaborate any terms written with equi-recursive types to 𝜆𝐹𝑖 . We identify the equi- tofull iso-recursive encoding as one of the key applications of our work, as already discussed in §1.
On the other hand, the unfolding and folding operators in standard iso-recursive types canbe recovered from our type casting relation. For example, the term (cast [fold𝐴 ] 𝑒) is essentiallyequivalent to (fold [𝐴] 𝑒), and the term (cast [unfold𝐴 ] 𝑒) is equivalent to (unfold [𝐴] 𝑒) in termsof typing and dynamic semantics, as we will show in the following sections. Therefore, full isorecursive types are a generalization of standard iso-recursive types.
Push Rules. The extended typing rules brings new challenges to the design of semantics and theproof of type soundness. With the casting operator, there are terms that are not simple unfoldings
or foldings of recursive types: the operational semantics needs to be extended to handle these terms.
For example, terms such as (cast [id → fold (𝜇𝛼 . Int→𝛼 ) ] 𝑒), which have no analogous representationin 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:
Red-cast𝑒 ↩→ 𝑒 ′Red-cast-arr

Red-cast-id

cast [𝑐] 𝑒 ↩→ cast [𝑐] 𝑒 ′ (cast [𝑐 1 → 𝑐 2 ] 𝑣 1 ) 𝑣 2 ↩→ cast [𝑐 2 ] (𝑣 1 (cast [¬𝑐 1 ] 𝑣 2 )) cast [id] 𝑣 ↩→ 𝑣
The reduction rules are designed in a call-by-value fashion, and we also define the cast of values offunction types (i.e. cast [𝑐 1 → 𝑐 2 ] 𝑣) 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 rulesin the design of calculi with coercions [Cretin 2014; Sulzmann et al. 2007]. Note that the casting
operator ¬𝑐 1 computes the dual of the casting operator 𝑐 1 , which is used to indicate the reverse
transformation that 𝑐 1 represents (e.g. ¬ fold𝜇𝛼 . 𝐴 = unfold𝜇𝛼 . 𝐴 , ¬ id = id). Intuitively, the pushrules are designed to ensure that the casting operators can be reduced to smaller constructs andapplied to the correct types, so that the reduction steps are always type preserving. We will reason
about the behavior of the push rules formally in §4.1. A running example of a reduction using thepush rules is shown as follows:(cast [id → fold (𝜇𝛼 . Int→𝛼 ) ] 𝑣) 1↩→ cast [fold (𝜇𝛼 . Int→𝛼 ) ] (𝑣 (cast [id] 1))↩→ cast [fold (𝜇𝛼 . Int→𝛼 ) ] (𝑣 1)(Red-cast-arr)(Red-cast-id and Red-cast)

A key result of our work is the type soundness of the full iso-recursive calculus, which is provedby showing that the push rules preserve the type of the terms and the type casting relation. Thisis one step beyond Brandt and Henglein’s work, where a coercion typing rule similar to ourcasting rules was introduced, but no results about the dynamic semantics were studied. Anothercontribution of our work is that with full iso-recursive types, we retain the computational structureof the terms when encoding equi-recursive types. 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. Unlike regular iso-recursive types, which requirecomputationally relevant term coercions for some type conversions, no such coercions are needed
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:10

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveirain our approach. For example, all the reduction steps in the example above are erased to the originalterm (𝑣 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 theencoded 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 thesame expressive power as equi-recursive types”.
Subtyping. Our results extend to subtyping. Our main observation is that the equi-recursive
subtyping relation can be defined by a combination of equi-recursive equality and the iso-recursive
subtyping relation [Abadi and Cardelli 1996; Cardelli 1985; Zhou et al. 2022], as shown below:
𝐴 ≤𝑒 𝐵 ≜ ∃ 𝐶 1 𝐶 2 . (𝐴  𝐶 1 ) ∧ (𝐶 1 ≤𝑖 𝐶 2 ) ∧ (𝐶 2  𝐵)
Here ≤𝑒 denotes an equi-recursive subtyping relation, and ≤𝑖 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 existingequi-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 isorecursive setting with subtyping. For example, given an equi-recursive term 𝑒 that has the type 𝐴
with 𝐴 ≤𝑒 𝐵, we can encode 𝑒 : 𝐵 in the full iso-recursive setting as ((cast [𝑐 2 ] (cast [𝑐 1 ] 𝑒 ′ )) : 𝐵), in
which 𝑐 1 and 𝑐 2 are casts encoding the equality relation 𝐴  𝐶 1 and 𝐶 2  𝐵, and 𝑒 ′ is the encodingof (𝑒 : 𝐴). 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 tothe 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 𝜆𝐹𝑖 . Our calculus isbased on the simply typed lambda calculus extended with recursive types and type cast operators.
3.1

Syntax and Well-Formedness𝜇The syntax of 𝜆𝐹𝑖 is shown at the top of Figure 3.
Types. Meta-variables 𝐴, 𝐵 range over types. Types include base types (Int), function types(𝐴1 → 𝐴2 ), type variables (𝛼), and recursive types (𝜇𝛼 . 𝐴).
Expressions. Meta-variables 𝑒 range over expressions. Most of the expressions are standard,
including: variables (𝑥), integers (n), applications (𝑒 1 𝑒 2 ) and lambda abstractions (𝜆𝑥 : 𝐴. 𝑒). We also
have a type cast operator (cast [𝑐] 𝑒) that transforms the type of the expression 𝑒 to an equivalenttype using the cast operator 𝑐. The cast operators 𝑐 include cast variables (𝜄), the identity cast (id),the fold and unfold casts (fold𝐴 and unfold𝐴 ), the arrow cast (𝑐 1 → 𝑐 2 ), the sequential cast (𝑐 1 ; 𝑐 2 ),and the fixpoint cast (fix 𝜄. 𝑐). We will define the type cast rules for these operators in §3.2.
Values. Meta-variables 𝑣 range over values. Integers (n) and lambda abstractions (𝜆𝑥 : 𝐴. 𝑒),
are considered as values, which are standard for a simply typed lambda calculus. In standard
iso-recursive types, the folding of a value is considered a value, since it serves as the canonicalform of a recursive type (e.g. fold [𝜇𝛼 . 𝐴] 𝑣 has the type 𝜇𝛼 . 𝐴) and there are no further reduction
rules for reducing fold [𝐴] 𝑣. Therefore, in our calculus the corresponding encoding (cast [fold𝐴 ] 𝑣)
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:11

Types
Expressions
ValuesCast Operators
Type Contexts
Typing Contexts
Type Cast Contexts

𝐴, 𝐵
𝑒
𝑣
𝑐
Δ
Γ
E

F
F
F
F
F
F
F

Int | 𝐴1 → 𝐴2 | 𝛼 | 𝜇𝛼 . 𝐴
𝑥 | n | 𝑒 1 𝑒 2 | 𝜆𝑥 : 𝐴. 𝑒 | cast [𝑐] 𝑒n | 𝜆𝑥 : 𝐴. 𝑒 | cast [fold𝐴 ] 𝑣 | cast [𝑐 1 → 𝑐 2 ] 𝑣
𝜄 | id | fold𝐴 | unfold𝐴 | 𝑐 1 → 𝑐 2 | 𝑐 1 ; 𝑐 2 | fix 𝜄. 𝑐
· | Δ, 𝛼· | Γ, 𝑥 : 𝐴· | E, 𝜄 : 𝐴 ↩→ 𝐵

Δ⊢A

(Well-formed Type)WFT-var

WFT-arrow

WFT-rec

WFT-int𝛼∈Δ

Δ⊢𝐴

Δ, 𝛼 ⊢ 𝐴

Δ ⊢ Int

Δ⊢𝛼

Δ⊢𝐵

Δ⊢𝐴→𝐵

Δ ⊢ 𝜇𝛼 . 𝐴
𝜇Fig. 3. Syntax and type well-formedness of 𝜆𝐹𝑖 .

is also considered a value. We also consider arrow casts of a value (cast [𝑐 1 → 𝑐 2 ] 𝑣) to be values,
since they cannot be reduced further without applying them to an argument.
Contexts and Well-formedness. Type contexts Δ track bound type variables 𝛼. A type is wellformed if all of its free variables are in the context. Well-formedness for types is standard, andshown at the bottom Figure 3. Typing contexts Γ track bound variables 𝑥 with their types. A typing
context is well-formed (⊢ Γ) if there are no duplicate variables and all the types are well-formed.
We also define a type cast context E to keep track of the cast variables 𝜄 and the cast operatorsthat they are associated with. This will be used in the type cast rules, defined in §3.2. For typevariables and term variables, we assume the usual notions of free and bound variables, and the usual
capture-avoiding substitution function, denoted by 𝐴[𝛼 ↦→ 𝐵], that replaces the free occurrencesof variable 𝛼 in 𝐴 by 𝐵, while avoiding the capture of any bound variable in 𝐴. When needed, we
assume that 𝛼-equivalence is applied at will to avoid the clashing of free variables.
3.2

Typing𝜇The top of Figure 4 shows the typing rules for 𝜆𝐹𝑖 . 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 Δ; E ⊢ A ↩→ B : 𝑐, Δ is the typecontext used to ensure that all the types in the cast derivation are well-formed. E tracks of the castvariables 𝜄 that appear in 𝑐 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 theability to encode the coinductive reasoning in equi-recursive equalities.
For instance, the equality 𝜇𝛼 . Int → Int → 𝛼  𝜇𝛼 . Int → 𝛼 that we have seen in §2.1 can be
encoded as the following type casting relation:
𝜇𝛼 . Int → Int → 𝛼 ↩→ 𝜇𝛼 . Int → 𝛼 :unfold𝜇𝛼 . Int→Int→𝛼 ; (fix 𝜄. id → ((id →(unfold𝜇𝛼 . Int→Int→𝛼 ; 𝜄; fold𝜇𝛼 . Int→𝛼 )); fold𝜇𝛼 . Int→𝛼 )); fold𝜇𝛼 . Int→𝛼

We show the derivation of this type casting relation in Figure 5. Essentially the coinductive “cyclic
reasoning” of Int → Int → 𝐴  Int → 𝐵 in the derivation is captured by the fixpoint castoperator (fix 𝜄. id → 𝑐 1 ), as rule Cast-fix shows. Note that due to the complexity of equi-recursive
equalities, the cast operator can sometimes be quite lengthy, as in this example. But as we will
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:12

Litao Zhou, Qianyong Wan, and Bruno C. d. S. OliveiraΓ ⊢𝑒 :A(Typing)
Typ-int

Typ-var⊢Γ⊢ΓΓ ⊢ 𝑛 : Int

Typ-absx :𝐴 ∈ ΓΓ, x : 𝐴1 ⊢ 𝑒 : 𝐴2

Γ⊢x :𝐴Γ ⊢ 𝜆x : 𝐴1 . 𝑒 : 𝐴1 → 𝐴2
Typ-cast

Typ-appΓ ⊢ 𝑒 1 : 𝐴1 → 𝐴2

Γ ⊢𝑒 :𝐴Γ ⊢ 𝑒 2 : 𝐴1

Γ ⊢ 𝑒 1 𝑒 2 : 𝐴2·; · ⊢ 𝐴 ↩→ 𝐵 : 𝑐Γ ⊢ cast [𝑐] 𝑒 : 𝐵

Δ; E ⊢ A ↩→ B : 𝑐(Type Casting)
Cast-arrow

Cast-idΔ⊢𝐴

Δ; E ⊢ 𝐴1 ↩→ 𝐴2 : 𝑐 1⊢E

Δ; E ⊢ 𝐴 ↩→ 𝐴 : id

Δ; E ⊢ 𝐵 1 ↩→ 𝐵 2 : 𝑐 2

Δ; E ⊢ 𝐴1 → 𝐵 1 ↩→ 𝐴2 → 𝐵 2 : 𝑐 1 → 𝑐 2

Cast-unfold

Cast-foldΔ ⊢ 𝜇𝛼 . 𝐴

Δ ⊢ 𝜇𝛼 . 𝐴⊢EΔ; E ⊢ 𝜇𝛼 . 𝐴 ↩→ 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴] : unfold𝜇𝛼 . 𝐴
Cast-seq⊢E

Δ; E ⊢ 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴] ↩→ 𝜇𝛼 . 𝐴 : fold𝜇𝛼 . 𝐴
Cast-var

Δ; E ⊢ 𝐴 ↩→ 𝐵 : 𝑐 1

Δ; E ⊢ 𝐵 ↩→ 𝐶 : 𝑐 2

Δ⊢𝐴

Δ⊢𝐵

⊢E

𝜄 : 𝐴 ↩→ 𝐵 ∈ E

Δ; E ⊢ 𝐴 ↩→ 𝐶 : 𝑐 1 ; 𝑐 2

Δ; E ⊢ 𝐴 ↩→ 𝐵 : 𝜄Δ; E, 𝜄 : 𝐴1 → 𝐵 1 ↩→ 𝐴2 → 𝐵 2 ⊢ 𝐴1 ↩→ 𝐴2 : 𝑐 1

Δ; E, 𝜄 : 𝐴1 → 𝐵 1 ↩→ 𝐴2 → 𝐵 2 ⊢ 𝐵 1 ↩→ 𝐵 2 : 𝑐 2

Cast-fix

Δ; E ⊢ 𝐴1 → 𝐵 1 ↩→ 𝐴2 → 𝐵 2 : fix 𝜄. (𝑐 1 → 𝑐 2 )𝜇Fig. 4. Typing and type cast rules for 𝜆𝐹𝑖 .

show, this is not a runtime burden because the cast operators can be erased during runtime without
affecting the behavior of the program.
Our type casting rules, ignoring the cast variables and operators, are very similar to the typeequality 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 withrespect to their type equality rules.
Theorem 3.1 (Soundness and completeness of type casting). For any types 𝐴 and 𝐵, · ⊢ 𝐴  𝐵 if andonly if there exists a cast operator 𝑐 such that ·; · ⊢ 𝐴 ↩→ 𝐵 : 𝑐.
Equivalence to a calculus with equi-recursive typing. The only difference between the equi𝜇recursive typing rules and 𝜆𝐹𝑖 ’s typing rules is replacing type casting in rule Typ-cast witha type equality relation. Figure 6 shows an alternative definition of the equi-recursive typing𝜇rules. The gray parts are used to generate a term in 𝜆𝐹𝑖 , and can be ignored for understanding theequi-recursive typing rules. The standard equi-recursive type equality relation in rule Typ-eq isreplaced by the type casting relation in rule ETyp-eq. Since the two relations are equivalent by
Theorem 3.1, the typing rules in Figure 6 are equivalent to the standard equi-recursive typing rules.

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:13

𝜄 : 𝐶 ↩→ 𝐷 ∈ E
Cast-var
Cast-unfold, Cast-seq
E ⊢ 𝐶 ↩→ 𝐷 : 𝜄
Cast-idand Cast-fold
E ⊢ 𝐴 ↩→ 𝐵 : unfold𝐴 ; 𝜄; fold𝐵
E ⊢ Int ↩→ Int : id
Cast-arrow
E ⊢ Int → 𝐴 ↩→ Int → 𝐵 : id → unfold𝐴 ; 𝜄; fold𝐵
Cast-seq, Cast-fold
E ⊢ Int → 𝐴 ↩→ 𝐵 : (id → unfold𝐴 ; 𝜄; fold𝐵 ); fold𝐵...
Cast-idE ⊢ Int ↩→ Int : id
E ⊢ Int → 𝐴 ↩→ 𝐵 : 𝑐 1
Cast-arrow
E ⊢ Int → Int → 𝐴 ↩→ Int → 𝐵 : id → 𝑐 1
Cast-fix· ⊢ Int → Int → 𝐴 ↩→ Int → 𝐵 : fix 𝜄. id → 𝑐 1
Cast-unfold, Cast-seq· ⊢ 𝐴 ↩→ 𝐵 : 𝑐and Cast-fold
𝐴 = 𝜇𝛼 . Int → Int → 𝛼
𝐶 = Int → Int → 𝐴
𝑐 = unfold𝐴 ; (fix 𝜄. id → 𝑐 1 ); fold𝐵
E = 𝜄 : 𝐶 ↩→ 𝐷

𝐵 = 𝜇𝛼 . Int → 𝛼
𝐷 = Int → 𝐵
𝑐 1 = (id → unfold𝐴 ; 𝜄; fold𝐵 ); fold𝐵

Fig. 5. A derivation of type casting with fixpoint casts (well-formedness conditions omitted).

Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′(Equi-recursive typing and full iso-recursive elaboration)
ETyp-abs

ETyp-int

ETyp-var⊢Γ⊢ΓΓ ⊢𝑒 𝑛 : Int ▷ 𝑛

x :𝐴 ∈ ΓΓ ⊢𝑒 x : 𝐴 ▷ xETyp-appΓ, x : 𝐴1 ⊢𝑒 𝑒 : 𝐴2 ▷ 𝑒 ′Γ ⊢𝑒 𝜆x : 𝐴1 . 𝑒 : 𝐴1 → 𝐴2 ▷ 𝜆x : 𝐴1 . 𝑒 ′ETyp-eqΓ ⊢𝑒 𝑒 1 : 𝐴1 → 𝐴2 ▷ 𝑒 1′Γ ⊢𝑒 𝑒 2 : 𝐴1 ▷ 𝑒 2′Γ ⊢𝑒 𝑒 1 𝑒 2 : 𝐴2 ▷ 𝑒 1′ 𝑒 2′Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′·; · ⊢ 𝐴 ↩→ 𝐵 : 𝑐Γ ⊢𝑒 𝑒 : 𝐵 ▷ cast [𝑐] 𝑒 ′𝜇Fig. 6. An equivalent equi-recursive typing system and elaboration rules to 𝜆𝐹𝑖 .

Theorem 3.2 (Equivalence of alternative equi-recursive typing). For any expression 𝑒 and type 𝐴,Γ ⊢𝑒 𝑒 : 𝐴 in the standard equi-recursive typing with rule Typ-eq if and only if there exists a full
iso-recursive term 𝑒 ′ such that Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ using the rules in Figure 6.
Our alternative formulation of equi-recursive typing also provides a way to elaborate equirecursive terms into full iso-recursive terms, as shown by the gray colored parts in Figure 6. 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 acast 𝑐, which can be viewed as evidence of the type transformation from type 𝐴 into type 𝐵. Then,𝜇we use 𝑐 in an explicit cast in the elaborated 𝜆𝐹𝑖 term, which will trigger the type transformation in𝜇𝜆𝐹𝑖 . 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:

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:14

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira𝑒 ↩→ 𝑒 ′(Reduction)
Red-appl

Red-cast

Red-appr𝑒 1 ↩→ 𝑒 1′

𝑒 2 ↩→ 𝑒 2′𝑒 ↩→ 𝑒 ′(𝜆x : 𝐴. 𝑒) 𝑣 ′ ↩→ 𝑒 [x ↦→ 𝑣 ′ ]𝑒 1 𝑒 2 ↩→ 𝑒 1′ 𝑒 2𝑣 1 𝑒 2 ↩→ 𝑣 1 𝑒 2′

cast [𝑐] 𝑒 ↩→ cast [𝑐] 𝑒 ′Red-cast-id

Red-cast-arr

cast [id] 𝑣 ↩→ 𝑣

(cast [𝑐 1 → 𝑐 2 ] 𝑣 1 ) 𝑣 2 ↩→ cast [𝑐 2 ] (𝑣 1 (cast [¬𝑐 1 ] 𝑣 2 ))Red-beta

Red-cast-seq

Red-castelim

cast [𝑐 1 ; 𝑐 2 ] 𝑣 ↩→ cast [𝑐 2 ] (cast [𝑐 1 ] 𝑣)

cast [unfold𝐴 ] (cast [fold𝐵 ] 𝑣) ↩→ 𝑣

Red-cast-fix

cast [fix 𝜄. 𝑐] 𝑣 ↩→ cast [𝑐 [𝜄 ↦→ fix 𝜄. 𝑐]] 𝑣
Fig. 7. Reduction rules.

Theorem 3.3 (Equi-recursive to full iso-recursive typing). For any expressions 𝑒, 𝑒 ′ and type 𝐴, ifΓ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ then Γ ⊢ 𝑒 ′ : 𝐴.
Theorem 3.4 (Full iso-recursive to equi-recursive typing). For any expressions 𝑒 and type 𝐴, ifΓ ⊢ 𝑒 : 𝐴 then Γ ⊢𝑒 |𝑒 | : 𝐴 ▷ 𝑒.
In the theorem above, the full iso-recursive expressions can be erased to the equi-recursive expressions by removing the casts. The erasure operation |𝑒 | is defined as follows:|n||𝑒 1 𝑒 2 ||cast [𝑐] 𝑒 |=n= |𝑒 1 | |𝑒 2 |= |𝑒 ||𝑥 ||𝜆𝑥 : 𝐴. 𝑒 |=𝑥= 𝜆𝑥 : 𝐴. |𝑒 |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 theunfold/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 𝑒, 𝑒 ′ and type 𝐴, if Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ ,then |𝑒 ′ | = 𝑒.
3.3

Semantics𝜇Figure 7 shows the reduction rules for 𝜆𝐹𝑖 . 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 arevalues, 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
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:15by analyzing the structure of 𝑐 as follows:¬𝜄¬ fold𝐴¬ (𝑐 1 → 𝑐 2 )¬ (fix 𝜄. 𝑐)=𝜄= unfold𝐴= (¬ 𝑐 1 ) → (¬ 𝑐 2 )= fix 𝜄. ¬ 𝑐¬ id¬ unfold𝐴¬ (𝑐 1 ; 𝑐 2 )= id= fold𝐴= (¬ 𝑐 2 ); (¬ 𝑐 1 )We will see why this reverse operation is necessary in §4.1. 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-castelim). Thus,
rule Red-castelim 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). The addition of the push rules for the cast operators is necessary for the type𝜇𝜇soundness of 𝜆𝐹𝑖 , since the cast rules are necessary to preserve types. 𝜆𝐹𝑖 is type sound, proved
with the usual preservation and progress theorems:
Theorem 3.6 (Progress). For any expression 𝑒 and type 𝐴, if · ⊢ 𝑒 : 𝐴 then either 𝑒 is a value or there
exists an expression 𝑒 ′ such that 𝑒 ↩→ 𝑒 ′ .
Theorem 3.7 (Preservation). For any expression 𝑒 and type 𝐴, if · ⊢ 𝑒 : 𝐴 and 𝑒 ↩→ 𝑒 ′ then · ⊢ 𝑒 ′ : 𝐴.
𝜇

A running example. To illustrate how the reduction rules work in the 𝜆𝐹𝑖 calculus, we present a
relatively complex example that involves fixpoint casts. Assume that we have a term 𝑒 with thetype 𝜇𝛼 . Int → Int → 𝛼, which repeatedly takes two integers at a time and returns itself. With𝜇term-level recursion constructors (which can be easily added to 𝜆𝐹𝑖 or encoded by fold/unfold
casts [Abadi and Fiore 1996]), denoted as rec (𝑥 : 𝐴). 𝑒, such a term can be defined as follows:𝑒 = rec (self : 𝜇𝛼 . Int → Int → 𝛼). cast [fold𝜇𝛼 . Int→Int→𝛼 ] (𝜆(𝑥 : Int). 𝜆(𝑦 : Int). self )Now we would like to apply this term to a single integer argument. Using the cast operator 𝑐 that
we have defined in Figure 5, we can write (cast [unfold𝜇𝛼 . Int→𝛼 ] (cast [𝑐] 𝑒)) 1. This expression
first turns this term into a type 𝜇𝛼 . Int → 𝛼, and then applies the term after iso-recursive unfolding
to an integer 1. In Figure 8 we try to evaluate this term. The reduction rules are applied step bystep. The push rules Red-cast-seq and Red-cast-arr reduce the cast operator into more atomic
forms, and the unfold/fold cast pairs are eventually eliminated by rule Red-castelim in various
steps. Notably, the rule Red-cast-fix for fixpoint casts may introduce a larger cast operator after
substitution during runtime. However, when combined with other push rules, the resulting term
can be safely reduced. In our case, the term reduces to a value, since the result is a fold of arrowcasts and belongs to the value syntax.
Equivalence to the equi-recursive dynamic semantics. As explained in §2.5, the reduction rules forthe 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 𝑒, if
𝑒 ↩→∗ 𝑣 then |𝑒 | ↩→𝑒∗ |𝑣 |.
Here ↩→𝑒 is the reduction relation in the equi-recursive setting, which is basically defined by asubset of the reduction rules in Figure 7 (rules Red-beta, Red-appl, and Red-appr). We use ↩→∗to denote the reflexive, transitive closure of the reduction relation. Theorem 3.8 can be further
illustrated by the example in Figure 8. It can be seen that most of the steps related to the castoperators are simply for the sake of typing correctness, and all the cast operators in the reductions
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:16

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

↩→
↩→
↩→
↩→
↩→
↩→
↩→
↩→
↩→
↩→
↩→
↩→

(cast [unfold𝐵 ] (cast [𝑐] 𝑒)) 1(cast [unfold𝐵 ] (cast [𝑐] (cast [fold𝐴 ] (𝜆(𝑥 𝑦 : Int). 𝑒)))) 1(cast [unfold𝐵 ] (cast [unfold𝐴 ; fix 𝜄. id → 𝑐 1 ; fold𝐵 ](cast [fold𝐴 ] (𝜆(𝑥 𝑦 : Int). 𝑒)))) 1(cast [unfold𝐵 ] (cast [(fix 𝜄. id → 𝑐 1 ); fold𝐵 ](cast [unfold𝐴 ] (cast [fold𝐴 ] (𝜆(𝑥 𝑦 : Int). 𝑒))))) 1(cast [unfold𝐵 ] (cast [(fix 𝜄. id → 𝑐 1 ) ; fold𝐵 ] (𝜆(𝑥 𝑦 : Int). 𝑒))) 1(cast [unfold𝐵 ] (cast [fold𝐵 ](cast [fix 𝜄. id → 𝑐 1 ] (𝜆(𝑥 𝑦 : Int). 𝑒)))) 1(cast [fix 𝜄. id → 𝑐 1 ] (𝜆(𝑥 𝑦 : Int). 𝑒)) 1(cast [id → 𝑐 1 [𝜄 ↦→ 𝑐]] (𝜆(𝑥 𝑦 : Int). 𝑒)) 1(cast [id → ((id → unfold𝐴 ; 𝑐; fold𝐵 ); fold𝐵 )] (𝜆(𝑥 𝑦 : Int). 𝑒)) 1(cast [(id → unfold𝐴 ; 𝑐; fold𝐵 ); fold𝐵 ]((𝜆(𝑥 𝑦 : Int). 𝑒) (cast [¬ id] 1)))
(cast [(id → unfold𝐴 ; 𝑐; fold𝐵 ); fold𝐵 ](𝜆(𝑥 𝑦 : Int). 𝑒 1)
cast [(id → unfold𝐴 ; 𝑐; fold𝐵 ); fold𝐵 ] (𝜆(𝑦 : Int). 𝑒)
cast [fold𝐵 ] (cast [id → unfold𝐴 ; 𝑐; fold𝐵 ] (𝜆(𝑦 : Int). 𝑒))(unrolling rec)(definition of 𝑐)(Red-cast-seq)(Red-castelim)(Red-cast-seq)(Red-castelim)(Red-cast-fix)(substitution)(Red-cast-arr)(Red-cast-id)(Red-beta)(Red-cast-seq)𝜇Fig. 8. Small step execution trace of a 𝜆𝐹𝑖 program (assuming same abbreviations as in Figure 5).

can be erased without affecting the behavior of the program. If we erase the cast operators duringruntime, the trace in Figure 8 simply boils down to𝑒 1 ↩→ (𝜆(𝑥 𝑦 : Int). 𝑒) 1 ↩→ 𝜆(𝑦 : Int). 𝑒
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 6. 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 𝑒, 𝑒 ′ and type 𝐴, if · ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ , then(1) 𝑒 ↩→𝑒∗ 𝑣 if and only if there exists 𝑣 ′ such that 𝑒 ′ ↩→∗ 𝑣 ′ and |𝑣 ′ | = 𝑣.
(2) 𝑒 diverges if and only if 𝑒 ′ diverges.
4

Metatheory of Full Iso-recursive Types𝜇

In this section we discuss the key proof techniques and results in the metatheory of 𝜆𝐹𝑖 . The𝜇metatheory covers three components: type soundness of 𝜆𝐹𝑖 (Theorem 3.6 and 3.7), the typing
𝜇equivalence between 𝜆𝐹𝑖 and equi-recursive types (Theorem 3.2, 3.3 and 3.4), and the behavioral
𝜇equivalence between 𝜆𝐹𝑖 and equi-recursive types (Theorem 3.9).
4.1

Type Soundness𝜇Progress. For 𝜆𝐹𝑖 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 iseither a value or can be further reduced. The definition of value has been discussed in §3.1. There𝜇
are two canonical forms for a value with function types (𝐴1 → 𝐴2 ) in 𝜆𝐹𝑖 : lambda abstractions(𝜆𝑥 : 𝐴. 𝑒) and arrow casts (cast [𝑐 1 → 𝑐 2 ] 𝑣). Therefore in the progress proof for function
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types𝑣 1 : 𝐵1

¬𝑐 1

𝐵2

𝑐1

𝑐2

278:17𝐵 1 ↩→ 𝐴1 : 𝑐 1 𝐵 2 ↩→ 𝐴2 : 𝑐 2
Cast-arrow
𝐵 1 → 𝐵 2 ↩→ 𝐴1 → 𝐴2 : 𝑐 1 → 𝑐 2
Typ-cast
cast [𝑐 1 → 𝑐 2 ] 𝑣 1 : 𝐴1 → 𝐴2
𝑣 2 : 𝐴1
Typ-app(cast [𝑐 1 → 𝑐 2 ] 𝑣 1 ) 𝑣 2 : 𝐴2
𝑣 1 : 𝐵1 → 𝐵2

𝐵 1 ↩→ 𝐴1 : 𝑐 1
Lemma 4.1
𝐴1 ↩→ 𝐵 1 : ¬𝑐 1
Typ-cast
cast [¬𝑐 1 ] 𝑣 2 : 𝐵 1
𝑣 1 : 𝐵1 → 𝐵2
Typ-app𝑣 1 (cast [¬𝑐 1 ] 𝑣 2 ) : 𝐵 2
𝐵 2 ↩→ 𝐴2 : 𝑐 2
Typ-cast
cast [𝑐 2 ] (𝑣 1 (cast [¬𝑐 1 ] 𝑣 2 )) : 𝐴2𝑣 2 : 𝐴1𝑣 2 : 𝐴1

𝐴2

Fig. 9. Typing derivation for the function push rule (empty environments omitted).

applications (𝑒 1 𝑒 2 ), we need to consider one extra case when 𝑒 1 is an arrow cast. We push the castoperator 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· ⊢ 𝑒 : 𝐴 and then induction on the reduction relation 𝑒 ↩→ 𝑒 ′ . The interesting cases are when the
reduction rule is a push rule. Most cases of the push rules are straightforward, by inversion on thetype 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, we illustrate the typing derivation for the two terms in the reduction
rule in Figure 9. We show the type casting relation (using the ↩→ arrow) between the types of
the two principal terms 𝑣 1 and 𝑣 2 in the left part of the figure, and the detailed typing derivation
steps for the terms before and after the reduction are shown in the right part. By inversion on
the typing derivation of · ⊢ (cast [𝑐 1 → 𝑐 2 ] 𝑣 1 ) 𝑣 2 : 𝐴2 we know that 𝑣 1 has a function type𝐵 1 → 𝐵 2 , 𝑣 2 has type 𝐴1 , and 𝐵 1 → 𝐵 2 can be cast to 𝐴1 → 𝐴2 by 𝑐 1 → 𝑐 2 , which in turn implies
that 𝐵 1 ↩→ 𝐴1 : 𝑐 1 and 𝐵 2 ↩→ 𝐴2 : 𝑐 2 . In order to show that the type of the reduced expression(cast [𝑐 2 ] (𝑣 1 (cast [¬𝑐 1 ] 𝑣 2 ))) is still 𝐴2 , we need to prove 𝐴1 ↩→ 𝐵 1 : ¬𝑐 1 . This goal can be achievedby Lemma 4.1 below, which is proved by induction on the type casting relation. The analysis ofrule Red-cast-arr also shows that it is necessary to insert the reverse operation on the cast𝜇operator 𝑐 1 to ensure the preservation of 𝜆𝐹𝑖 .
Lemma 4.1 (Reverse of casting). For any types 𝐴 and 𝐵, and casting operators 𝑐, if ·; E ⊢ 𝐴 ↩→ 𝐵 : 𝑐then ·; ¬ E ⊢ 𝐵 ↩→ 𝐴 : ¬ 𝑐, where ¬ E reverses the direction of casting in E (i.e. 𝜄 : 𝐶 ↩→ 𝐷 in E
becomes 𝜄 : 𝐷 ↩→ 𝐶 after reversing).
As for the Red-cast-fix case, the reduction rule unfolds the fixpoint cast (fix 𝜄. 𝑐) to (𝑐 [𝜄 ↦→(fix 𝜄. 𝑐)]). By inversion on the type casting relation ·; · ⊢ 𝐴 ↩→ 𝐵 : fix 𝜄. 𝑐, we know that·; 𝜄 : 𝐴 ↩→ 𝐵 ⊢ 𝐴 ↩→ 𝐵 : 𝑐(2)

Essentially the cast operator (fix 𝜄. 𝑐) and its unrolling (𝑐 [𝜄 ↦→ (fix 𝜄. 𝑐)]) should represent the same
proof. The type casting judgement (2) can be interpreted as: if we know that there is a cast variable𝜄 that can cast 𝐴 to 𝐵, then we can cast 𝐴 to 𝐵 by 𝑐, using the cast variable 𝜄. Since we already knowthat fix 𝜄. 𝑐 can do the same job as 𝜄 in casting 𝐴 to 𝐵, it should be safe to replace 𝜄 with fix 𝜄. 𝑐 in the
cast operator 𝑐, and show that ·; · ⊢ 𝐴 ↩→ 𝐵 : 𝑐 [𝜄 ↦→ (fix 𝜄. 𝑐)]. This idea can be formalized by thefollowing cast substitution lemma, which is proved by induction on the type casting relation of 𝑐 1 .

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:18

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

Lemma 4.2 (Cast substitution). For any contexts Γ, E, types 𝐴, 𝐵, 𝐶, 𝐷, cast operators 𝑐 1 , 𝑐 2 and castvariable 𝜄, if Γ; E ⊢ 𝐴 ↩→ 𝐵 : 𝑐 1 , and Γ; E, 𝜄 : 𝐴 ↩→ 𝐵 ⊢ 𝐶 ↩→ 𝐷 : 𝑐 2 then Γ; E ⊢ 𝐶 ↩→ 𝐷 : 𝑐 2 [𝜄 ↦→ 𝑐 1 ].
4.2

Typing Equivalence

As discussed in §3.2, the key to the typing equivalence between full iso-recursive types and equirecursive types is to show our type casting rules are equivalent to Brandt and Henglein’s typeequality 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 totheir type equality rules, so the proof for these cases is straightforward. For instance, the treatmentof coinductive reasoning by introducing new premises for function types in our rule Cast-fix isexactly 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 castusing rule Cast-fix as Brandt and Henglein did in rule Tye-arrfix, we also allow function types tobe 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 𝜆𝐹𝑖 . By rule Cast-fix, all
the fixpoint casts in well-typed expressions are in the form of fix 𝜄. 𝑐 1 → 𝑐 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𝑐 1′ → 𝑐 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 andprove 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 asymmetry rule for type casting. The main reason for this design choice is that we would like to havea simple treatment of reversing cast variables (i.e. ¬ 𝜄 = 𝜄 without considering contexts E) while
avoiding the overhead of reversing the whole environment (¬ E) frequently in the typing derivation.
In our current design, the reverse operation is only needed for cast operators in the reduction
rule Red-cast-arr and absent in the type casting rules. Since the casts are erasable, this reverse
operation will cause no runtime overhead. Alternative design choices, such as adding a symmetry
operator in the type casting rules, or turning the function casting rule into a contravariant one,would all require reversing the whole environment for the sake of soundness.
Δ; E ⊢ 𝐴 ↩→ 𝐵 : 𝑐
AltCast-symm
Δ; ¬ E ⊢ 𝐵 ↩→ 𝐴 : sym 𝑐

Δ; ¬ E ⊢ 𝐴2 ↩→ 𝐴1 : 𝑐 1
AltCast-arrow
Δ; E ⊢ 𝐴1 ↩→ 𝐴2 : 𝑐 1

Although by setting E in Lemma 4.1 to be empty, we can show that symmetry is admissible inour type casting relation, when the initial environment is empty, there is still a missing step toprove the equivalence between our type casting rules and Brandt and Henglein’s type equality
rules. Note that changing the type casting context from ¬ E in Lemma 4.1 to E as rule Tye-symm
specifies will not work. In other words, rule Tye-symm, in its general form, with the same list ofassumptions 𝐻 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 𝐻 , which are not derivable by the type
casting rules. For example, Int  Int → Int ⊢ Int → Int  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 a symmetric 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
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:19

∗
𝑣
𝑒

𝑒

𝑒1

𝑒2

𝑣

𝑒

up to erasure

𝑒′

∗

𝑣′

(a) The “only if” direction.

+ ′
𝑒2

𝑒 1′
(b) Lemma 4.3.

∗

𝑒′

𝑣′

(c) Lemma 4.4.

Fig. 10. Illustration of the proof idea for behavioral equivalence.

introduced to the environment are guaranteed to be derivable from an empty assumption list by thetype 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 𝜆𝐹𝑖 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 thepreservation of divergence behavior can then be proved by contradiction. The “if” direction of thetheorem (from full-iso recursive reduction to equi-recursive reduction) is easy, directly from thebehavioral 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 illustrate
the proof idea in Figure 10.
Basically we would like to show that if an equi-recursive term 𝑒 can be reduced to 𝑣, then its
corresponding full iso-recursive term 𝑒 ′ can also be reduced to a value 𝑣 ′ , as illustrated in Figure 10a.
To prove this, we first show that every step of equi-recursive reduction can be simulated by several
steps of full iso-recursive reduction (Lemma 4.3), as shown in Figure 10b. Moreover, the encodingof an equi-recursive value might not be a value in the full iso-recursive setting, since the encoding
result may contain casts that are not values. Therefore we also need to show that the encoding ofan equi-recursive value can be further reduced to a value in the full iso-recursive setting, and stillpreserves the elaboration relation (Lemma 4.4), as shown in Figure 10c. By induction on the lengthof the equi-recursive reduction steps in Figure 10a, we complete the proof for Theorem 3.9.
Lemma 4.3 (Simulation of equi-recursive reduction). For any expressions 𝑒 1 , 𝑒 1′ , 𝑒 2 and type 𝐴, if· ⊢𝑒 𝑒 1 : 𝐴 ▷ 𝑒 1′ and 𝑒 1 ↩→𝑒 𝑒 2 , then there exists 𝑒 2′ such that 𝑒 1′ ↩→+ 𝑒 2′ and · ⊢𝑒 𝑒 2 : 𝐴 ▷ 𝑒 2′ .
Lemma 4.4 (Reductions of full iso-recursive terms from equi-recursive values). For any expression𝑒 and type 𝐴, if · ⊢𝑒 𝑣 : 𝐴 ▷ 𝑒 ′ , then there exists 𝑣 ′ such that 𝑒 ′ ↩→∗ 𝑣 ′ and · ⊢𝑒 𝑣 : 𝐴 ▷ 𝑣 ′ .
During the proof we find the congruence lemmas for full iso-recursive reductions and thesubstitution lemma for the elaboration relation useful, as shown below.
Lemma 4.5 (Congruence lemma of full iso-recursive reduction).
(1) If 𝑒 1 ↩→∗ 𝑒 1′ , then 𝑒 1 𝑒 2 ↩→∗ 𝑒 1′ 𝑒 2 .
(2) If 𝑒 2 ↩→∗ 𝑒 2′ , then 𝑣 1 𝑒 2 ↩→∗ 𝑣 1 𝑒 2′ .
(3) If 𝑒 ↩→∗ 𝑒 ′ , then cast [𝑐] 𝑒 ↩→∗ cast [𝑐] 𝑒 ′ .
and the propositions above also hold for the transitive closure ↩→+ .
Lemma 4.6 (Substitution lemma for elaboration). For any typing context Γ, expressions 𝑒 1 , 𝑒 1′ , 𝑒 2 , 𝑒 2′
and types 𝐴, 𝐵, if Γ, 𝑥 : 𝐴 ⊢𝑒 𝑒 1 : 𝐵 ▷ 𝑒 1′ and Γ ⊢𝑒 𝑒 2 : 𝐴 ▷ 𝑒 2′ , then Γ ⊢𝑒 𝑒 1 [𝑥 ↦→ 𝑒 2 ] : 𝐵 ▷ 𝑒 1′ [𝑥 ↦→ 𝑒 2′ ].
The proof of Lemma 4.4 is straightforward by induction on the typing derivation · ⊢𝑒 𝑣 : 𝐴 ▷ 𝑒 ′and using the congruence lemmas. In the rest of this section we focus on the proof of Lemma 4.3.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:20

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

proof of Lemma 4.3. The proof of Lemma 4.3 is done by first induction on the equi-recursive
reduction relation 𝑒 1 ↩→𝑒 𝑒 2 , and then induction on the elaboration relation · ⊢𝑒 𝑒 1 : 𝐴 ▷ 𝑒 1′ . Mostof the cases are straightforward, by applying the induction hypothesis and using the congruencelemmas to construct the reduction steps.
The tricky case is when 𝑒 1 ↩→𝑒 𝑒 2 is a beta reduction (case Red-beta). By inversion on the
reduction relation, we know that 𝑒 1 is a function application (𝑒 1 = (𝜆𝑥 : 𝐴1 .𝑒 0 ) 𝑣 1 ) and 𝑒 2 is(𝑒 0 [𝑥 ↦→ 𝑣 1 ]). By induction on the elaboration relation · ⊢𝑒 𝑒 1 : 𝐴 ▷ 𝑒 1′ , case ETyp-eq can be proved
using the induction hypothesis. We consider case ETyp-app, where· ⊢ 𝜆𝑥 : 𝐴1 .𝑒 0 : 𝐴1 → 𝐴 ▷ 𝑒 3′and· ⊢ 𝑣 1 : 𝐴1 ▷ 𝑒 4′(3)

However, we do not know the exact form of 𝑒 3′ and 𝑒 4′ , 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, Lemma 4.4 is used to show that regardless of the form of 𝑒 3′ and𝑒 4′ , they can always be further reduced to values. By applying Lemma 4.4 to the two terms in thetricky case (3) above, we also know that the value of evaluating 𝑒 3′ preserves the function type,so it must be one of the two canonical forms: a lambda abstraction (𝜆𝑥 : 𝐴1 .𝑒 0′ ) or an arrow cast
(cast [𝑐 1 → 𝑐 2 ] 𝑣 1′ ), and then we can construct the reduction steps for (𝑒 3′ 𝑒 4′ ) as shown below:
↩→∗
↩→∗
↩→

𝑒 3′ 𝑒 4′(𝜆𝑥 : 𝐴1 .𝑒 0′ ) 𝑒 4′
(𝜆𝑥 : 𝐴1 .𝑒 0′ ) 𝑣 2′
𝑒 0′ [𝑥 ↦→ 𝑣 2′ ]

or
or
or

(cast [𝑐 1 → 𝑐 2 ] 𝑣 1′ ) 𝑒 4′
(cast [𝑐 1 → 𝑐 2 ] 𝑣 1′ ) 𝑣 2′
(cast [𝑐 2 ] (𝑣 1′ (cast [¬𝑐 1 ] 𝑣 2′ )))(Lemma 4.4 and 4.5(1))(Lemma 4.4 and 4.5(2))(Rule Red-beta or Red-cast-arr)

Now we are left to prove the second goal of this case, that is, the result of the reduction constructedabove can be derived from the elaboration relation, i.e.
· ⊢𝑒 𝑒 0 [𝑥 ↦→ 𝑣 1 ] : 𝐴 ▷ 𝑒 0′ [𝑥 ↦→ 𝑣 2′ ]or· ⊢𝑒 𝑒 0 [𝑥 ↦→ 𝑣 1 ] : 𝐴 ▷ (cast [𝑐 2 ] (𝑣 1′ (cast [¬𝑐 1 ] 𝑣 2′ )))The latter case for rule Red-cast-arr follows from the induction hypothesis. The first case forrule Red-beta can be proved by the substitution lemma for the elaboration relation (Lemma 4.6).
□
With Lemma 4.5, 4.4 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 andFiore’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 𝜆𝐹𝑖 is completely
mechanized in Coq. The proof does not rely on any user-defined conjectures or axioms except
functional_extensionality_dep and proof_irrelevance introduced by the Coq standard library, andeq_rect_eq and JMeq_eq as their corollaries, or those introduced by Metalib that we used to formalize
variables and binders with the locally nameless representation [Aydemir et al. 2008].
5

Recursive Subtyping

In this section we show that our results in the previous sections can be extended to a calculus with𝜇<:subtyping called 𝜆𝐹𝑖 .
5.1

A Calculus with Subtyping

Adapting the results in §3 to a calculus with subtyping requires only a few changes. In terms oftypes, we add a top type (⊤). Expressions and values remain the same.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:21

Σ ⊢ 𝐴 ≤⊕ 𝐵

(Equi-recursive/Iso-recursive Subtyping)Sub-eqSub-top

Sub-intΣ ⊢ 𝐴 ≤⊕ ⊤

Σ ⊢ Int ≤𝑖 Int

Sub-trans

Sub-var

𝐴𝐵

𝛼≤𝛽∈Σ

Sub-selfΣ ⊢ 𝐴 ≤𝑒 𝐵

Σ ⊢ 𝛼 ≤⊕ 𝛽Σ ⊢ 𝜇𝛼 . 𝐴 ≤𝑖 𝜇𝛼 . 𝐴

Sub-arrowΣ ⊢ 𝐴 ≤𝑒 𝐵

Σ ⊢ 𝐵 ≤𝑒 𝐶

Σ ⊢ 𝐴 ≤𝑒 𝐶

Σ ⊢ 𝐵 1 ≤ ⊕ 𝐴1

Sub-recΣ ⊢ 𝐴2 ≤ ⊕ 𝐵 2

Σ ⊢ 𝐴1 → 𝐴2 ≤ ⊕ 𝐵 1 → 𝐵 2

Σ, 𝛼 ≤ 𝛽 ⊢ 𝐴 ≤⊕ 𝐵
Σ ⊢ 𝜇𝛼 . 𝐴 ≤⊕ 𝜇𝛽. 𝐵

Fig. 11. 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 11. The subtyping rules
use a special environment Σ, which tracks a set of pairs of type variables that are assumed in thesubtyping relation, as explained in §2.4. We use ≤⊕ parameterized by a metavariable ⊕ ∈ {𝑖, 𝑒}
to denote the subtyping rules for both relations: 𝑖 denotes iso-recursive subtyping, and 𝑒 denotes
equi-recursive subtyping. We use ≤𝑒 to denote the subtyping rules (rules Sub-eq and Sub-trans)
that only apply to equi-recursive types, and ≤𝑖 to denote the subtyping rules (rules Sub-int andSub-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 andSub-self and removes transitivity rule Sub-trans from the original Amber rules. The different
treatment of reflexivity between the two formulations are denoted by dedicated rules Sub-int andSub-self for iso-recursive subtyping and rule Sub-eq for equi-recursive subtyping in Figure 11.
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. For
the iso-recursive subtyping relation we strictly follow their formulation to maximally reuse theirmechanized proof in our work.
Lemma 5.1 (Reflexivity of iso-recursive subtyping). If 𝐴 is a closed type, then Σ ⊢ 𝐴 ≤𝑖 𝐴.
Lemma 5.2 (Transitivity of iso-recursive subtyping). If · ⊢ 𝐴 ≤𝑖 𝐵 and · ⊢ 𝐵 ≤𝑖 𝐶, then · ⊢ 𝐴 ≤𝑖 𝐶.
In Lemma 5.1, the assumption that 𝐴 is a closed type can be implied by the fact that the freevariable sets of 𝐴 and 𝐵 in the subtyping relation Σ ⊢ 𝐴 ≤𝑖 𝐵 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 isorecursive 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. Accordingly, the elaboration rules defined in Figure 6 are also extended
with rule ETyp-isub for iso-recursive subtyping. As we will discuss later, rules ETyp-isub and ETypeq can together be used to encode equi-recursive subtyping. Therefore in the equi-recursive typing
relation (Figure 6 without the gray parts), instead of adding rule ETyp-isub on top of the existing
rules, we replace rule ETyp-eq with the rule ETyp-bare-sub so that the typing relation faithfully
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:22

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveirareflects the conventional equi-recursive type system. There are no changes to the reduction rules.
ETyp-isubTyp-subΓ ⊢𝑒 :𝐴· ⊢ 𝐴 ≤𝑖 𝐵Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′Γ ⊢𝑒 :𝐵
5.2

ETyp-bare-sub· ⊢ 𝐴 ≤𝑖 𝐵Γ ⊢𝑒 𝑒 : 𝐵 ▷ 𝑒

Γ ⊢𝑒 𝑒 : 𝐴· ⊢ 𝐴 ≤𝑒 𝐵Γ ⊢𝑒 𝑒 : 𝐵′

Type Soundness𝜇<:There are no significant technical challenges in extending the type soundness proof to 𝜆𝐹𝑖 . The
only part that requires extra care is the preservation lemma, in which we need to show thatrule Red-castelim preserves the typing in the presence of subtyping. Let us consider an expression
cast [unfold𝜇𝛼 . 𝐴 ] (cast [fold𝜇𝛼 . 𝐵 ] 𝑣). The derivation below shows the typing of this expression.
· ⊢ 𝑣 : 𝐵 [𝛼 ↦→ 𝜇𝛼 . 𝐵]...
Typ-cast· ⊢ cast [fold𝜇𝛼 . 𝐵 ] 𝑣 : 𝜇𝛼 . 𝐵· ⊢ 𝜇𝛼 . 𝐵 ≤𝑖 𝜇𝛼 . 𝐴
Typ-sub· ⊢ cast [fold𝜇𝛼 . 𝐵 ] 𝑣 : 𝜇𝛼 . 𝐴...
Typ-cast· ⊢ cast [unfold𝜇𝛼 . 𝐴 ] (cast [fold𝜇𝛼 . 𝐵 ] 𝑣) : 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴]
By inversion we know that after reduction using rule Red-castelim, the result 𝑣 has the type
𝐵 [𝛼 ↦→ 𝜇𝛼 . 𝐵], and that 𝜇𝛼 . 𝐵 ≤𝑖 𝜇𝛼 . 𝐴. The preservation proof goal for this case can be expressedas the following lemma:
Lemma 5.3 (Unfolding lemma). If · ⊢ 𝜇𝛼 . 𝐵 ≤𝑖 𝜇𝛼 . 𝐴, then · ⊢ 𝐵 [𝛼 ↦→ 𝜇𝛼 . 𝐵] ≤𝑖 𝐴[𝛼 ↦→ 𝜇𝛼 . 𝐴].
The proof of this lemma has been shown by Zhou et al. [2022, Corollary 59]. They proposed analternative 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 𝜆𝐹𝑖 .
𝜇<:

𝜇<:

Theorem 5.4 (Type soundness of 𝜆𝐹𝑖 ). For any term 𝑒 and type 𝐴 in 𝜆𝐹𝑖 ,(1) (Progress) if · ⊢ 𝑒 : 𝐴 then either 𝑒 is a value or there exists a term 𝑒 ′ such that 𝑒 ↩→ 𝑒 ′ .
(2) (Preservation) if · ⊢ 𝑒 : 𝐴 and 𝑒 ↩→ 𝑒 ′ then · ⊢ 𝑒 ′ : 𝐴.
5.3

Typing Equivalence𝜇𝜇<:Similarly to 𝜆𝐹𝑖 with equality, we can prove that 𝜆𝐹𝑖 with iso-recursive subtyping is sound andcomplete with respect to a calculus with equi-recursive subtyping. The key idea is encoding the equirecursive 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). · ⊢ 𝐴 ≤𝑒 𝐵 if and only if there exist types
𝐶 1 and 𝐶 2 such that 𝐴  𝐶 1 , · ⊢ 𝐶 1 ≤𝑖 𝐶 2 , and 𝐶 2  𝐵.
The soundness direction (i.e. the “if” direction) of this lemma is straightforward by rules Sub-eq
and Sub-trans and the fact that ≤𝑖 is a sub-relation of ≤𝑒 . The completeness direction can bederived from Amadio and Cardelli’s proof of completeness with respect to the tree model forthe equi-recursive Amber rules. They proved that for any types 𝐴, 𝐵 that are in the tree modelinterpretation of the equi-recursive subtyping relation, one can find types 𝐶 1 and 𝐶 2 such that𝐴  𝐶 1 , 𝐶 1 ≤𝑒 𝐶 2 , and 𝐶 2  𝐵 hold [Amadio and Cardelli 1993, Lemma 5.4.1, Lemma 5.4.3].
Moreover, the derivation of 𝐶 1 ≤𝑒 𝐶 2 satisfies the one-expansion property, which means that in thederivation each recursive type is unfolded at most once, informally speaking. Although this resultis expressed as an equi-recursive subtyping relation in their conclusion, we can rewrite all theoccurrences of 𝐶 1 ≤𝑒 𝐶 2 with one-expansion property in their proof to an iso-recursive subtyping
relation 𝐶 1 ≤𝑖 𝐶 2 . Every application of rules Sub-eq and Sub-trans in their proofs can either be
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:23

P1
Sub-rec
Tyeq-unfold⊢ ⊤ ≤𝑒 ⊤ ⊢ 𝐴2 ≤𝑒 𝐵
Tyeq-contract
Sub-arrow
𝐴1  ⊤ → 𝐴2
⊢ ⊤ → 𝐴2 ≤𝑒 ⊤ → 𝐵
Sub-eq and Sub-trans⊢ Int ≤𝑒 Int⊢ 𝐴1 ≤𝑒 ⊤ → 𝐵
Tyeq-unfold
Sub-arrow⊢ 𝐴 ≤𝑒 Int → ⊤ → 𝐵⊢ Int → ⊤ → 𝐵  𝐵 Sub-transand Sub-eq⊢ 𝐴 ≤𝑒 𝐵
P2
Sub-rec⊢ ⊤ ≤𝑖 ⊤ ⊢ 𝐴2 ≤𝑖 𝐵
Lemma 5.1
Sub-arrow⊢ ⊤ → 𝐴2 ≤𝑖 ⊤ → 𝐴2 ⊢ ⊤ → 𝐴2 ≤𝑖 ⊤ → 𝐵
Lemma 5.2
⊢ Int ≤𝑖 Int⊢ ⊤ → 𝐴2 ≤𝑖 ⊤ → 𝐵
Lemma 5.1
Sub-arrow⊢ 𝐶 ≤𝑖 𝐷⊢ 𝐷 ≤𝑖 𝐷
Lemma 5.2
⊢ 𝐶 ≤𝑖 𝐷
𝐴 = Int → (𝜇𝛼 . ⊤ → 𝛼)
𝐵 = 𝜇𝛼 . Int → ⊤ → 𝛼
𝐶 = Int → ⊤ → (𝜇𝛼 . ⊤ → ⊤ → 𝛼) 𝐷 = Int → ⊤ → (𝜇𝛼 . Int → ⊤ → 𝛼)
𝐴1 = 𝜇𝛼 . ⊤ → 𝛼
𝐴2 = 𝜇𝛼 . ⊤ → ⊤ → 𝛼
P1 is the judgement 𝛼 ≤ 𝛽 ⊢ ⊤ → ⊤ → 𝛼 ≤𝑒 Int → ⊤ → 𝛽
P2 is the judgement 𝛼 ≤ 𝛽 ⊢ ⊤ → ⊤ → 𝛼 ≤𝑖 Int → ⊤ → 𝛽
Fig. 12. Illustration of decomposing an equi-recursive subtyping derivation.

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 𝛼-renaming. In other words, Amadio and Cardelli’s proof of their Lemma 5.4.3 can be seen asa 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 therules Sub-eq and Sub-trans.
The idea of this decomposition can be illustrated by an example in Figure 12. The upper partof the figure shows a derivation by following Amadio and Cardelli’s subtyping algorithm forequi-recursive subtyping. Note that there are two applications of rule Sub-eq in the derivation,
one for expanding the type 𝜇𝛼 . ⊤ → 𝛼 to ⊤ → 𝜇𝛼 . ⊤ → ⊤ → 𝛼 and the other for expanding
the type 𝐵 to its unfolding Int → ⊤ → 𝐵. Although rule Sub-eq is applied in the middle of thederivation, 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 showssuch a derivation, in which we use 𝐶 and 𝐷 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Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′·; · ⊢ 𝐴 ↩→ 𝐶 1 : 𝑐 1· ⊢ 𝐶 1 ≤𝑖 𝐶 2·; · ⊢ 𝐶 2 ↩→ 𝐵 : 𝑐 2Γ ⊢𝑒 𝑒 : 𝐵 ▷ cast [𝑐 2 ] (cast [𝑐 1 ] 𝑒 )′Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:24

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

If one ignores the gray parts in the rule, rule ETyp-sub is equivalent to rule ETyp-bare-sub. We canfirst 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 𝜆𝐹𝑖 . Therefore,𝜇<:
we can conclude that 𝜆𝐹𝑖 with iso-recursive subtyping is sound and complete with respect to a
calculus with equi-recursive subtyping in terms of typing.
𝜇Unlike 𝜆𝐹𝑖 , the cast operator in rule ETyp-sub cannot be automatically generated, since Theorem 5.5 by Amadio and Cardelli is not done in a constructive way, and they choose regular equations,a different representation of recursive types, to complete the proof. Therefore, it is not easy toturn their results into an algorithm that generates the cast operator for equi-recursive subtyping,𝜇<:which we leave as future work. Nevertheless, 𝜆𝐹𝑖 itself is still useful if one wants to work with
iso-recursive types but expects expressive power similar to equi-recursive subtyping.
Theorem 5.6 (Typing equivalence for 𝜆𝐹𝑖 ). For any expressions 𝑒, 𝑒 ′ and type 𝐴,(1) (Soundness) if Γ ⊢ 𝑒 : 𝐴 then Γ ⊢𝑒 |𝑒 | : 𝐴 ▷ 𝑒.
(2) (Completeness) if Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ then Γ ⊢ 𝑒 ′ : 𝐴.
(3) (Round-tripping) if Γ ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ , then |𝑒 ′ | = 𝑒.
𝜇<:

5.4

Behavioral Equivalence𝜇<:We also show that 𝜆𝐹𝑖 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 𝜆𝐹𝑖 to equi-recursive behavioral equivalence by erasure of castoperators 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 𝜆𝐹𝑖 in preserving the equi-recursive reductions, except thatduring 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, 𝜆𝐹𝑖 is equivalent
to a calculus with equi-recursive subtyping.
Theorem 5.7 (Behavioral equivalence of 𝜆𝐹𝑖 ). For any expression 𝑒, 𝑒 ′ and type 𝐴 in 𝜆𝐹𝑖 , if
· ⊢𝑒 𝑒 : 𝐴 ▷ 𝑒 ′ , then(1) 𝑒 ↩→𝑒∗ 𝑣 if and only if there exists 𝑣 ′ such that 𝑒 ′ ↩→∗ 𝑣 ′ and |𝑣 ′ | = 𝑣.
(2) 𝑒 diverges if and only if 𝑒 ′ 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 [Crary et al. 1999; Gunter 1992; Harper and Mitchell 1993]. 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 andTobin-Hochstadt 2016], and the foundation of Scala through Dependent object types (DOT) [Aminet 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].
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:25In real-world programming languages, different languages have adopted different formulations. Isorecursive types are used in languages like Standard ML [Vanderwaart et al. 2003], Haskell [Weirich
et al. 2011], and OCaml [Dreyer et al. 2001], while equi-recursive types are used in languages like
Modula-3 [Cardelli et al. 1989] and Scala [Odersky et al. 2004].
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 translatingequi-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 programlogic which was conjectured to be sound. As we have argued in §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, andalso prevents a round-tripping property. Thirdly, their coercion rules are based on a declarative
specification of equi-recursive type equality by Amadio and Cardelli [1993], which does not have aknown algorithm to generate coercions automatically. To see this, consider their coercion typing
rule for rule Tyeq-contract:𝑠 : 𝐴[𝛼 ↦→ 𝐵 1 ]  𝐵 1 : 𝑡𝑠 ′ : 𝐴[𝛼 ↦→ 𝐵 2 ]  𝐵 2 : 𝑡 ′𝐴 is contractive in 𝛼it(𝑡 ′, 𝑠 ′ ).coit(𝑡, 𝑠) : 𝐵 1  𝐵 2 : it(𝑡, 𝑠).coit(𝑡 ′, 𝑠 ′ )The judgement 𝑠 : 𝐴  𝐵 : 𝑡 extends Amadio and Cardelli’s equi-recursive type equality with two
coercion functions 𝑠 : 𝐴 → 𝐵 and 𝑡 : 𝐵 → 𝐴. For example, the first premise says that from equality𝐴[𝛼 ↦→ 𝐵 1 ]  𝐵 1 one can derive coercion functions 𝑠 : 𝐴[𝛼 ↦→ 𝐵 1 ] → 𝐵 1 and 𝑡 : 𝐵 1 → 𝐴[𝛼 ↦→ 𝐵 1 ].
They define special combinators it(·, ·) and coit(·, ·) to combine these coercion functions. Basically,
the it combinator can be used to obtain a coercion function it(𝑠, 𝑡) : 𝜇𝛼 . 𝐴 → 𝐵 1 , while the coit
combinator gives coit(𝑡 ′, 𝑠 ′ ) : 𝐵 2 → 𝜇𝛼 . 𝐴. Therefore their composition it(𝑡, 𝑠).coit(𝑡 ′, 𝑠 ′ ) serves asa coercion function from 𝐵 2 to 𝐵 1 . As can be seen from the rule, to obtain a well-typed coercion
function from the rule Tyeq-contract, these complex combinators are necessary and cause asignificant overhead. By using casts, we avoid all these issues with coercion functions, leading toan easier, and fully formalized, way to establish behavioral equivalence.
Recently, Patrignani et al. [2021] examined the contextual equivalence between iso- and equirecursive types, providing a mechanized proof in Coq for fully abstract compilers. Their focus wason the compilation from iso-recursive to equi-recursive types. They proved that the translationfrom iso-recursive to equi-recursive types, by erasing unfold/fold operations, is fully abstract withrespect to contextual equivalence. The work also covered the compiler from term-level fixpoints toequi-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 typeequality, 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 refinedand simplified the original study [Brandt and Henglein 1998; Danielsson and Altenkirch 2010;
Gapeyev et al. 2002; Komendantsky 2011]. In particular, Brandt and Henglein [1998] introduced afixpoint rule for a coinductive relation within an inductive framework. Their rules give rise to anatural operational interpretation of proofs as coercions, as they indicated as future work in theirpaper. Our work is inspired by their work, and we formally present an operational interpretation ofequi-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
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:26

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

types. Furthermore, we show that our computationally irrelevant cast operators simplify themetatheory and extend to subtyping as well.
Iso-recursive subtyping, notably through the Amber rules [Cardelli 1985], has long been used.
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]. This proof relies on a complex inductive argument and wasfound difficult to formalize in theorem provers [Backes et al. 2014; Zhou et al. 2022]. Zhou et al.,proposed alternative formulations of iso-recursive subtyping equivalent to the Amber rules and arealso easier to reason with. Their work comes with a comprehensive formalization of the metatheoryof iso-recursive subtyping. Our work is based on some of their findings. In particular we reuse theirmechanized 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 moregeneral setting, in terms of typing and operational semantics.
To address the complexities of iso-recursive subtyping, several alternative formulations of isorecursive 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. Thisapproach extends the iso-recursive Amber rules but is still not complete with respect to the equirecursive 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 semanticinterpretation 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 andsum 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 relationthat allows an explicit transitivity rule to be included. They formally proved that this relation isequivalent to the tree model of subtyping as well as Brandt and Henglein’s subtyping relation. In asimilar 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 froma calculus with term-level fixpoints to a calculus with equi-recursive types. All of our results aremechanized 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 thetransformations between types related by equi-recursive equalities. Several studies [Cretin 2014;
Gundry 2013; Kimmell et al. 2012; Sjöberg et al. 2012; Sjöberg and Weirich 2015; Stump et al. 2009;
Sulzmann et al. 2007; Weirich et al. 2017; Yang and Oliveira 2019] have also used explicit casts forProc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:27

managed type-level computation. However, casts in those approaches primarily address type-levelcomputations within contexts such as dependent types or type-level programming, rather than theoperational interpretation of recursive type equalities. When considering the dynamic semantics ofcast-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; Weirich et al.
2013, 2017; Yorgey et al. 2012], which is the approach that we adopt in our work. Our push rules
designs resemble the ones used in the work of Sulzmann et al. [2007], where input arguments
are applied a reversed cast, but our work directly creates a new cast expression for the concrete
input expression while Sulzmann et al. rewrite the 𝜆-term. Similar designs can also be seen inother lines of work, such as the blame calculus and gradual typing [Findler and Felleisen 2002;
Siek and Taha 2007]. However, with full iso-recursive types we expect the casts to be erasable
during runtime, which is not the case in gradual typing. Pure Iso-type Systems (PITS) [Yang andOliveira 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 ofsubsuming 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 computationallyirrelevant cast operator in the term language that captures all the equi-recursive type equalities.
𝜇
We present 𝜆𝐹𝑖 , a calculus that extends simply typed lambda calculus with full iso-recursive types.
𝜇𝜆𝐹𝑖 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, byencoding equi-recursive subtyping using iso-recursive subtyping with cast operators.
𝜇As future work, we plan to extend 𝜆𝐹𝑖 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.
Data-Availability Statement
The artifact that supports the paper is available on Zenodo [Zhou et al. 2024] and https://github.
com/ltzone/Full-Iso-Recursive-Types.
Acknowledgments
We are grateful to the anonymous reviewers for their valuable comments. This work has beensponsored by Hong Kong Research Grant Council project number 17209821.
References
Martin Abadi and Luca Cardelli. 1996. A theory of objects. Springer Science & Business Media. https://doi.org/10.1007/9781-4419-8598-9
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. https://doi.org/10.1109/LICS.1996.561324
Roberto M Amadio and Luca Cardelli. 1993. Subtyping recursive types. ACM Transactions on Programming Languages andSystems (TOPLAS) 15, 4 (1993), 575–631. https://doi.org/10.1145/155183.155231
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:28

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

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. https://doi.org/10.1007/978-3-319-30936-1_14
Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. 2008. Engineering formal
metatheory. Acm sigplan notices 43, 1 (2008), 3–15. https://doi.org/10.1145/1328897.1328443
Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2014. Union, intersection and refinement types and reasoning abouttype disjointness for secure protocol implementations. J. Comput. Secur. 22, 2 (mar 2014), 301–353.
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.
https://doi.org/10.1145/1890028.1890031
Michael Brandt and Fritz Henglein. 1998. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta
Informaticae 33, 4 (1998), 309–338. https://doi.org/10.3233/FI-1998-33401
Yufei Cai, Paolo G Giarrusso, and Klaus Ostermann. 2016. System F-omega with equirecursive types for datatype-generic
programming. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. 30–43.
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).
Luca Cardelli, Jim Donahue, Mick Jordan, Bill Kalsow, and Greg Nelson. 1989. The Modula–3 type system. In Proceedings ofthe 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 202–212. https://doi.org/10.1145/
75277.75295
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.
https://doi.org/10.1145/1599410.1599437
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.
https://doi.org/10.1145/2643135.2643138
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. https://doi.org/10.1007/978-3-662-46669-8_11
Dario Colazzo and Giorgio Ghelli. 2005. Subtyping recursion and parametric polymorphism in kernel fun. Information andComputation 198, 2 (2005), 71–147. https://doi.org/10.1016/j.ic.2004.11.003
Karl Crary. 2000. Typed compilation of inclusive subtyping. In Proceedings of the fifth ACM SIGPLAN international conference
on Functional programming. 68–81. https://doi.org/10.1145/351240.351247
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. https://doi.org/10.1145/301618.301641
Julien Cretin. 2014. Erasable coercions: a unified approach to type systems. Ph. D. Dissertation. Université Paris-Diderot-Paris
VII.
Nils Anders Danielsson and Thorsten Altenkirch. 2010. Subtyping, declaratively: An exercise in mixed induction andcoinduction. In Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June
21-23, 2010. Proceedings 10. Springer, 100–118. https://doi.org/10.1007/978-3-642-13321-3_8
Derek Dreyer. 2005. Understanding and Evolving the ML Module System. Ph. D. Dissertation. School of Computer Science,
Carnegie Mellon University.
Derek R. Dreyer, Robert Harper, and Karl Krary. 2001. Toward a Practical Type Theory for Recursive Modules. Technical
Report CMU-CS-01-112. School of Computer Science, Carnegie Mellon University.
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. https://doi.org/10.1145/586088.586093
Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for higher-order functions. In Proceedings of the seventh ACM
SIGPLAN international conference on Functional programming. 48–59. https://doi.org/10.1145/581478.581484
Vladimir Gapeyev, Michael Y Levin, and Benjamin C Pierce. 2002. Recursive subtyping revealed. Journal of Functional
Programming 12, 6 (2002), 511–548. https://doi.org/10.1017/S0956796802004318
Simon Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. Acta Informatica 42 (2005), 191–225.
https://doi.org/10.1007/s00236-005-0177-z
Simon J Gay and Vasco T Vasconcelos. 2010. Linear type theory for asynchronous session types. Journal of Functional
Programming 20, 1 (2010), 19–50. https://doi.org/10.1017/S0956796809990268
Giorgio Ghelli. 1993. Recursive types are not conservative over F≤. In International Conference on Typed Lambda Calculi
and Applications. Springer, 146–162. https://doi.org/10.1007/BFb0037104
Adam Michael Gundry. 2013. Type inference, Haskell and dependent types. (2013).

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

Full Iso-Recursive Types

278:29Carl A Gunter. 1992. Semantics of programming languages: structures and techniques. MIT press.
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. https://doi.org/10.1145/169701.169696
Robert Harper and Christopher Stone. 2000. A type-theoretic interpretation of Standard ML. (2000). https://doi.org/10.
7551/mitpress/5641.003.0019
Martin Hofmann and Benjamin Pierce. 1995. Positive subtyping. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposiumon Principles of programming languages. 186–197.
Alan Jeffrey. 2001. A symbolic labelled transition system for coinductive subtyping of F< types. In 2001 IEEE Conference on
Logic and Computer Science (LICS 2001), Vol. 323.
Timothy Jones and David J Pearce. 2016. A mechanical soundness proof for subtyping over recursive types. In Proceedingsof the 18th Workshop on Formal Techniques for Java-like Programs. 1–6. https://doi.org/10.1145/2955811.2955812
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 andcall-by-value semantics. In Proceedings of the sixth workshop on Programming languages meets program verification. 15–26.
https://doi.org/10.1145/2103776.2103780
Vladimir Komendantsky. 2011. Subtyping by folding an inductive relation into a coinductive one. In International Symposiumon Trends in Functional Programming. Springer, 17–32.
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.
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. https://doi.org/10.1145/2994596
James H Morris. 1968. Lambda calculus models of programming languages. (1968).
Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Stphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik
Stenman, and Matthias Zenger. 2004. The Scala language specification.
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. https://doi.org/10.1145/3434302
Benjamin C Pierce. 2002. Types and programming languages. MIT press.
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.
https://doi.org/10.1145/2983990.2984008
Andreas Rossberg. 2023. Mutually Iso-Recursive Subtyping. Proceedings of the ACM on Programming Languages 7, OOPSLA2(2023), 347–373. https://doi.org/10.1145/3622809
Claudio V. Russo. 2001. Recursive Structures for Standard ML. In Proceedings of the Sixth ACM SIGPLAN International
Conference on Functional Programming (ICFP ’01), Firenze (Florence), Italy, September 3-5, 2001, Benjamin C. Pierce (Ed.).
ACM, 50–61.
Jeremy Siek and Walid Taha. 2007. Gradual typing for objects. In European Conference on Object-Oriented Programming.
Springer, 2–27.
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.
https://doi.org/10.1007/978-3-319-30936-1_21
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 typesystems. arXiv preprint arXiv:1202.2923 (2012).
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. https://doi.org/10.1145/2676726.2676974
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. https://doi.org/10.1145/
1481848.1481856
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. https://doi.org/10.1145/1190315.1190324
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. https://doi.org/10.1145/2034574.
2034811Pawel Urzyczyn. 1995. Positive recursive type assignment. In International Symposium on Mathematical Foundations ofComputer Science. Springer, 382–391.

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.

278:30

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira

Joseph C Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, and Perry Cheng. 2003. Typed compilationof recursive datatypes. ACM SIGPLAN Notices 38, 3 (2003), 98–108. https://doi.org/10.1145/640136.604187
Stephanie Weirich, Justin Hsu, and Richard A Eisenberg. 2013. System FC with explicit kind equality. ACM SIGPLAN Notices
48, 9 (2013), 275–286. https://doi.org/10.1145/2544174.2500599
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. https://doi.org/10.1145/3110275
Stephanie Weirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic. 2011. Generative type abstraction andtype-level computation. ACM SIGPLAN Notices 46, 1 (2011), 227–240. https://doi.org/10.1145/1925844.1926411
Yanpeng Yang and Bruno C. d. S. Oliveira. 2019. Pure iso-type systems. Journal of Functional Programming 29 (2019), e14.
https://doi.org/10.1017/S0956796819000108
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. https://doi.org/10.1145/2103786.2103795
Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira. 2024. Full Iso-recursive Types (Artifact). https://doi.org/10.5281/
zenodo.12669929
Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira. 2023. Recursive Subtyping for All. Proceedings of the ACM on
Programming Languages 7, POPL (2023), 1396–1425. https://doi.org/10.1145/3571241
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. https://doi.org/10.1145/3428291
Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2022. Revisiting Iso-recursive subtyping. ACM Transactions on
Programming Languages and Systems (TOPLAS) 44, 4 (2022), 1–54. https://doi.org/10.1145/3549537

Received 2024-04-04; accepted 2024-08-18

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA2, Article 278. Publication date: October 2024.