1
Revisiting Iso-Recursive Subtyping
YAODA ZHOU, The University of Hong Kong, China
JINXU ZHAO, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
The Amber rules are well-known and widely used for subtyping iso-recursive types. They were first briefly
and informally introduced in 1985 by Cardelli in a manuscript describing the Amber language. Despite theiruse over many years, important aspects of the metatheory of the iso-recursive style Amber rules have notbeen studied in depth or turn out to be quite challenging to formalize.
This paper aims to revisit the problem of subtyping iso-recursive types. We start by introducing a novel
declarative specification for Amber-style iso-recursive subtyping. Informally, the specification states that tworecursive types are subtypes if all their finite unfoldings are subtypes. The Amber rules are shown to haveequivalent expressive power to this declarative specification. We then show two variants of sound, complete
and decidable algorithmic formulations of subtyping with respect to the declarative specification, which
employ the idea of double unfoldings. Compared to the Amber rules, the double unfolding rules have theadvantage of: (1) being modular; (2) not requiring reflexivity to be built in; (3) leading to an easy proof oftransitivity of subtyping; and (4) being easily applicable to subtyping relations that are not antisymmetric(such as subtyping relations with record types). This work sheds new insights on the theory of subtyping
iso-recursive types, and the new rules based on double unfoldings have important advantages over the originalAmber rules involving recursive types. All results are mechanically formalized in the Coq theorem prover.
CCS Concepts: • Theory of computation → Type theory; • Software and its engineering → Object
oriented languages.
Additional Key Words and Phrases: Iso-recursive types, Formalization, Subtyping
ACM Reference Format:
Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2022. Revisiting Iso-Recursive Subtyping. ACM Trans.
Program. Lang. Syst. 1, 1, Article 1 (January 2022), 55 pages. https://doi.org/10.1145/3549537

1

INTRODUCTION

Recursive types are used in nearly all languages to define recursive data structures like sequences ortrees. They are also used in Object-Oriented Programming every time a method needs an argument
or return type of the enclosing class.
Recursive types come in two flavours: equi-recursive types and iso-recursive types [Crary et al.
1999]. With equi-recursive types a recursive type is equal to its unfolding. With iso-recursive types,a recursive type and its unfolding are only isomorphic. To convert between the (iso-)recursivetype and its isomorphic unfolding, explicit folding and unfolding constructs are necessary. The
main advantage of equi-recursive types is convenience, as no explicit conversions are necessary.
Authors’ addresses: Yaoda Zhou, Department of Computer Science, The University of Hong Kong, Hong Kong, China,
ydzhou@cs.hku.hk; Jinxu Zhao, Department of Computer Science, The University of Hong Kong, Hong Kong, China,
jxzhao@cs.hku.hk; Bruno C. d. S. Oliveira, Department of Computer Science, The 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 components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2022 Association for Computing Machinery.
0164-0925/2022/1-ART1 $15.00
https://doi.org/10.1145/3549537

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:2

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

However, a disadvantage is that algorithms for languages with equi-recursive types are quite
complex. Furthermore, integrating equi-recursive types in type systems with advanced type features, while retaining desirable properties such as decidable type-checking, can be hard (or even
impossible) [Colazzo and Ghelli 1999; Ghelli 1993; Solomon 1978].
The Amber rules are well-known and widely used for subtyping iso-recursive types. They
were briefly and informally introduced in 1985 by Cardelli in a manuscript describing the Amber
language [Cardelli 1985]. Later on, Amadio and Cardelli [1993] made a comprehensive study ofthe theory of recursive subtyping for a system with equi-recursive types employing Amber-stylerules. One nice result of their study is a declarative model for specifying when two recursive types
are in a subtyping relation. In essence, two (equi-)recursive types are subtypes if their infinite
unfoldings are subtypes. Amadio and Cardelli’s study remains to the day a standard reference
for the theory of equi-recursive subtyping, although newer work simplifies and improves on theoriginal theory [Brandt and Henglein 1997; Gapeyev et al. 2003]. Since then variants of the Amber
rules have been employed multiple times in a variety of calculi and languages, but often in an
iso-recursive setting [Abadi and Cardelli 1996; Bengtson et al. 2011; Chugh 2015; Duggan 2002;
Lee et al. 2015; Swamy et al. 2011]. Perhaps most prominently the seminal work on “A Theory of
Objects” by Abadi and Cardelli [1996] employs iso-recursive style Amber rules.
The Amber rules are appealing due to their apparent simplicity, but the metatheory for their isorecursive formulation is not well studied. Unlike an equi-recursive formulation, which has a clear
declarative specification, there is no similar declarative specification for an iso-recursive formulation
so far. Moreover, there are fundamental differences between equi-recursive and iso-recursive
subtyping: while equi-recursive subtyping deals with infinite trees and is naturally understood in acoinductive setting [Brandt and Henglein 1997; Gapeyev et al. 2003], an Amber-style iso-recursive
formulation deals with finite trees and ought to be understood in an inductive setting. Furthermore,
important properties for algorithmic versions of the iso-recursive Amber rules are lacking or arequite difficult to prove. In particular, there is very little work in the literature regarding proof oftransitivity for algorithmic formulations of the Amber rules. Finally, a fundamental lemma thatarises in proofs of type preservation for calculi with iso-recursive subtyping is:
If 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵
We call this lemma the unfolding lemma. The unfolding lemma plays a similar role in preservation
to the substitution lemma (which is needed for proving preservation of beta-reduction), and isused to prove the case dealing with recursive type unfolding. The proof for the unfolding lemma is
non-trivial, but there is also little work on proofs of this lemma for the Amber rules. While there
are some interesting alternatives for iso-recursive subtyping [Hofmann and Pierce 1996; Ligatti
et al. 2017], Amber-style subtyping strikes a good balance between expressive power and simplicity,and is widely used. Thus understanding Amber-style subtyping further is worthwhile.
This paper aims to revisit the problem of subtyping iso-recursive types. We start by introducing anovel declarative specification for Amber-style iso-recursive subtyping. Informally, the specification
states that two recursive types are subtypes if all their finite unfoldings are subtypes. More formally,
the subtyping rule for recursive types is:Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐴] 𝑛 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝑛 𝐵Γ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵∀𝑛 = 1 · · · ∞S-RecHere the notation [𝛼 ↦→ 𝐴] 𝑛 denotes the 𝑛-times finite unfolding of a type. The 𝑛 times unfolding
applies 𝑛 − 1 substitutions to the type 𝐴 (the recursive type body), and the rule checks that all
𝑛-times unfoldings are subtypes. Such a declarative formulation plays a similar role to Amadio andCardelli’s declarative specification for equi-recursive types. Because the specification is defined
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:3

with respect to the finite unfoldings, this naturally leads to an inductive treatment of the theory. For
example, the proof of transitivity of subtyping is fairly straightforward, with the more significant
challenge being the unfolding lemma. With all the metatheory in place, proving subject-reduction
for a typed lambda calculus with recursive types is a routine exercise. Moreover, the Amber rules
are shown to be equivalent (in terms of expressive power) to this declarative specification.
We also show alternative algorithmic formulations based on the idea of double unfoldings. We
discuss two variants of rules for subtyping recursive types. The first variant, which we call the
double unfolding rule, checks both 1-time and 2-times finite unfoldings. The second variant canbe seen as an optimization that checks only 2-times finite unfoldings, by tracking the names of
the recursive types to avoid the 1-time finite unfolding check. We call the second variant nominal
unfolding. Both rules accept all valid subtyping statements that the Amber rules accept, but they
have important advantages. In particular the rules with double unfoldings:• Enable modular proofs. The new subtyping rules for recursive types are modular in thesense that proofs for properties such as transitivity or reflexivity only need to account for the
new recursive case. All the other cases remain essentially the same as in a subtyping relation
without recursive types. Key to this form of modularity is the use standard environments,
which are just a collection of type variables.
• Have easy proofs of transitivity of subtyping. A particular consequence of the previous
point is an easy proof for transitivity, which has been a stumbling block in the past for
the iso-recursive Amber rules. The Amber rules have a pervasive impact in the subtyping
relation, which is the root cause of the difficulties in doing proofs such as transitivity. To ourknowledge the only transitivity proof for the Amber rules is due to Bengtson et al. [2011],
and the proof is quite intricate, relying on a complex inductive argument.
• Do not require built-in reflexivity. An additional benefit is that reflexivity does not haveto be built in, but it can be derived instead. In the Amber rules built-in reflexivity is necessary
to deal with contravariant occurrences of recursive type variables.
• Are applicable to non-antisymmetric subtyping relations. Built-in reflexivity can beproblematic in some settings, including calculi with record subtyping or intersection/union
types. Such calculi can have “isomorphic” subtyping where two syntactically different types
𝐴 and 𝐵 can be subtypes of each other. In other words the subtyping relation is not antisymmetric. Avoiding built-in reflexivity makes the rules easier to apply in such settings. As weshow, the double unfolding rules can deal with record types easily.
The focus of our work is on iso-recursive subtyping rules that enable easy metatheory, andimproving the understanding of Amber-style iso-recursive subtyping. Therefore our work will be
useful to those interested on the theory of recursive types, as well as for formalizations of calculi
using iso-recursive subtyping. Formalizations can benefit from our work to easily develop calculi
with recursive types and prove important properties, such as transitivity, decidability and typesoundness. While the rules based on double unfolding rules are algorithmic and therefore can beused in implementations, our focus is not on efficient algorithms. For implementations, the use of
the Amber rules may still be preferable if efficiency is an important concern. Moreover, there arealternatives to the Amber rules, such as the complete rules by Ligatti et al. [2017], which may be
preferable for extra expressive power in the subtyping relation, as well as efficient algorithms.
To validate all our results we have mechanically formalized all our results in the Coq theorem
prover. As far as we know this is the first comprehensive treatment of iso-recursive subtyping
dealing with unrestricted recursive types in a theorem prover.
In summary, the contributions of this paper are:
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:4

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Table 1. Some key theorems in the paper.

Reflexivity Transitivity Unfolding Lemma
Amber Rules
Built-in
Corollary 58
Corollary 59
Finite Unfolding
Theorem 5
Theorem 6
Lemma 8
Double Unfolding
Theorem 15 Theorem 16
Lemma 24
Nominal Unfolding
Theorem 25 Theorem 26
Lemma 27
Weakly Positive Subtyping Theorem 39 Theorem 41
Lemma 42
• A declarative specification for iso-recursive subtyping: We propose a new declarative
specification for iso-recursive subtyping, where two recursive types are subtypes if all thefinite unfoldings are subtypes in Section 3.
• Algorithmic subtyping based on double unfoldings: We show two sound, complete anddecidable algorithmic formulations of subtyping employing the idea of double unfoldings
in Section 4. The first formulation uses a so-called double unfolding rule, and the second
formulation uses a so-called nominal unfolding rule.
• Equivalence to the Amber rules: We prove that the Amber rules are equivalent, in termsof expressive power, to our new formulation of subtyping in Section 5.
• Subject-reduction for a typed lambda calculus with recursive types and record types:
To illustrate the applicability of our results to calculi with subtyping relations that are notantisymmetric, we formalize a typed lambda calculus with recursive types as well as record
types and prove type preservation and progress in Section 6.
• Subtyping with a Weakly Positive Restriction: In addition to the Amber rules and thefinite and the rules based on double unfoldings, we also give another equivalent formulation ofsubtyping based on a weakly positive restriction of recursive variables. This variant captures
precisely a folklore observation that the Amber rules express two situations where a recursive
variable can be a subtype of another type: positive subtyping and reflexivity. This variant,presented as part of Section 5, is used as an intermediate step to prove the equivalence
between the Amber rules and a formulation using double unfolding.
• Mechanical formalization: All the results are formalized in the Coq theorem prover andcan be found at: https://github.com/juda/Iso-Recursive-Subtyping
Table 1 and Figure 1 summarize some key lemmas and theorems of this paper. In particular, it
shows that all five formulations of subtyping presented in this paper are equivalent in terms ofexpressive power.
This article is a significantly expanded version of a conference paper [Zhou et al. 2020]. There
are several improvements with respect to the conference version. First of all, we considerably
simplify the proof of soundness theorem between double and finite unfoldings, and provide a proofof the unfolding lemma directly using the double unfolding rules. In the original soundness proof,a special relation capturing valid subtyping derivations was used. In the new proof, this relationand proof technique is no longer used, greatly simplifying the proof. Secondly, we prove that
the Amber rules are complete with respect to the double unfolding formalization. Consequently,
all five subtyping formulations are shown to be equivalent (Figure 1). The conference version
only shows the soundness of the Amber rules with respect to finite unfoldings, but not theircompleteness. Thirdly we present a variant of double unfoldings, called nominal unfoldings, which
are more efficient that double unfoldings and yet preserve all of the key advantages in terms ofthe development of the meta-theory of the original double unfolding rules. Finally, the material
in Section 6, showing that our new rules can be applied to calculi with record types, is new. ThisACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:5

Nominal UnfoldingΓ ⊢𝑛 𝐴 ≤ 𝐵(Figure 9)
Corollary 32

Corollary 33
Theorem 31

Finite Unfolding(Specification)Γ⊢𝐴 ≤𝐵(Figure 6)
Corollary 50

Theorem 17
Theorem 21

Corollary 57

Amber Rules
Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵(Figure 10)

Theorem 45
Theorem 55

Theorem 30

Double UnfoldingΓ ⊢𝑎 𝐴 ≤ 𝐵(Figure 8)
Theorem 49

Theorem 52

Weakly Positive SubtypingΓ ⊢ 𝐴 ≤+ 𝐵
(Figure 11)

Fig. 1. A diagram with the soundness and completeness lemmas in this work.

is interesting because it shows that rules based on double unfoldings can deal smoothly with
subtyping relations that are not antisymmetric, unlike the Amber rules.
2

OVERVIEWThis section provides an overview of the problem of iso-recursive subtyping and our results. We
first briefly review applications of iso-recursive subtyping, introduce some alternative formulations
for iso-recursive subtyping, and discuss some issues with the Amber rules. Then we present the key
ideas of our work, including a novel declarative formulation of subtyping and the two algorithmic
variants based on double unfoldings. Finally, we show how the double unfolding rule can be
employed in calculi with record types.
2.1

Applications of Iso-Recursive Types

Before we move to our work we first briefly review some of the applications of iso-recursive types.
Many programming languages adopt an iso-recursive formulation. In practice, the inconvenienceof iso-recursive types is mostly eliminated by “hiding” the explicit folding and unfolding in otherconstructs. For example, in functional languages, such as Haskell or ML, a flavour of iso-recursive
types is provided via datatypes.
Figure 2 (left) illustrates a simple recursive type in Haskell. The List datatype is recursive, as
the Cons constructor requires a List as the second argument. Functions such as map, can thenbe defined by pattern matching. While there are no explicit folding or unfolding operations in
the program, every use of the constructors (Nil and Cons) triggers folding of the recursive type.
Conversely, the patterns on Nil and Cons trigger unfolding of the recursive type. Similarly, in
nominal Object-Oriented (OO) languages such as Java, iso-recursive types can be introduced in classdefinitions such as the one to the right of Figure 2. This class definition requires recursive types
because both compareArea and clone need to refer to the enclosing class. Like the Haskell program
above, there are no explicit uses of folding and unfolding. Instead, constructors trigger foldingof the recursive type; while method calls (such as area()) trigger recursive type unfolding. The
relationship between iso-recursive types, algebraic datatypes and pattern matching, and nominal
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:6

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveiradata List = Nil | Cons Int List
map :: (Int -> Int) -> List -> List
map f Nil=
Nil
map f (Cons x xs) =Cons (f x) (map f xs)

class Shape {int area() {...}
boolean compareArea(Shape s) {return s.area() == area();}
Shape clone() {return new Shape();}}Fig. 2. Recursive types in Haskell (left) and Java (right).

OO class definitions is well-understood in the research literature [Lee et al. 2015; Pierce 2002; Stoneand Harper 1996; Vanderwaart et al. 2003; Yang and Oliveira 2019].
2.2

Subtyping Recursive Types

Subtyping is a widely-used inclusion relation that compares two types. Many calculi have no typesof “infinite” size. In such calculi comparing two types is relatively easy. However, with the existenceof recursive types, comparing two types is no longer trivial. A recursive type 𝜇𝛼 . 𝐴 usually contains
itself as a subpart, represented by the type variable 𝛼. Therefore, a subtyping relation (or anotherform of comparison) needs to treat these types in a special way.
We choose to use a minimal set of types throughout this work for illustration. A type 𝐴, 𝐵, 𝐶, or
𝐷 may refer to the primitive nat type, the top type ⊤, a function type 𝐴 → 𝐵, a type variable 𝛼 ora recursive type 𝜇𝛼 . 𝐴. The subtyping rules for the top type, primitive types and function types are
standard:𝐵 1 ≤ 𝐴1𝐴2 ≤ 𝐵 2𝐴≤⊤nat ≤ nat
𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2
Before diving into the design of subtyping relations for recursive types, we first look at someexamples. We also discuss the role of the unfolding lemma in checking whether a subtyping relation
between two recursive types is valid or not.
Example 1. Any type should be a subtype of itself, including1• 𝜇𝛼 . 𝛼 → 𝛼 ≤ 𝜇𝛼 . 𝛼 → 𝛼,
• 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → nat,
• 𝜇𝛼 . nat → 𝛼 ≤ 𝜇𝛼 . nat → 𝛼.
An important aspect to pay attention to here is the negative occurrences of recursive type variables,
which occur in the first two examples. The combination of contravariance of function types andrecursive types is a key cause to some complexity which is necessary when subtyping recursive
types, even for the case of equal types. Indeed, this is the key reason why in the Amber rules areflexivity rule is needed. We will come back to this point in Section 2.5.
Example 2. A second example is 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → 𝛼. This example illustrates positive
recursive subtyping, since the recursive variables are used only in positive positions, and the two
types are not equal. The left type is a function that consumes infinite values of any type, and theright type consumes infinite nat values. Hence, the left type is more general than the right type.
Example 3. The type 𝜇𝛼 . 𝛼 → nat is not a subtype of 𝜇𝛼 . 𝛼 → ⊤. This final example serves
the purpose of illustrating negative recursive subtyping, where recursive type variables occur innegative positions. If we ignore the recursive parts of these types, 𝐴 → nat ≤ 𝐴 → ⊤ holds for
1 We assume that recursive types have lower priority. That is, 𝜇𝛼 . ⊤ → 𝛼 means 𝜇𝛼 . (⊤ → 𝛼) not (𝜇𝛼 . ⊤) → 𝛼.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:7

any type 𝐴. But that does not imply that 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → ⊤, because the type variable 𝛼
on different sides refers to different types. If we unfold both types twice, we get:((𝜇𝛼 .𝛼 → nat) → nat) → nat

v.s.

((𝜇𝛼 .𝛼 → ⊤) → ⊤) → ⊤which should be rejected by the subtyping relation. Because of the contravariance of functions, weneed to check not only that nat ≤ ⊤ but also that ⊤ ≤ nat (which does not hold).
The role of the unfolding lemma. In Example 3 we argued that subtyping should be rejectedwithout actually defining a rule for subtyping of recursive types. The argument was that in suchcase subtyping should be rejected because unfolding the recursive type a few times leads to a
subtyping relation that is going to be rejected by some other rule not involving recursive types.
The unfolding lemma captures the essence of this argument formally:
If 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵
It states that unfolding the types one time in a valid subtyping relation between recursive types
always leads to a valid subtyping relation between the unfoldings. This property plays an importantrole in type soundness, and it essentially guarantees the type preservation of recursive typeunfolding.
In the following subsections, we briefly review some possible designs for recursive subtyping.
2.3

A Rule That Only Works for Covariant Subtyping

As observed by Amadio and Cardelli [1993], a first idea to compare two recursive types is to use
the following rules:Γ, 𝛼 ⊢ 𝐴 ≤ 𝐵𝛼∈ΓΓ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵Γ⊢𝛼 ≤𝛼which accept, for example, 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → 𝛼 and 𝜇𝛼 . 𝛼 → 𝛼 ≤ 𝜇𝛼 . 𝛼 → 𝛼. Unfortunately,
these rules are unsound in the presence of negative recursive subtyping and contravariant subtyping
for function types. We can easily derive the following invalid relation with those rules:
𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → ⊤If we ignore the recursive symbol 𝜇, it is not immediately obvious that the subtyping relation is
problematic:
𝛼 → nat ≤ 𝛼 → ⊤However, after unfolding the types twice the problem becomes obvious, as shown in Example 3:((𝜇𝛼 . 𝛼 → nat) → nat) → nat ≤ ((𝜇𝛼 . 𝛼 → ⊤) → ⊤) → ⊤Generally speaking, these rules are sound for positive recursive subtyping. However, contravariant
recursive types, where the recursive type variables occur in negative positions, may allow unsoundsubtyping statements, as shown above.
2.4

The Positive Restriction Rule

To fix the unsound rule in the presence of contravariant subtyping, we might restrict it withpositivity checks on the types:
Γ, 𝛼 ⊢ 𝐴 ≤ 𝐵

non-neg(𝛼, 𝐴)
non-neg(𝛼, 𝐵)Γ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵

where non-neg(𝛼, 𝐴) is false when 𝛼 occurs in negative positions of 𝐴. This restriction, which was
also observed by Amadio and Cardelli [1993], solves the unsoundness problem and is employedin some languages and calculi [Backes et al. 2014]. The logic behind this restriction is that all the
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:8

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

subderivations which encounter 𝛼 ≤ 𝛼 (for some recursive type variable 𝛼) are valid. Since such
subderivations only occur in positive (or covariant) positions, the left 𝛼 represents 𝜇𝛼 . 𝐴, and theright 𝛼 represents 𝜇𝛼 . 𝐵. Since the subtyping is covariant, the statement 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 is valid, andall substatements 𝛼 ≤ 𝛼 are valid as well.
The main drawback of this rule is that no negative recursive subtyping is possible. It rejects
some valid relations, such as 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . 𝛼 → 𝛼. Furthermore, at least without some form ofreflexivity built-in, it even rejects subtyping of equal types with negative recursive variables, suchas 𝜇𝛼 . 𝛼 → 𝛼 ≤ 𝜇𝛼 . 𝛼 → 𝛼.
2.5

The Amber Rules

Equi-recursive Amber rules. The Amber rules were introduced in the Amber language by Cardelli[1985]. Later, Amadio and Cardelli [1993] studied the metatheory for a subtyping relation that
employs Amber-like rules. These rules are presented in Figure 3. The subtyping relation is declarative
as the transitivity rule (rule OAmber-trans) is built-in. The rule OAmber-top and rule OAmberarrow are standard. Rule OAmber-rec is the most prominent one, describing subtyping between
two recursive types. The key idea in the Amber rules is to use distinct type variables for the tworecursive types being compared (𝛼 and 𝛽). These two type variables are stored in the environment.
Later, if a subtyping statement of the form 𝛼 ≤ 𝛽 is found, rule OAmber-assmp is used to check
whether that pair is in the environment. The nice thing about rule OAmber-rec and rule OAmberassmp is that they work very well for positive subtyping. Furthermore, they rule out some bad caseswith negative subtyping, such as 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛽. 𝛽 → ⊤. Unfortunately, rule OAmber-rec
rules out too many cases with negative subtyping, including statements about equal types, suchas 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛽. 𝛽 → nat. To compensate for this, rule OAmber-rec is complemented by a(generalization of the) reflexivity rule (rule OAmber-refl). In the case of Amadio and Cardelli’s
original rules, rule OAmber-rec comes with a non-trivial definition of equality 𝐴 = 𝐵 (we refer totheir paper for details). Such equality allows deriving statements such as 𝜇𝛼 . nat → 𝛼 = 𝜇𝛼 . nat →nat → 𝛼 or 𝜇𝛼 . nat → 𝛼 = nat → 𝜇𝛼 . nat → 𝛼, which is used to ensure that recursive types andtheir unfoldings are equivalent. That is, generally speaking, the following equality holds at the
type-level:
𝜇𝛼 . 𝐴 = [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴
In other words, the set of rules defines a subtyping relation for equi-recursive types. Amadio andCardelli [1993] did a thorough study of the metatheory of such equi-recursive subtyping, including
providing an intuitive specification for recursive subtyping. In essence two recursive types are
subtypes if their infinite unfoldings are subtypes.
Iso-recursive Amber rules. Amadio and Cardelli’s set of rules is more powerful than what isnormally considered to be the folklore Amber rules for iso-recursive subtyping. Many typicalpresentations of the Amber rule simply use a variant of syntactic equality2 in reflexivity, which isless powerful, but it is enough to express iso-recursive subtyping. In what follows we consider thefolklore rules, where the equality (𝐴 = 𝐵) used in rule OAmber-refl is simplified by just considering
syntactic equality. The iso-recursive rules can deal correctly with all the examples illustrated sofar, accepting the various examples that we have argued should be accepted, and rejecting theother ones. Perhaps a small nitpicking point is the absence of well-formedness constraints in thesubtyping rules. By modern day standards, this may look a little suspicious, but then again wellformedness of environments and types is typically standard and straightforward. Unfortunately, as
it turns out, a suitable definition of well-formedness is non-trivial for Amber subtyping. We will
2 More precisely, in a setting where binders and variables are encoded using names, alpha-equivalence is used. In settings

where De Bruijn indices are used, it amounts to syntactic equality.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:9

Γ⊢𝐴 ≤𝐵
OAmber-refl

𝐴=𝐵(Original Amber Rules)
OAmber-trans

Γ⊢A≤B

Γ⊢A≤B

OAmber-assmp

Γ⊢B≤C

Γ⊢A≤C
OAmber-arrowΓ ⊢ B1 ≤ A1𝛼≤𝛽∈ΓOAmber-topΓ⊢𝛼 ≤𝛽Γ⊢A≤⊤

OAmber-recΓ ⊢ A2 ≤ B2

Γ ⊢ A1 → A2 ≤ B1 → B2

Γ, 𝛼 ≤ 𝛽 ⊢ A ≤ BΓ ⊢ 𝜇𝛼 . A ≤ 𝜇𝛽. 𝐵

Fig. 3. The complete Amber subtyping rules by Amadio and Cardelli [1993] for equi-recursive subtyping.

come back to this issue in Section 5. Setting the issue of well-formedness aside for the moment, theAmber rules have some other important issues:
Reflexivity cannot be eliminated. The reflexivity rule is essential to the subtyping relation. As wehave seen, one cannot even derive 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → nat without the reflexivity rule, due
to the contravariant positions of the variables. One possible fix is to add another rule that allows
variable subtyping in contravariant positions:𝛼≤𝛽∈ΓΓ⊢𝛽 ≤𝛼However, such rule allows unsound subtypes, for instance, 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → ⊤. In fact,adding this rule leads to a similar system to that in Section 2.3.
The reflexivity rule, if present in the subtyping relation, depends on a specific equivalence
judgment. Simple systems with antisymmetric subtyping relations might use syntactic equivalenceor alpha-equivalence. Yet syntactic or alpha-equivalence might be insufficient for other systems.
For example, permutation of fields on record types should be considered as equivalent types, thus
we may accept the following subtyping statement:
𝜇𝛼 . {𝑥 : 𝛼, 𝑦 : nat} → nat ≤ 𝜇𝛼 . {𝑦 : nat, 𝑥 : 𝛼 } → nat
However, if the built-in reflexivity employs only alpha-equivalence, such a subtyping statement
may be rejected. For instance if record types are modelled as sequences in the abstract syntax(which is quite common [Pierce 2002]), then the two records {𝑥 : 𝛼, 𝑦 : nat} and {𝑦 : nat, 𝑥 : 𝛼 }will be syntactically different. In this case the subtyping relation is not antisymmetric. That is both
{𝑥 : 𝛼, 𝑦 : nat} ≤ {𝑦 : nat, 𝑥 : 𝛼 } and {𝑦 : nat, 𝑥 : 𝛼 } ≤ {𝑥 : 𝛼, 𝑦 : nat} are true, but the two types
are not equal. Thus, a (strict) reflexivity rule employing syntactic equality is not adequate in suchcases. For record types it may be possible to avoid this issue by using a different representationin the abstract syntax. For instance, we could try to model record types instead as finite maps
from field names to types. Then equality of finite maps could have the expected properties forequality and a standard reflexivity rule could suffice. However, other type system features, such as
union (𝐴 ∨ 𝐵) and intersection types (𝐴 ∧ 𝐵) [Barbanera et al. 1995; Coppo et al. 1981; Pottinger
1980], would pose similar challenges. In those type systems we wish to have 𝐴 ∧ 𝐵 and 𝐵 ∧ 𝐴 to beequivalent types, for example. A change of representation of abstract syntax does not seem to help
for such features.
The reader may refer to work by Ligatti et al. [2017] for a more extended discussion on thecomplications of having the reflexivity rule built-in. We will also come back to this point in
Section 2.8.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:10

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Finding an algorithmic formulation: transitivity elimination is non-trivial. In the rules that Amadio
and Cardelli [1993] use, and assuming that equivalence in reflexivity is just alpha-equivalence,
simply dropping transitivity (rule OAmber-trans) to obtain an algorithmic formulation loses
expressive power. A simple example that illustrates this is:
𝛼 1 ≤ 𝛼 2, 𝛼 2 ≤ 𝛼 3 ⊢ 𝛼 1 ≤ 𝛼 2

𝛼 1 ≤ 𝛼 2, 𝛼 2 ≤ 𝛼 3 ⊢ 𝛼 2 ≤ 𝛼 3
does not hold!

𝛼 1 ≤ 𝛼 2, 𝛼 2 ≤ 𝛼 3 ⊢ 𝛼 1 ≤ 𝛼 3Such derivation is valid in a declarative formulation with transitivity, but invalid when transitivity
is dropped. Therefore, either the declarative specification must be changed to eliminate “invalid”
derivations, or the simply dropping transitivity will not work and some changes in the algorithmic
rules are necessary.
Proofs of transitivity and other lemmas are hard. A related problem is that proving transitivity ofan algorithmic formulation with Amber-style rules is hard. Surprisingly to us, despite the wide useof the Amber rules since 1985 for iso-recursive subtyping, there is very little work that describes
transitivity proofs. Many works simply avoid the problem by considering only declarative ruleswith transitivity built-in [Abadi and Cardelli 1996; Cardone 1991; Lee et al. 2015; Pottier 2013]. The
only proof that we are aware of for transitivity of an algorithmic formulation of the iso-recursive
Amber rules is by Bengtson et al. [2011]. Some researchers have tried, but failed, to formalize
this proof in Coq [Backes et al. 2014]. They found transitivity is hard to prove syntactically, as it
requires a “very complicated inductive argument”. Thus, they finally adopt the positive restriction,
as we discussed in Section 2.4. We also tried to directly prove some of these properties in Coq withvariations of the Amber rules, but none of them works properly.
Non-orthogonality of the Amber rules. Finally, the Amber rules interact with other subtyping
rules. Besides requiring reflexivity, they require a specific kind of entries in the typing environment,
which is different from typical entries in other subtyping relations. This affects other rules, and inparticular it affects the proofs for cases that are not related to recursive types. For instance this is a
key issue that we encountered when trying to prove transitivity and other properties. Furthermore,
it also affects implementations, since adding the Amber rules to an existing implementation ofsubtyping requires changing existing definitions and some cases of the subtyping algorithm. In
short, the Amber rules are not very modular: their addition has significant impact on existing
definitions, rules, implementations and, most importantly, proofs.
2.6 A New Declarative Specification for Iso-Recursive Subtyping
While the Amber rules are simple, as we have argued, there are important issues with the rules.
In particular developing the metatheory for the Amber rules is quite hard. As a first step towards
understanding the essence of the Amber rules we provide a new declarative specification of isorecursive subtyping in terms of finite unfoldings. We prove that the Amber rules are equivalent(sound and complete) with respect to this new formulation.
The key idea. The key idea of the new rules is inspired by the rules presented for covariant
subtyping in Section 2.3. The logic of the covariant rules is to approximate recursive subtyping
using what we call a 1-time finite unfolding. We say that the unfolding is finite because we simply
use 𝛼 instead of using the recursive type itself during unfolding. If we apply finite unfoldings to
all recursive types, we eventually end up having a comparison of two types representing finite
trees. The covariant rules work fine in a setting with covariant subtyping only, but are unsound ina setting that also includes contravariant subtyping. A plausible question is then: can we fix theserules to become sound in the presence of contravariant subtyping?
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:11

The answer to this question is yes! Let us have a second look at the unsound counter-example
that was presented in Section 2.3:
𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → ⊤As we have argued, this subtyping statement should fail because unfolding the recursive typetwice leads to an invalid subtyping statement. However, with the 1-time finite unfolding used by
the rules in Section 2.3, all that is checked is whether 𝛼 ⊢ 𝛼 → nat ≤ 𝛼 → ⊤ holds. Since suchstatement does hold, the rule unsoundly accepts 𝜇𝛼 . 𝛼 → nat ≤ 𝜇𝛼 . 𝛼 → ⊤. The problem is thatwhile the 1-time unfolding works, other 𝑛-times unfoldings do not. Therefore, an idea is to check
whether other 𝑛-times unfoldings work as well to recover soundness.
Declarative subtyping. Our declarative subtyping rules build on the previous observation andonly accept the subtyping relation between two recursive types if and only if all their 𝑛-times finite
unfoldings are subtypes for any positive integer 𝑛:Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐴] 𝑛 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝑛 𝐵Γ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵∀𝑛 = 1 · · · ∞S-RecIn comparison to the rules showed in Section 2.3, our subtyping rule S-rec has a stricter condition,by checking the subtyping relation for all 𝑛-times finite unfoldings, instead of only the 1-time finite
unfolding. Such restriction eliminates the false positives on contravariant recursive types. The
definition of 𝑛-times finite unfolding used in the rule is as follows:
Definition 1 (𝑛-times finite unfolding).
[𝛼 ↦→ 𝐴] 𝑛 𝐵 := [𝛼 ↦→ 𝐴] [𝛼 ↦→ 𝐴] · · · [𝛼 ↦→ 𝐴] 𝐵|{z}(𝑛−1) times

By definition, [𝛼 ↦→ 𝐴] 𝑛 𝐴 is the 𝑛-times finite unfolding of 𝜇𝛼 . 𝐴, but we use a slight generalization(mainly for proofs) to unfold a type 𝐵 with another type 𝐴 multiple times. For example, for therecursive type 𝜇𝛼 . nat → 𝛼, the one-time finite unfolding is nat → 𝛼 and the two times finite
unfolding is nat → nat → 𝛼. Note that the zero-times finite unfolding of a recursive type 𝜇𝛼 . 𝐴
would be the recursive type itself, according to our terminology. In our definition of 𝑛-times finite
unfolding we start counting from 1 and we apply the definition to the recursive type body (rather
than the recursive type itself). In other words, we execute (𝑛 − 1) times substitutions (where 𝑛corresponds to the arity of the finite unfolding) of the body of the recursive type to itself. For
example, [𝛼 ↦→ 𝐴] 1 𝐴 = 𝐴, [𝛼 ↦→ 𝐴] 2 𝐴 = [𝛼 ↦→ 𝐴] 𝐴, [𝛼 ↦→ 𝐴] 3 𝐴 = [𝛼 ↦→ 𝐴] [𝛼 ↦→ 𝐴] 𝐴, etc.
The counting scheme for the n-times finite unfolding definition may look at little odd. One may
expect the more natural looking definition where the body is unfolded 𝑛 times instead of 𝑛 − 1times. However, using 𝑛 times instead of 𝑛 − 1 would disagree with our terminology for finite
unfoldings of recursive types. For instance, the one-time unfolding of 𝜇𝛼 . nat → 𝛼 is nat → 𝛼, anddoes zero (not one!) substitutions in the body.
In rule S-rec, the number of times that the left and the right types are unfolded is exactly the same.
One may wonder if it makes sense to consider cases where we would unfold the recursive types adifferent number of types on the left and on the right. We believe that such approach would lead toa type unsound rule, and that it is important that the number of finite unfoldings is the same. For
instance, consider 𝜇𝛼 . nat → 𝛼 ≤ 𝜇𝛼 . nat → nat → ⊤. In this case if we choose to unfold the bodyof the left recursive type 𝑛 + 1 times and the body of the right recursive type only 𝑛 times (for all 𝑛)then we would get a valid subtyping statement. However, those two types should not be subtypes
since if we apply the unfolding lemma we would obtain: nat → (𝜇𝛼 . nat → 𝛼) ≤ nat → nat → ⊤.
The latter is not a valid subtyping statement.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:12

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

≤

→

≥

→

⊤

≥

→

⊤

⊤

≤

≥

→

→

≤

→

nat

≤

→

nat

nat
≤

...

→

...

Fig. 4. Tree model for equi-recursive subtyping.

Contrasting Equi and Iso-Recursive Types. It is useful to contrast the rule S-rec and its formulationin terms of finite unfoldings to Amadio and Cardelli’s specification of equi-recursive subtyping
in terms of infinite unfoldings of the recursive types. In Amadio and Cardelli’s work they use thenotion of finite approximation of a tree, which is closely related to the idea of finite unfoldings. A
simplified3 specification of equi-recursive subtyping in terms of subtyping of infinite trees can bereformulated in terms of finite unfoldings as:Γ ⊢ [𝛼 → 𝐴] ∞ 𝐴 ≤ [𝛼 → 𝐵] ∞ 𝐵
S-EqiΓ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵
Where the notation [𝛼 → 𝐴] ∞ 𝐴 denotes applying infinite substitutions to 𝐴. In other words, wedefine the equi-recursive comparison by just one comparison on the limit case, which will potentiallycompare two infinite trees. With rule S-Eqi subtyping statements such as 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat →𝛼 hold, just like with the rule S-rec for iso-recursive subtyping. However, unlike iso-recursive
subtyping, subtyping statements such as 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → nat → 𝛼 also hold, since weunfold both trees to the limit. Figure 4 visualizes the tree model equi-recursive subtyping. Notethat the figure applies to both 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → 𝛼 and 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → nat → 𝛼,since in both cases the infinite unfoldings of the trees in the subtyping statements are the same.
Instead of a single comparison in the limit case, the rule S-rec for iso-recursive subtyping requires
infinitely many comparisons, one for each 𝑛-time unfolding. For example, Figure 5 visualizes thecomparisons for 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → 𝛼 in the iso-recursive model. In the figure we show only
the first 3 comparisons, which would correspond to the 1-time, 2-times and 3-times finite unfoldings
respectively. However, there would be an infinite number of such comparisons for all 𝑛-times finite
unfoldings. Using rule S-rec the subtyping statement 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → nat → 𝛼 fails,
unlike in the equi-recursive model. It is easy to see why this is the case. Since rule S-rec requires
3 This definition is simplified because the rule S-Eqi compares only two recursive types. In general, in equi-recursive

formulations, any two types (recursive or not) can be unfolded and compared. For instance nat → (𝜇𝛼 . nat → 𝛼) ≤𝜇𝛼 . nat → 𝛼 should hold, since the infinite unfoldings of the two types are the same.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:13

≤

→

≥

⊤

→

≤

𝛼

𝛼

nat
(a) Rank-1 tree

≤

→

≥

→

⊤

→

≤

≥

⊤

→

nat

≤

𝛼

𝛼

nat
(b) Rank-2 tree

≤

→

≥

→

⊤

≥

→

⊤

⊤

→

≤

≤

≥

𝛼

→

nat

≤

→

nat

nat

𝛼

(c) Rank-3 tree
Fig. 5. Tree model for iso-recursive subtyping for the first 3 finite unfoldings for 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . 𝑛𝑎𝑡 → 𝛼.

that all comparisons are successful, to show that two recursive types are not subtypes it is enoughto show that one of the finite comparisons fails. For example, the comparison of one-time finite
unfoldings, which amounts to ⊤ → 𝛼 ≤ nat → nat → 𝛼, fails. Therefore, we can see that rule S-rec
rejects 𝜇𝛼 . ⊤ → 𝛼 ≤ 𝜇𝛼 . nat → nat → 𝛼.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:14

2.7

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Algorithmic Subtyping: Double and Nominal Unfoldings

An infinite amount of conditions is impossible to check algorithmically. Therefore, we must findalternative formulations that are algorithmic for implementations. As we will show, a suitable
formulation with iso-recursive Amber rules is equivalent to our declarative specification. Thus,
the Amber rules can in principle serve as a foundation for an implementation. However, there
are reasons to seek for alternative algorithmic rules. Most importantly, as we have argued in
Section 2.5, the Amber rules are hard to work with in proofs and metatheory. Therefore, to provide
a detailed account of the metatheory for iso-recursive subtyping we propose alternative algorithmic
definitions for subtyping of recursive types. The new formulations of subtyping have important
advantages over the Amber rules: the new rules are more modular; they do not require reflexivity
to be built-in; and transitivity and various other lemmas are easier to prove. Furthermore, we provethat the new rules are also equivalent with respect to the declarative specification of iso-recursive
subtyping and the Amber rules.
Double Unfoldings. It turns out that we only need to check 1-time and 2-times finite unfoldings
to obtain an algorithmic formulation that is sound, complete and decidable with respect to thedeclarative formulation of subtyping. We can informally explain why 1-time and 2-times finite
unfoldings are enough by looking again at the counter-example in Section 2.3. The 2-times finite
unfolding for the example is:𝛼 ⊢ (𝛼 → nat) → nat ≤ (𝛼 → ⊤) → ⊤When a recursive type variable in a negative position is unfolded twice, the types in the corresponding positive positions (i.e. the nat and ⊤) will now appear in both negative and positive
positions. In turn, the subtyping relation now has to check both that nat ≤ ⊤ (which is valid),and ⊤ ≤ nat (which is invalid). Thus, the 2-times finite unfolding fails. In general, more finite
unfoldings (3-times, 4-times, etc.) will only repeat the same checks that are done by the 1-time and2-times finite unfolding, thus not contributing anything new to the subtyping check. Thus, the rulethat we employ in the algorithmic formulation is the so-called double unfolding rule:
Γ, 𝛼 ⊢ 𝐴 ≤ 𝐵Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝐵
S-DoubleΓ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵
With this rule one may wonder if we can just check the 2-times finite unfolding (and do not
do the 1-time finite unfolding check). Unfortunately this would lead to an unsound rule, as thefollowing counter-example illustrates:
𝜇𝛼 . nat → 𝛼 ̸ ≤ 𝜇𝛼 . nat → nat → ⊤This statement should fail because it violates the unfolding lemma:
nat → (𝜇𝛼 . nat → 𝛼) ̸ ≤ nat → nat → ⊤But the 2-times finite unfolding for this example (nat → nat → 𝛼 ≤ nat → nat → ⊤) is a valid
subtyping statement! By checking only the 2-times finite unfolding, the subtyping statement iswrongly accepted. We must also check the 1-time finite unfolding (nat → 𝛼 ̸ ≤ nat → nat → ⊤),which fails and is the reason why the double unfolding rule rejects this example.
Nominal Unfoldings. The double unfolding rule is interesting because it directly relates to thedeclarative formulation using finite unfoldings. However, the double unfolding rules have exponential time complexity due to the two premises for both (1-time and 2-times) finite unfoldings.
At first, the 1-time finite unfolding appears unnecessary, since the 2-times unfolding seems to do
all the checks of the 1-time finite unfolding. Unfortunately, as our previous counter-example has
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:15

shown, the 1-time finite unfolding check cannot be avoided, due to some spurious subtyping thatexists when using only the 2-times finite unfolding. In an implementation, there are potentiallysome approaches to avoid the cost of the extra 1-time finite unfolding check. For example, we canstore the result of one-time finite unfolding during subtype checking, and reuse that result as partof subtype checking of the double unfoldings. This would avoid recomputation and lead to a more
efficient algorithm. However, it would be nicer to address this issue of the double unfoldings in theformalism itself.
For avoiding the 1-time finite unfolding in the double unfolding rule, we propose a variant of
the rule. Having understood the nature of the spurious subtyping problem that appeared in ourcounter-example using only 2-times finite unfoldings, the key idea to solve the problem is simple.
We track the name of the recursive variables during double unfoldings to avoid accidental subtyping.
Our approach is to add an extra label with the recursive variable name of the recursive type. This
regulates the structure of the derivation tree. Formally, our nominal unfolding rule is:Γ, 𝛼 ⊢ [𝛼 ↦→ {𝛼 : 𝐴}] 𝐴 ≤ [𝛼 ↦→ {𝛼 : 𝐵}] 𝐵
S-NominalΓ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵
Compared to the double unfolding rule, our nominal unfolding rule only has one premise. More
importantly, it avoids the spurious subtyping problem. In our new nominal unfolding rule, we do notneed the extra check for the one-time finite unfolding (checking Γ, 𝛼 ⊢ 𝐴 ≤ 𝐵). The derivation tree
below reflects the change for our simpler counter-example of the double unfolding rule (without
the extra one-time finite unfolding check):nat ≤ nat
{𝛼 : nat → 𝛼 } ≤ nat → ⊤ (fails!)
nat → {𝛼 : nat → 𝛼 } ≤ nat → nat → ⊤𝜇𝛼 . nat → 𝛼 ≤ 𝜇𝛼 . nat → nat → ⊤The presence of the extra label means that we now get {𝛼 : nat → 𝛼 } ≤ nat → ⊤ (which fails)
instead of nat → 𝛼 ≤ nat → ⊤ (which succeeds). In other words, the presence of the nominal label
avoids the need for the extra one-time finite unfolding check to rule out the counter-example.
Discussion. As we shall see, both the double and the nominal unfolding rules are easy to work within terms of proofs and metatheory, and the nominal unfolding rules can even simplify some proofs
due to the single premise. The double unfolding rule is directly inspired by the finite unfolding
specification. The nominal unfolding rule additionally employs the idea of tracking the recursivetype variable as a label to avoid spurious subtyping that arises from double unfoldings. Therefore,
it can avoid the extra 1-time finite unfolding check. In the nominal unfolding rule it is interesting
to observe that the names of recursive type variables play an important role, just as in the Amber
rules. However, in the Amber rules, we use distinct type variable names and track the subtyping
relation between those variables. In the nominal unfolding rule we use the same type variable
name, which is sufficient to identify types that originate from the double unfolding substitutions.
Therefore, spurious subtyping when using only double unfoldings can be avoided in the nominal
unfolding rule.
As a final remark, in follow up work to the work in this article, we have encountered somesettings where nominal unfolds and double unfoldings are not equivalent. In particular, in a settingwith intersection types 𝐴 ∧ 𝐵 [Barbanera et al. 1995; Coppo et al. 1981; Pottinger 1980], the nominal
unfolding rule works well, but the double unfolding rule accepts more subtyping statements, whichinvalidates the unfolding lemma. It appears that the issue is related to subtyping relations thatallow multiple ways to derive the same subtyping statement. In systems with intersection types,
for instance, there are multiple overlapping rules to deal with intersections. Therefore, in somesettings the nominal label seems to be not just useful to perform an optimization, but also to ensure
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:16

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

the correctness of subtyping. Nonetheless, we have not encountered any setting yet where thenominal unfolding rule does not work.
Some Final Implementation Considerations. The double unfolding and nominal unfolding rules areprimarily designed with the goal of leading to a simple metatheory and proofs. Both rules employ
substitutions which, if used directly in an implementation, have significant performance penalties.
To avoid substitutions one possibility would be to adopt explicit substitutions [Abadi et al. 1991],
which are a standard solution to avoid the performance penalties associated with substitutions.
Another possibility would be to adopt some ideas in the implementation approach proposed by
Ligatti et al. [2017]. Although Ligatti et al.’s rules have different expressive power compared to
the Amber rules and our rules, they also employ substitutions. They present an optimized 𝑂 (𝑚𝑛)algorithm that avoids the use of substitutions, and we believe that it should be possible to adopt
some of those ideas to implement double/nominal unfoldings. Finally, a simple optimization forboth double and nominal unfoldings is to avoid substitutions in positive positions. As Section 2.3
discusses for covariant subtyping using Γ ⊢ 𝐴 ≤ 𝐵 in the premise of the recursive subtyping rule issound. Thus, we should not need to substitute recursive type variables that are found in positive
positions, which avoids extra subtype checks of the substituted types. In other words, we could
have the variant (here for nominal unfoldings):
Γ, 𝛼 ⊢ [𝛼 ↦→ {𝛼 : 𝐴}] + 𝐴 ≤ [𝛼 ↦→ {𝛼 : 𝐵}] + 𝐵
S-Nominal+Γ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵
The idea is to employ a polarized form of substitution [𝛼 ↦→ 𝐴]𝑚 𝐵, which is parametrized by apositive (+) or negative (−) mode 𝑚. This form of substitution would only perform substitutions
at negative occurrences of type variables. Thus, the special case of covariant subtyping would
behave equivalently to the rule presented in Section 2.3. We leave the development and proof ofcorrectness for an efficient algorithm for future work.
2.8

A Calculus with Recursive Record Types

As an illustration of the advantages of our rules, in Section 6 we show an application to a calculus
with records and iso-recursive types.
In Section 2.5, we have discussed that the Amber rules cannot deal well with some formsof subtyping. In particular, the reflexivity rule is limiting when the subtyping relation is notantisymmetric. In the context of subtyping, antisymmetry is the property that if two types are both
subtypes of each other, then the two types are (syntactically) equal. More formally:Γ ⊢𝐴 ≤𝐵∧Γ ⊢𝐵 ≤𝐴⇒𝐴=𝐵
In simple subtyping relations, such as for instance a simply typed lambda calculus extended withthe top type and recursive types, this property holds. For instance, the calculus in Section 3 has anantisymmetric subtyping relation.
Unfortunately, many languages contain subtyping relations that are not antisymmetric. For
instance, if a language contains some form of record types (which includes essentially all OOP
languages), then the subtyping relation is not antisymmetric. In the example below, the subtyping
statement
𝜇𝛼 . {𝑥 : 𝛼, 𝑦 : nat} → nat ≤ 𝜇𝛼 . {𝑦 : nat, 𝑥 : 𝛼 } → natshould hold, since {𝑥 : 𝛼, 𝑦 : nat} and {𝑦 : nat, 𝑥 : 𝛼 } are subtypes of each other. However, the two
types are not syntactically equal. In such a setting, the use of the Amber rules would require that,instead of using syntactic equality in the reflexivity rule, we should use an equivalence relation on
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:17

types. However, we cannot simply define equivalence to be:Γ ⊢ 𝐴 ∼ 𝐵 := Γ ⊢ 𝐴 ≤ 𝐵 ∧ Γ ⊢ 𝐵 ≤ 𝐴
because then the reflexivity rule would become (by a simple unfolding of the equivalence definition):Δ⊢𝐴 ≤𝐵 Δ⊢𝐵 ≤𝐴
Amber-Refl-WrongΔ⊢𝐴 ≤𝐵
which would lead to a circular (and ill-behaved) subtyping relation. Instead, a separate equivalence
relation needs to be defined to ensure that record types are equivalent up-to permutation. But
adding such a separate relation on types would add complexity, since we would need a new set ofrules and theorems about such relation.
In contrast, with the double unfolding rules, because reflexivity is not built-in, we can simply
define the equivalence relation above (Γ ⊢ 𝐴 ∼ 𝐵) via subtyping. Thus, the double unfolding rules
do not require a separate definition of equivalence, and they also do not rely on the subtyping
relation being antisymmetric. The calculus in Section 6 illustrates the addition of records andrecords types to the calculus in Section 3. This addition has minimal impact of the calculus andmetatheory: the proof techniques are similar, except that instead of syntactic equality we use ourequivalence definition for types when proving the unfolding lemma.
3

A CALCULUS WITH SUBTYPING AND RECURSIVE TYPESIn this section we will introduce a full calculus with declarative subtyping and recursive types.
Our calculus is based on the simply typed lambda calculus extended with iso-recursive types andsubtyping. This declarative system captures the idea that, with iso-recursive types, two recursive
types are subtypes if all their finite unfoldings are subtypes. Notably we prove reflexivity, transitivity
and the unfolding lemma.
3.1

Syntax and Well-Formedness

Syntax. The calculus that we model is a simply typed lambda calculus with subtyping. The syntax
of types and contexts for this calculus is shown below.
Types
𝐴, 𝐵, 𝐶, 𝐷
Expressions 𝑒
Values𝑣
Contexts
Γ

F
F
F
F

nat | ⊤ | 𝐴1 → 𝐴2 | 𝛼 | 𝜇𝛼 . 𝐴
𝑥 | i | 𝑒 1 𝑒 2 | 𝜆𝑥 : 𝐴. 𝑒 | unfold [𝐴] 𝑒 | fold [𝐴] 𝑒i | 𝜆𝑥 : 𝐴. 𝑒 | fold [𝐴] 𝑣· | Γ, 𝛼 | Γ, 𝑥 : 𝐴

Meta-variables 𝐴, 𝐵, 𝐶, 𝐷 range over types. These types consist of: natural numbers (nat), thetop type (⊤), function types (𝐴 → 𝐵), type variables (𝛼) and recursive types (𝜇𝛼 . 𝐴). Expressions,denoted as 𝑒, include: term variables (𝑥), natural numbers (i), applications (𝑒 1 𝑒 2 ), lambda expressions(𝜆𝑥 : 𝐴. 𝑒). The expression unfold [𝐴] 𝑒 is used to unfold the recursive type of an expression 𝑒;
while fold [𝐴] 𝑒 is used to fold the recursive type of an expression 𝑒. Some expressions are also
values: natural numbers (i), lambda expressions (𝜆𝑥 : 𝐴. 𝑒) as well as fold expressions (fold [𝐴] 𝑣) if
their inner expressions are also values. The context is used to store variables with their type andtype variables.
Well-formedness. The definition of a well-formed environment ⊢ Γ is standard (Figure 6), ensuringthat all variables in the environment are distinct. In a well-formed environment, repetition ofvariables is not allowed and the order of variables are not important. Note that, throughout the
paper, we adopt the convention that variables are distinct. For instance, in rule wft-rec the 𝛼
introduced in Γ is distinct from other variables in Γ. In our Coq formalization the use of a locally
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:18

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira⊢Γ(Well-Formed Environment)
wfe-sub⊢Γ

wfe-empty

wfe-typ

𝛼∉Γ

⊢Γ

𝑥∉Γ

⊢ Γ, 𝛼⊢·Γ⊢A⊢ Γ, 𝑥 : AΓ⊢𝐴(Well-Formed Type)wft-varwft-arrowΓ ⊢ A1

wft-natwft-Top𝛼∈ΓΓ ⊢ natΓ⊢⊤Γ⊢𝛼

wft-recΓ ⊢ A2

Γ ⊢ A1 → A2Γ⊢𝐴 ≤𝐵S-nat

Γ ⊢ nat ≤ natΓ ⊢ 𝜇𝛼 . A(Declarative Subtyping)

S-var

S-top

⊢Γ

Γ, 𝛼 ⊢ A

⊢Γ

Γ⊢A

Γ⊢A≤⊤

⊢Γ

S-arrow𝛼∈ΓΓ⊢𝛼 ≤𝛼Γ ⊢ B1 ≤ A1

Γ ⊢ A2 ≤ B2

Γ ⊢ A1 → A2 ≤ B1 → B2

S-rec

Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐴] 𝑛 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝑛 𝐵∀𝑛 = 1 · · · ∞Γ ⊢ 𝜇𝛼 . A ≤ 𝜇𝛼 . B
Fig. 6. Well-formedness and subtyping rules.

nameless [Charguéraud 2011] encoding for binders makes such informal conventions precise. The
top of Figure 6 also shows the judgement for well-formed types. A type is well-formed if all of its
free variables are in the context. The rules of this judgement are mostly standard. The rule wft-recstates that if the body of a recursive type is well-formed under an extended context then therecursive type is well-formed.
3.2

Subtyping

The bottom of Figure 6 shows the declarative subtyping judgement. Our subtyping rules are standard
with the exception of the new rule for recursive types. Rule S-top states that any well-formed
type 𝐴 is a subtype of the ⊤ type. Rule S-var is a standard rule for type variables which are
introduced when unfolding recursive types: variable 𝛼 is a subtype of itself. The rule for function
types (rule S-arrow) is standard, but worth mentioning because it is contravariant on input types.
As illustrated in Section 2 (and various previous works), the interaction between recursive types
and contravariance has been a key difficulty in the development of subtyping with recursive types.
Finally, rule S-rec is the most significant: it tells us that a recursive type 𝜇𝛼 . 𝐴 is a subtype of 𝜇𝛼 . 𝐵,
if all their corresponding finite unfoldings are subtypes. Both [𝛼 ↦→ 𝐴] 𝑛 𝐴 and [𝛼 ↦→ 𝐵] 𝑛 𝐵 areused to denote 𝑛-times finite unfolding, as Definition 1 has illustrated.
3.3

Metatheory of Subtyping

The metatheory of the subtyping relation includes three essential properties: reflexivity, transitivity
and the unfolding lemma.
A better induction principle for subtyping properties. The first challenge that we face when looking
at the metatheory of subtyping with recursive types is to find adequate induction principles forvarious proofs. In particular the proofs of reflexivity and transitivity can be non-trivial without asuitable induction principle. A first idea to prove both reflexivity and transitivity is to use induction
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:19

on well-formed types. However, the problem of using this approach is that there is a mismatch
between the well-formedness and subtyping rules for recursive types. The induction hypothesisthat we get from rule wft-rec gives us a statement that works on 1-time finite unfoldings, whereas
in the subtyping rule we have a premise expressed in terms of all finite unfoldings.
Fortunately, we can define an alternative variant of well-formedness that gives us a better
induction principle. The idea is to replace rule wft-rec with a rule that expresses that if all finite
unfoldings of a recursive type are well-formed then the recursive type is well-formed.
Definition 2. Rule wft-inf is defined as:
wft-inf

Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐴] 𝑛 𝐴 ∀𝑛 = 1 · · · ∞Γ ⊢ 𝜇𝛼 . A
The two definitions of well-formedness are provably equivalent. In the proofs that follow, when weuse induction on well-formed types, we use the variant with the rule wft-inf.
Reflexivity and transitivity. Next we prove reflexivity and transitivity. First of all, we know that
subtyping is regular, i.e. subtyping implies well-formedness of context and types:
Lemma 3. Regularity: If Γ ⊢ 𝐴 ≤ 𝐵 then ⊢ Γ and Γ ⊢ 𝐴 and Γ ⊢ 𝐵.
Another important property of our subtyping rules is that the order of variables in contexts isirrelevant. That is we can always permute whole portions of the environment:
Lemma 4. If Γ1, Γ2, Γ3, Γ4 ⊢ 𝐴 ≤ 𝐵 then Γ1, Γ3, Γ2, Γ4 ⊢ 𝐴 ≤ 𝐵.
Thanks to our standard context, the proofs of both reflexivity and transitivity are straightforward using the variant of well-formedness with rule wft-inf. This contrasts with the Amber rules [Cardelli
1985], where reflexivity needs to be built-in and the proof of transitivity is quite complex (and hardto mechanize on a theorem prover) [Backes et al. 2014; Bengtson et al. 2011].
Theorem 5. Reflexivity.
If Γ ⊢ 𝐴 then Γ ⊢ 𝐴 ≤ 𝐴.
Theorem 6. Transitivity.
If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ 𝐵 ≤ 𝐶 then Γ ⊢ 𝐴 ≤ 𝐶.
Proof. From Lemma 3 we know all types and the environment are well-formed. Do inductionon Γ ⊢ 𝐵 (with the rule wft-inf).
• Rule wft-nat: Do inversion on both two subtyping statements, and we know that 𝐴 is nat
and 𝐶 is nat or ⊤.
• Rule wft-Top: Do inversion on Γ ⊢ ⊤ ≤ 𝐶, and we know that 𝐶 is ⊤.
• Rule wft-var: Do inversion on both two subtyping statements, and we know that 𝐴 is 𝛼 and𝐶 is 𝛼 or ⊤.
• Rule wft-arrow: Assume 𝐵 := 𝐵 1 → 𝐵 2 .
– Do inversion on Γ ⊢ 𝐵 1 → 𝐵 2 ≤ 𝐶, we know 𝐶 is ⊤ or 𝐶 := 𝐶 1 → 𝐶 2 . The former one issolved immediately. From the latter one, we obtain Γ ⊢ 𝐶 1 ≤ 𝐵 1 and Γ ⊢ 𝐵 2 ≤ 𝐶 2 .
– Do inversion on Γ ⊢ 𝐴 ≤ 𝐵 1 → 𝐵 2 , we know 𝐴 := 𝐴1 → 𝐴2 and obtain Γ ⊢ 𝐵 1 ≤ 𝐴1 andΓ ⊢ 𝐴2 ≤ 𝐵 2 .
– Now the goal is Γ ⊢ 𝐴1 → 𝐴2 ≤ 𝐶 1 → 𝐶 2 . Applying the arrow rule, what we need toprove are Γ ⊢ 𝐶 1 ≤ 𝐴1 and Γ ⊢ 𝐴2 ≤ 𝐶 2 . The two goals can be solved by the induction
hypotheses.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:20

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira• Rule wft-inf: Assume 𝐵 := 𝜇𝛼 . 𝐵 ′.
– Firstly, it is worthwhile stating the induction hypothesis that we get from rule wft-inf
explicitly: ∀𝑛 𝐴 𝐶, Γ, 𝛼 ⊢ 𝐴 ≤ [𝛼 ↦→ 𝐵 ′] 𝑛 𝐵 ′ ∧ Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐵 ′] 𝑛 𝐵 ′ ≤ 𝐶 ⇒ Γ, 𝛼 ⊢ 𝐴 ≤ 𝐶.
– Do inversion on Γ ⊢ 𝜇𝛼 . 𝐵 ′ ≤ 𝐶, we know 𝐶 is ⊤ or 𝐶 := 𝜇𝛼 . 𝐶 ′. The former one is solved
immediately. From the latter one, we obtain ∀𝑛, Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐵 ′] 𝑛 𝐵 ′ ≤ [𝛼 ↦→ 𝐶 ′] 𝑛 𝐶 ′.
– Do inversion on Γ ⊢ 𝐴 ≤ 𝜇𝛼 . 𝐵 ′, we know 𝐴 := 𝜇𝛼 . 𝐴 ′ and obtain ∀𝑛, Γ, 𝛼 ⊢ [𝛼 ↦→𝐴 ′] 𝑛 𝐴 ′ ≤ [𝛼 ↦→ 𝐵 ′] 𝑛 𝐵 ′.
– Now the goal is Γ ⊢ 𝜇𝛼 . 𝐴 ′ ≤ 𝜇𝛼 . 𝐶 ′. Applying the rule for recursive types, what we needto prove is ∀𝑛, Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐴 ′] 𝑛 𝐴 ′ ≤ [𝛼 ↦→ 𝐶 ′] 𝑛 𝐶 ′, which can be solved by the induction
hypothesis.
□
Modularity of the proofs. Note that in our transitivity proof, all the cases, except for the recursive
case, are standard and essentially the same as in a calculus without recursive types. In other words
the proof is modular in the sense that existing cases of the proof are not significantly affected by theaddition of recursive types. Other proofs, such as reflexivity or weakening, are similarly modular
in the same sense. Existing proofs for previous formulations of iso-recursive subtyping [Bengtson
et al. 2011; Ligatti et al. 2017] and in particular transitivity proofs are non-modular, and requiresignificant changes after the addition of recursive types. We discuss this in more detail in Section 8.
Unfolding lemma. Next, we turn to the unfolding lemma: if two recursive types are in a subtyping
relation, then substituting themselves into their bodies preserves the subtyping relation. Thislemma plays a crucial role in the proof of type preservation as we shall see in Section 3.5. However,the lemma cannot be proved directly: we need to prove a generalized lemma first.
Lemma 7. If(1) Γ1, 𝛼, Γ2 ⊢ 𝐴 ≤ 𝐵;
(2) Γ1, Γ2 ⊢ 𝜇𝛼 1 . 𝐶 and Γ1, Γ2 ⊢ 𝜇𝛼 1 . 𝐷;(3) 𝛼 does not occur free in 𝐶 and 𝐷;(4) Γ1, 𝛼, Γ2 ⊢ [𝛼 ↦→ 𝐶] 𝑛 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝑛 𝐵 holds for all 𝑛,then Γ1, Γ2 ⊢ [𝛼 ↦→ 𝜇𝛼 1 . 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 1 . 𝐷] 𝐵.
Proof. Induction on Γ1, 𝛼, Γ2 ⊢ 𝐴 ≤ 𝐵. Cases rules S-nat, S-top, and S-arrow are simple.
• Rule S-var. Assume that 𝐴 and 𝐵 are variable 𝛽. If 𝛽 ≠ 𝛼, then the goal is proven directly.
Otherwise, the fourth premise is Γ1, 𝛼, Γ2 ⊢ [𝛼 ↦→ 𝐶] 𝑛 𝛼 ≤ [𝛼 ↦→ 𝐷] 𝑛 𝛼, where 𝑛 is arbitrary.
The goal becomes Γ1, Γ2 ⊢ 𝜇𝛼 1 . 𝐶 ≤ 𝜇𝛼 1 . 𝐷. Then we can apply the rule for recursive types.
Note that in the context, the order of variables is unimportant (see Lemma 4) we can permute
the context without affecting the correctness. Therefore, the goal is equal to the fourthpremise after context permutation and alpha-conversion between 𝛼 1 and 𝛼, which is possible
due to the premise (3). Note also, that premise (3) can be derived from premise (2), but we
explicitly show it as a premise due to the role in the proof.
• Rule S-rec. Assume that the shape of 𝐴 is 𝜇𝛼 2 . 𝐴 ′ and the shape of 𝐵 is 𝜇𝛼 2 . 𝐵 ′.
– The fourth premise becomes ∀𝑛 ′, Γ1, 𝛼, Γ2 ⊢ [𝛼 ↦→ 𝐶] 𝑛 𝜇𝛼 2 . 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝑛 𝜇𝛼 2 . 𝐵 ′, which
can be rewritten to ∀𝑛 ′, Γ1, 𝛼, Γ2 ⊢ 𝜇𝛼 2 . [𝛼 ↦→ 𝐶] 𝑛 𝐴 ′ ≤ 𝜇𝛼 2 . [𝛼 ↦→ 𝐷] 𝑛 𝐵 ′.
– The goal becomes Γ1, Γ2 ⊢ [𝛼 ↦→ 𝜇𝛼 1 . 𝐶] 𝜇𝛼 2 . 𝐴 ′ ≤ [𝛼 ↦→ 𝜇𝛼 1 . 𝐷] 𝜇𝛼 2 . 𝐵 ′, which can be
rewritten to Γ1, Γ2 ⊢ 𝜇𝛼 2 . [𝛼 ↦→ 𝜇𝛼 1 . 𝐶] 𝐴 ′ ≤ 𝜇𝛼 2 . [𝛼 ↦→ 𝜇𝛼 1 . 𝐷] 𝐵 ′.
– If we apply rule S-rec to the goal, we get: ∀𝑛, Γ1, Γ2, 𝛼 2 ⊢ [𝛼 2 ↦→ ( [𝛼 ↦→ 𝜇𝛼 1 . 𝐶] 𝐴 ′)] 𝑛 ( [𝛼 ↦→𝜇𝛼 1 . 𝐶] 𝐴 ′) ≤ [𝛼 2 ↦→ ( [𝛼 ↦→ 𝜇𝛼 1 . 𝐷] 𝐵 ′)] 𝑛 ( [𝛼 ↦→ 𝜇𝛼 1 . 𝐷] 𝐵 ′).
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:21– We rewrite the goal above, getting: ∀𝑛, Γ1, Γ2, 𝛼 2 ⊢ [𝛼 ↦→ 𝜇𝛼 1 . 𝐶] [𝛼 2 ↦→ 𝐴 ′] 𝑛 𝐴 ′ ≤ [𝛼 ↦→𝜇𝛼 1 . 𝐷] [𝛼 2 ↦→ 𝐵 ′] 𝑛 𝐵 ′.
– The induction hypothesis is complex, so we write it here explicitly for readability of the′′proof: ∀𝑛, (∀𝑛 ′, Γ1, 𝛼, Γ2 ⊢ [𝛼 ↦→ 𝐶] 𝑛 [𝛼 2 ↦→ 𝐴 ′] 𝑛 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝑛 [𝛼 2 ↦→ 𝐵 ′] 𝑛 𝐵 ′) ⇒
′
𝑛
′
′
𝑛
′
Γ1, 𝛼 2, Γ2 ⊢ [𝛼 ↦→ 𝜇𝛼 1 . 𝐶] [𝛼 2 ↦→ 𝐴 ] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 1 . 𝐷] [𝛼 2 ↦→ 𝐵 ] 𝐵 .
– By applying context permutation and induction hypothesis to the goal, we get: ∀𝑛, ∀𝑛 ′, Γ1, 𝛼, Γ2 ⊢′′[𝛼 ↦→ 𝐶] 𝑛 [𝛼 2 ↦→ 𝐴 ′] 𝑛 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝑛 [𝛼 2 ↦→ 𝐵 ′] 𝑛 𝐵 ′, which can be proven by the inversion of fourth premise due to the fact that substitution is commutative.
□
Lemma 7 captures the idea of finite approximation. It relates the boundless unfolding with limited
unfolding. This lemma is a generalization of the unfolding lemma, and when 𝐴 = 𝐶 and 𝐵 = 𝐷, one
easily obtains the unfolding lemma.
Lemma 8. Unfolding Lemma.
If Γ ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then Γ ⊢ [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
3.4

Typing and Reduction Rules

Typing rules. As the top of Figure 7 shows, the typing rules are quite standard. Noteworthy are
the rules involving recursive types. Rule typing-unfold reveals that if 𝑒 has type 𝜇𝛼 . 𝐴 then, after
unfolding, its type becomes [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴. Rule typing-fold says if 𝑒 has type [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴,
after folding, its type becomes 𝜇𝛼 . 𝐴, with an additional type well-formedness check on 𝜇𝛼 . 𝐴. The
two constructs establish an isomorphism, which is used to deal with expressions with iso-recursive
types. The last rule is the standard subsumption rule (rule typing-sub).
Reduction. The bottom of Figure 7 shows the reduction rules, which are also quite standard.
We only focus on the last three rules involving recursive types. Rule step-fld cancels a pair of
unfold and fold. Note that the two types 𝐴 and 𝐵 are not necessarily the same. The last two rules(rule step-unfold and rule step-fold) simply reduce the inner expressions for unfold’s and fold’s.
3.5Type Soundness

In this subsection, we briefly illustrate how to prove type-soundness. The technique is mostly
conventional, except for the fundamental use of the unfolding lemma in the preservation proof(via Lemma 10). Firstly, we need a conventional substitution lemma to deal with beta reduction inpreservation:
Lemma 9. Substitution lemma. If Γ1, 𝑥 : 𝐵, Γ2 ⊢ 𝑒 : 𝐴 and Γ2 ⊢ 𝑒 ′ : 𝐵 then Γ1, Γ2 ⊢ [𝑥 ↦→ 𝑒 ′] 𝑒 : 𝐴.
Then we show how the unfolding lemma is used in the proof on type soundness, via an inversionof typing lemma for fold expressions:Lemma 10. Inversion of typing for fold expressions: If Γ ⊢ fold [𝐴] 𝑒 : 𝑆 and Γ ⊢ 𝑆 ≤ 𝜇𝛼 . 𝐵, then∃𝑇 , Γ ⊢ 𝑒 : [𝛼 ↦→ 𝜇𝛼 . 𝑇 ] 𝑇 ∧ Γ ⊢ [𝛼 ↦→ 𝜇𝛼 . 𝑇 ] 𝑇 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
Proof. Do induction on Γ ⊢ fold [𝐴] 𝑒 : 𝑆.
• Rule typing-fold: the premises become Γ ⊢ 𝑒 : [𝛼 ↦→ 𝜇𝛼 . 𝐴 ′] 𝐴 ′ (assume 𝐴 = 𝜇𝛼 . 𝐴 ′)and Γ ⊢ 𝜇𝛼 . 𝐴 ′ ≤ 𝜇𝛼 . 𝐵. In such situation, let 𝑇 = 𝐴 ′, we achieve the goal by applying theunfolding lemma (Lemma 8).
• Rule typing-sub: trivial by applying transitivity (Theorem 6).
□
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:22

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. OliveiraΓ ⊢𝑒 :𝐴(Typing)typing-nat

typing-var⊢Γ⊢Γ

typing-abs

𝑥 :𝐴∈Γ

Γ ⊢ i : nat

Γ, 𝑥 : A1 ⊢ e : A2

Γ⊢x:AΓ ⊢ 𝜆x : A1 . e : A1 → A2
typing-foldtyping-unfoldΓ ⊢ e : [𝛼 ↦→ 𝜇𝛼 . A] AΓ ⊢ e : 𝜇𝛼 . AΓ ⊢ unfold [𝜇𝛼 . A] e : [𝛼 ↦→ 𝜇𝛼 . A] AΓ ⊢ 𝜇𝛼 . AΓ ⊢ fold [𝜇𝛼 . A] e : 𝜇𝛼 . Atyping-app

typing-subΓ ⊢ e1 : A1 → A2

Γ ⊢ e2 : A1

Γ⊢e:AΓ ⊢ e1 e2 : A2

Γ⊢A≤B

Γ⊢e:B
(Reduction)𝑒 1 ↩→ 𝑒 2
step-appl
step-beta(𝜆x : A. e1 ) v2 ↩→ [𝑥 ↦→ v2 ] e1

step-appr

e1 ↩→ e1′e2 ↩→ e2′

e1 e2 ↩→ e1′ e2

v1 e2 ↩→ v1 e2′

step-unfold

step-folde ↩→ e′step-fld

unfold [A] (fold [B] v) ↩→ v

unfold [A] e ↩→ unfold [A] ee ↩→ e′′fold [A] e ↩→ fold [A] e′

Fig. 7. Typing and reduction rules.

Finally, we can proceed to the preservation and progress theorems, and the proof strategy is quite
standard.
Theorem 11. Preservation.
If Γ ⊢ 𝑒 : 𝐴 and 𝑒 ↩→ 𝑒 ′ then Γ ⊢ 𝑒 ′ : 𝐴.
Proof. By induction on Γ ⊢ 𝑒 : 𝐴. Most cases are trivial or standard, except for• Rule typing-unfold. In this case, 𝑒 is decomposed into unfold [𝜇𝛼 . 𝐴] 𝑒, and our goal is toprove Γ ⊢ 𝑒 ′ : [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴.
By inversion on unfold [𝜇𝛼 . 𝐴] 𝑒 ↩→ 𝑒 ′, we will get two sub-cases.
– The case for rule step-unfold is trivial: 𝑒 ′ continues to decompose into unfold [𝜇𝛼 . 𝐴] 𝑒 ′.
By applying rule typing-unfold and induction hypothesis, we achieve the goal.
– As for case involving rule step-fld, the first premise becomes Γ ⊢ fold [𝐴 ′] 𝑣 : 𝜇𝛼 . 𝐴. Then
we do the inversion on the first premise again, get two sub-cases. The first case is sameas the goal. The second case, raised by rule typing-sub, needs some extra work: what we
get now are Γ ⊢ fold [𝐴 ′] 𝑣 : 𝑆 and Γ ⊢ 𝑆 ≤ 𝜇𝛼 . 𝐴. Then we apply Lemma 10 (where theunfolding lemma is used) and rule typing-sub to achieve the goal.
□
Theorem 12. Progress.
If ⊢ 𝑒 : 𝐴 then 𝑒 is a value or exists 𝑒 ′, 𝑒 ↩→ 𝑒 ′ .
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:23

Γ ⊢𝑎 𝐴 ≤ 𝐵
SA-nat⊢ΓΓ ⊢a nat ≤ nat(Algorithmic Subtyping)SA-varSA-top

⊢Γ

⊢Γ

Γ⊢A

Γ ⊢a A ≤ ⊤SA-arrow𝛼∈ΓΓ ⊢a 𝛼 ≤ 𝛼Γ ⊢a B1 ≤ A1

Γ ⊢a A2 ≤ B2

Γ ⊢a A1 → A2 ≤ B1 → B2

SA-recΓ, 𝛼 ⊢a A ≤ BΓ, 𝛼 ⊢a [𝛼 ↦→ A] A ≤ [𝛼 ↦→ B] BΓ ⊢a 𝜇𝛼 . A ≤ 𝜇𝛼 . B

Fig. 8. Algorithmic subtyping.

4

ALGORITHMIC SUBTYPINGIn the last section we introduced a declarative formulation of subtyping with recursive types.
Unfortunately, such formulation is not directly implementable since the rule of subtyping forrecursive types checks against an infinite number of conditions (that all finite unfoldings are
subtypes). In this section, we first present two sound and complete algorithmic formulations ofsubtyping. This formulation replaces the declarative rule S-rec by rules based on double unfoldings.
A first rule, which we call the double unfolding rule, unfolds the recursive types 1-time and 2-times,
respectively. This double unfolding rule relates different other subtyping formulations in this paper,playing a significant role as a hub, as shown in Figure 1. We then give another algorithmic variant,using the nominal unfolding rule, and finally prove our subtyping rules for iso-recursive types are
decidable.
4.1

Syntax, Well-Formedness and Subtyping

The syntax and well-formedness of the algorithmic system share the same definitions as thedeclarative system presented in Section 3.
Well-Formedness. In the algorithmic version, we use Γ ⊢ 𝐴 to represent that 𝐴 is well-formed. The
rules of Γ ⊢ 𝐴 are the same as the top of Figure 6. Similarly to Section 3, we define an alternative
variant of well-formedness with the rule wft-recur to give us better induction principles for the
proofs.
Definition 13. Rule wft-recur is defined as:
wft-recur

Γ, 𝛼 ⊢ A

Γ, 𝛼 ⊢ [𝛼 ↦→ A] AΓ ⊢ 𝜇𝛼 . A

Subtyping. Figure 8 shows the algorithmic subtyping judgment. All the rules, except the one forrecursive types, remain the same as the declarative system. In algorithmic subtyping, rule SA-rec
states that two recursive types are subtypes when: 1) their bodies are subtypes; and 2) unfolding
the bodies one additional time preserves subtyping. In other words, checking 1-time and 2-times
finite unfoldings rather than all finite unfoldings is sufficient.
4.2

Reflexivity, Transitivity and CompletenessOur algorithmic subtyping simply relaxes the condition for recursive types while keeping the
judgment form. Therefore, regularity, reflexivity and transitivity are easy to prove using similar
techniques to those used in the declarative system.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:24

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Lemma 14. Regularity: If Γ ⊢𝑎 𝐴 ≤ 𝐵 then ⊢ Γ and Γ ⊢ 𝐴 and Γ ⊢ 𝐵.
Theorem 15. Reflexivity.
If Γ ⊢ 𝐴 then Γ ⊢𝑎 𝐴 ≤ 𝐴.
Theorem 16. Transitivity.
If Γ ⊢𝑎 𝐴 ≤ 𝐵 and Γ ⊢𝑎 𝐵 ≤ 𝐶 then Γ ⊢𝑎 𝐴 ≤ 𝐶.
Note that, like the declarative system (and unlike the Amber rules), the transitivity proof is very
simple with the double unfolding rule. The completeness of algorithmic subtyping is obvious, since
the declarative system has the same conditions of the algorithmic system (plus a few more).
Theorem 17. Completeness of algorithmic subtyping.
If Γ ⊢ 𝐴 ≤ 𝐵 then Γ ⊢𝑎 𝐴 ≤ 𝐵.
4.3

Soundness

The real challenge is the soundness of the algorithmic specification with respect to the declarative
system. For soundness, we wish to prove that:
If Γ ⊢𝑎 𝐴 ≤ 𝐵 then Γ ⊢ 𝐴 ≤ 𝐵.
The key problem is to show that finitely unfolding only one and two times is sufficient toguarantee that all finite unfoldings are sound. Although it is easy to give an informal argument as
to why this is the case, as we did in Section 2, formalizing this argument is a whole different matter.
Finding the right generalization for soundness. The key idea to prove that 1-time and 2-times finite
unfolding implies 𝑛-times finite unfolding is to capture this informal idea formally as a lemma:Γ ⊢ 𝐴 ≤ 𝐵 ∧ Γ ⊢ [𝛼 ↦→ 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝐵 ⇒ Γ ⊢ [𝛼 ↦→ 𝐴] 𝑛 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝑛 𝐵.
As we shall see this lemma is true but, unfortunately, it cannot be proved directly. The obvious
attempt would be to do induction on Γ ⊢ 𝐴 ≤ 𝐵. The essential problem with such an approach isthat we wish to analyze the different subcases for 𝐴 and 𝐵, but we still want to use the original
𝐴 and 𝐵 in the substitutions. For instance, suppose that we have 𝐴 := nat → 𝐴1 → 𝐴2 and𝐵 := nat → 𝐵 1 → 𝐵 2 . Here 𝐴1 → 𝐴2 and 𝐵 1 → 𝐵 2 are contained in the type 𝐴 and 𝐵. Now
consider the case for function types Γ ⊢ 𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2 , which would occur as a subcase in
the proof. What we would like to have is the conclusionΓ ⊢ [𝛼 ↦→ 𝐴] 𝑛 (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝐵] 𝑛 (𝐵 1 → 𝐵 2 )However, what we get instead isΓ ⊢ [𝛼 ↦→ (𝐴1 → 𝐴2 )] 𝑛 (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ (𝐵 1 → 𝐵 2 )] 𝑛 (𝐵 1 → 𝐵 2 )In other words, what gets substituted are not the original types 𝐴 and 𝐵, but only a part of those
types (𝐴1 → 𝐴2 and 𝐵 1 → 𝐵 2 ) that is being considered by the current case. Therefore, it is clearthat we need some generalization of this lemma. A first idea is to generalize it as follows:⇒Γ ⊢ 𝐴 ≤ 𝐵 ∧ Γ ⊢ 𝐶 ≤ 𝐷 ∧ Γ ⊢ [𝛼 ↦→ 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝐵Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝑛 𝐵.

Now it is possible to do induction on Γ ⊢ 𝐴 ≤ 𝐵 without affecting the substituted types. However,this lemma is false. A counter-example is:⇏Γ ⊢ ⊤ → 𝛼 ≤ nat → 𝛼 ∧ Γ ⊢ 𝛼 → nat ≤ 𝛼 → ⊤∧ Γ ⊢ ⊤ → 𝛼 → nat ≤ nat → 𝛼 → ⊤Γ ⊢ ⊤ → (𝛼 → nat) → nat ≤ nat → (𝛼 → ⊤) → ⊤.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:25

In this counter-example we choose 𝑛 = 2. All the premises are satisfied, but the conclusion is false.
Note that in the conclusion, because of the contravariance of function subtyping, we eventuallyrequire that Γ ⊢ 𝛼 → ⊤ ≤ 𝛼 → nat, which is clearly false.
By further analyzing the counter-example, we can see that the influence of contravariance onvariables is not reflected in such a lemma. Therefore, our generalized soundness lemma should deal
with type variables at contravariant positions and covariant positions respectively, but under thesame pattern. In other words we need a pair of lemmas: one to deal with covariance, and anotherto deal with contravariance.
The generalized lemma. Learning from the lessons of the failed attempts at soundness we reachto the following lemma, which holds:
Lemma 18. If,(1) Γ ⊢ 𝐴 ≤ 𝐵;
(2) Γ ⊢ 𝐶 ≤ 𝐷;(3) Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛 𝐶 ≤ [𝛼 ↦→ 𝐷] 𝑛 𝐷.
then(1) Γ ⊢ [𝛼 ↦→ 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝐵 implies Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛+1 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 and(2) Γ ⊢ [𝛼 ↦→ 𝐷] 𝐴 ≤ [𝛼 ↦→ 𝐶] 𝐵 implies Γ ⊢ [𝛼 ↦→ 𝐷] 𝑛+1 𝐴 ≤ [𝛼 ↦→ 𝐶] 𝑛+1 𝐵.
Proof. By induction on Γ ⊢ 𝐴 ≤ 𝐵.
• Case rule S-var: In such case 𝐴 = 𝐵 = 𝛽. If 𝛽 ≠ 𝛼, we prove the goal trivially. Otherwise,★ Goal (1): We want to prove Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛 𝐶 ≤ [𝛼 ↦→ 𝐷] 𝑛 𝐷, which can be obtained frompremise (3).
★ Goal (2), We have premises Γ ⊢ 𝐶 ≤ 𝐷 by premise (2) and Γ ⊢ 𝐷 ≤ 𝐶 from the condition ofgoal (2), thus 𝐶 = 𝐷 by Lemma 19. Goal (2) is proven by reflexivity.
• Case rule S-arrow: In such case 𝐴 = 𝐴1 → 𝐴2 and 𝐵 = 𝐵 1 → 𝐵 2 .
★ Goal (1): We need to prove Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛+1 (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝐷] 𝑛+1 (𝐵 1 → 𝐵 2 ), which
can be rewritten as Γ ⊢ ( [𝛼 ↦→ 𝐶] 𝑛+1 𝐴1 ) → ( [𝛼 ↦→ 𝐶] 𝑛+1 𝐴2 ) ≤ ( [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 1 ) →( [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 2 ). By applying rule S-arrow, we need to prove Γ ⊢ [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 1 ≤[𝛼 ↦→ 𝐶] 𝑛+1 𝐴1 and Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛+1 𝐴2 ≤ [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 2 . The former one can be provedby using the induction hypothesis arising from goal (2), while the latter one can be provedby using the induction hypothesis arising from goal (1).
★ Goal (2): We need to prove Γ ⊢ [𝛼 ↦→ 𝐷] 𝑛+1 (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝐶] 𝑛+1 (𝐵 1 → 𝐵 2 ), which
can be rewritten as Γ ⊢ ( [𝛼 ↦→ 𝐷] 𝑛+1 𝐴1 ) → ( [𝛼 ↦→ 𝐷] 𝑛+1 𝐴2 ) ≤ ( [𝛼 ↦→ 𝐶] 𝑛+1 𝐵 1 ) →( [𝛼 ↦→ 𝐶] 𝑛+1 𝐵 2 ). By applying rule S-arrow, we need to prove Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛+1 𝐵 1 ≤[𝛼 ↦→ 𝐷] 𝑛+1 𝐴1 and Γ ⊢ [𝛼 ↦→ 𝐷] 𝑛+1 𝐴2 ≤ [𝛼 ↦→ 𝐶] 𝑛+1 𝐵 2 . The former one can be provedby using the induction hypothesis arising from goal (1), while the latter one can be provedby using the induction hypothesis arising from goal (2).
• Case rule S-rec: Now we assume 𝐴 = 𝜇𝛼 ′ . 𝐴 ′ and 𝐵 = 𝜇𝛼 ′ . 𝐵 ′. Since in such case, we do notneed to consider the contravariance, we will just show how to prove goal (1). Goal (2) can beproved using the same approach.
– The condition arising from the goal (1) becomes Γ ⊢ [𝛼 ↦→ 𝐶] 𝜇𝛼 ′ . 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝜇𝛼 ′ . 𝐵 ′,which can be rewritten as Γ ⊢ 𝜇𝛼 ′ . [𝛼 ↦→ 𝐶] 𝐴 ′ ≤ 𝜇𝛼 ′ . [𝛼 ↦→ 𝐷] 𝐵 ′.
′– After inversion, we get ∀𝑛 ′, Γ ⊢ [𝛼 ′ ↦→ ( [𝛼 ↦→ 𝐶] 𝐴 ′)] 𝑛 [𝛼 ↦→ 𝐶] 𝐴 ′ ≤ [𝛼 ′ ↦→ ( [𝛼 ↦→′′𝐷)] 𝐵 ′] 𝑛 [𝛼 ↦→ 𝐷] 𝐵 ′, which can be rewritten as ∀𝑛 ′, Γ ⊢ [𝛼 ↦→ 𝐶] [𝛼 ′ ↦→ 𝐴 ′] 𝑛 𝐴 ′ ≤ [𝛼 ↦→′𝐷] [𝛼 ′ ↦→ 𝐵 ′] 𝑛 𝐵 ′.
– The goal now is Γ ⊢ [𝛼 ↦→ 𝐶] 𝑛+1 𝜇𝛼 ′ . 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝑛+1 𝜇𝛼 ′ . 𝐵 ′, which can be rewritten asΓ ⊢ 𝜇𝛼 ′ . [𝛼 ↦→ 𝐶] 𝑛+1 𝐴 ′ ≤ 𝜇𝛼 ′ . [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 ′.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:26

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira′– Applying rule S-rec on the goal, we get ∀𝑛 ′, Γ, 𝛼 ′ ⊢ [𝛼 ′ ↦→ ( [𝛼 ↦→ 𝐶] 𝑛+1 𝐴 ′)] 𝑛 [𝛼 ↦→′𝐶] 𝑛+1 𝐴 ′ ≤ [𝛼 ′ ↦→ ( [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 ′)] 𝑛 [𝛼 ↦→ 𝐷] 𝑛+1 𝐵 ′, which can be rewritten as
′
′
′
′
𝑛+
1
′
′
𝑛
′
∀𝑛 , Γ, 𝛼 ⊢ [𝛼 ↦→ 𝐶] [𝛼 ↦→ 𝐴 ] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝑛+1 [𝛼 ′ ↦→ 𝐵 ′] 𝑛 𝐵 ′.
– Finally, we apply the induction hypothesis, to prove goal (1).
□Compared with our last failed attempt, there is an extra condition (condition 3). More importantly,
there are now two conclusions. These conclusions basically express two different lemmas. One
lemma, with all the conditions and conclusion (1), and another lemma with all conditions andconclusion (2). Conclusion (1) covers covariant uses of the lemma, whereas conclusion (2) covers
contravariant uses of the lemma. Note that when we apply the lemma in our soundness theorem,
we have that 𝐴 = 𝐶 and 𝐵 = 𝐷. Those types will then become different as the subcases of type 𝐴
and 𝐵 are processed. For covariant cases, 𝐴 is a portion of the type 𝐶, and 𝐵 is a portion of the type
𝐷. Conclusion (1) covers this, and we can see that we are substituting 𝐶 in 𝐴 and 𝐷 in 𝐵. However,the contravariance of function types will flip the input types being checked for subtyping. Thismeans that in effect, 𝐴 is now a portion of 𝐷 (in a contravariant position in 𝐷) and 𝐵 is a portion of
𝐶 (in a contravariant position in 𝐶). Goal (2) captures such nuance and provides a formulation forthe lemma that deals with subparts of 𝐶 and 𝐷, which are in contravariant positions.
The proof of Lemma 18 relies on the following property of the subtyping relation:
Lemma 19. Antisymmetry of declarative subtyping: If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ 𝐵 ≤ 𝐴 then 𝐴 = 𝐵.
Also, from Lemma 18, we now can prove:
Lemma 20. If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ [𝛼 ↦→ 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝐵, then ∀𝑛, Γ ⊢ [𝛼 ↦→ 𝐴] 𝑛 𝐴 ≤ [𝛼 ↦→𝐵] 𝑛 𝐵.
Proof. Do induction on 𝑛. For the base case, we simply apply the premise (1). For the induction
case, we apply Lemma 18 with 𝐶 = 𝐴 and 𝐷 = 𝐵, then apply induction hypothesis.
□
The form of Lemma 20 is close to the shape of the infinite unfolding rule (rule S-rec) for recursive
types. Finally, we can prove the soundness theorem:
Theorem 21. Soundness of algorithmic subtyping.
If Γ ⊢𝑎 𝐴 ≤ 𝐵 then Γ ⊢ 𝐴 ≤ 𝐵.
4.4

The Unfolding Lemma for the Double Unfolding Rules

In Section 3, we showed how to prove the unfolding lemma for the declarative system. It turns
out that the unfolding lemma can also be proved relatively easily for the algorithmic system using
a technique similar to that employed in the proof of soundness in Section 4.3. A direct proof of
the unfolding lemma is useful for language designers wishing to skip the declarative system, andformulate only an algorithmic version.
Lemma 18 provides an interesting (and necessary) lemma for proving soundness between double
and finite unfoldings. For that lemma a key insight is that we need two forms: one for dealing with
contravariant cases, and another to deal with covariant cases. Inspired by this insight, we are able
to prove the unfolding lemma directly for the double unfolding rules, using a similar technique.
Firstly we need a lemma similar to Lemma 19, but for the algorithmic relation:
Lemma 22. Antisymmetry of algorithmic subtyping: If Γ ⊢𝑎 𝐴 ≤ 𝐵 and Γ ⊢𝑎 𝐵 ≤ 𝐴 then 𝐴 = 𝐵.
Then we can formulate the generalized lemma that is needed to prove the unfolding lemma as
follows:
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:27

Lemma 23. If(1) Γ1, 𝛼, Γ2, ⊢𝑎 𝐴 ≤ 𝐵;
(2) Γ1, 𝛼, Γ2, ⊢𝑎 𝐶 ≤ 𝐷;(3) Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤ 𝜇𝛼 . 𝐷;then(1) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝐵 implies Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 and(2) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐷] 𝐴 ≤ [𝛼 ↦→ 𝐶] 𝐵 implies Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐵.
Proof. Note that premise (2) can be obtained by inversion of premise (3). We explicitly show ithere just for convenience. The whole proof follows a similar structure to Lemma 18: we proceed byinduction on Γ1, 𝛼, Γ2 ⊢𝑎 𝐴 ≤ 𝐵.
• Case rule SA-var: In such case 𝐴 = 𝐵 = 𝛽. If 𝛽 ≠ 𝛼, we simply achieve the goal.
Otherwise,★ Goal (1): We want to prove Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤ 𝜇𝛼 . 𝐷, which is actually premise (3).
★ Goal (2): From the condition of goal (2), we have Γ1, 𝛼, Γ2, ⊢𝑎 𝐷 ≤ 𝐶, which is the inverse ofpremise (2). Thus, we get 𝐶 = 𝐷 by Lemma 22. Goal (2) is proven by reflexivity.
• Case rule SA-arrow: In such case 𝐴 = 𝐴1 → 𝐴2 and 𝐵 = 𝐵 1 → 𝐵 2 .
★ Goal (1):− We need to prove Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] (𝐵 1 → 𝐵 2 ),which can be rewritten as Γ1, Γ2 ⊢𝑎 ( [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴1 ) → ( [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴2 ) ≤ ( [𝛼 ↦→𝜇𝛼 . 𝐷] 𝐵 1 ) → ( [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 2 ).
− By applying rule SA-arrow, we need to prove Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 1 ≤ [𝛼 ↦→𝜇𝛼 . 𝐶] 𝐴1 and Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴2 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 2 .
− The former one can be proved by using induction hypothesis arising from goal (2), while
the latter one can be proved by using induction hypothesis arising from goal (1).
★ Goal (2):− We need to prove Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐷] (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐶] (𝐵 1 → 𝐵 2 ),which can be rewritten as Γ1, Γ2 ⊢𝑎 ( [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐴1 ) → ( [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐴2 ) ≤ ( [𝛼 ↦→𝜇𝛼 . 𝐶] 𝐵 1 ) → ( [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐵 2 ).
− By applying rule SA-arrow, we need to prove Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐵 1 ≤ [𝛼 ↦→𝜇𝛼 . 𝐷] 𝐴1 and Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐴2 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐵 2 .
− The former one can be proved by using induction hypothesis arising from goal (1), while
the latter one can be proved by using induction hypothesis arising from goal (2).
• Case rule SA-rec: Now we assume 𝐴 = 𝜇𝛼 ′ . 𝐴 ′ and 𝐵 = 𝜇𝛼 ′ . 𝐵 ′. Since in such case, we do
not need to consider the contravariance, we will just show how to prove goal (1). Goal (2)can be proven with the same approach.
– The goal now is Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝜇𝛼 ′ . 𝐴 ′ ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝜇𝛼 ′ . 𝐵 ′, which can be
rewritten as Γ1, Γ2 ⊢𝑎 𝜇𝛼 ′ . [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ′ ≤ 𝜇𝛼 ′ . [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 ′.
– The condition arising from the goal (1) becomes Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐶] 𝜇𝛼 ′ . 𝐴 ′ ≤ [𝛼 ↦→𝐷] 𝜇𝛼 ′ . 𝐵 ′, which can be rewritten as Γ1, 𝛼, Γ2 ⊢𝑎 𝜇𝛼 ′ . [𝛼 ↦→ 𝐶] 𝐴 ′ ≤ 𝜇𝛼 ′ . [𝛼 ↦→ 𝐷] 𝐵 ′.
– Do inversion on this condition and reorder the context and substitution, we get two new
conditions: Γ1, 𝛼, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝐵 ′ and Γ1, 𝛼, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝐶] [𝛼 ′ ↦→𝐴 ′] 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] [𝛼 ′ ↦→ 𝐵 ′] 𝐵 ′.
– Because of the double unfolding rule, we will have two induction hypotheses, which are★ I.H.(1), which comes from 1-time unfolding : Γ1, 𝛼, Γ2, ⊢𝑎 𝐶 ≤ 𝐷 ⇒ Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤𝜇𝛼 . 𝐷 ⇒ Γ1, 𝛼, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] 𝐵 ′ ⇒ Γ1, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ′ ≤[𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 ′.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:28

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira★ I.H.(2), which comes from 2-times unfolding : Γ1, 𝛼, Γ2, ⊢𝑎 𝐶 ≤ 𝐷 ⇒ Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤𝜇𝛼 . 𝐷 ⇒ Γ1, 𝛼, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝐶] [𝛼 ′ ↦→ 𝐴 ′] 𝐴 ′ ≤ [𝛼 ↦→ 𝐷] [𝛼 ′ ↦→ 𝐵 ′] 𝐵 ′ ⇒ Γ1, Γ2, 𝛼 ′ ⊢𝑎[𝛼 ↦→ 𝜇𝛼 . 𝐶] [𝛼 ′ ↦→ 𝐴 ′] 𝐴 ′ ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] [𝛼 ′ ↦→ 𝐵 ′] 𝐵 ′.
– Apply rule SA-rec on the goal, we obtain two sub-goals: Γ1, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ′ ≤[𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 ′ and Γ1, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ′ ↦→ ( [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ′)] [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ′ ≤ [𝛼 ′ ↦→( [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 ′)] [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 ′.
– For the former one, we apply the I.H.(1). As for the latter one, after rewriting the goal toΓ1, Γ2, 𝛼 ′ ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] [𝛼 ′ ↦→ 𝐴 ′] 𝐴 ′ ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] [𝛼 ′ ↦→ 𝐵 ′] 𝐵 ′, we apply the I.H.(2).
□Like Lemma 18, in Lemma 23 the two conclusions are basically reflecting two lemmas: one forcovariant uses (when 𝐴 is a part of 𝐶 and 𝐵 is a part of 𝐷), and another for contravariant uses
(when 𝐴 is a part of 𝐷 and 𝐵 is a part of 𝐶). By letting 𝐶 := 𝐴, 𝐷 := 𝐵, we easily obtain:
Lemma 24. Unfolding Lemma.
If Γ ⊢𝑎 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then Γ ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
4.5

Nominal Unfoldings

In this subsection, we will describe the nominal unfolding rule, which is another algorithmic variant
equivalent to declarative subtyping. Compared with the double unfolding rules, nominal unfoldings
have better efficiency (since only one premise is needed), while eliminating spurious subtyping
derivations that arise with double unfoldings (see example in Section 2.7).
Syntax and well-formedness. The syntax of contexts for this calculus is the same as Section 3.
For the syntax of types, based on the syntax in Section 3, we extend it with labelled types {𝛼 : 𝐴}.
Labelled types can be viewed as a simple form of nominal types. They are essentially a pair that
contains a name (or type variable) 𝛼 and a type.
The well-formedness Γ ⊢ 𝐴 is also defined as Section 3, but for recursive types and labelledtypes (the top of Figure 9). To get a better induction hypothesis, we slightly modify the form ofwell-formed recursive types, as rule wft-nominal shows. As before, rule wft-nominal is provento be equivalent to rule wft-rec. The first premise Γ, 𝛼 ⊢ 𝐴 might appear redundant at first glance,
but it is indeed necessary, because from the second premise Γ, 𝛼 ⊢ [𝛼 ↦→ {𝛼 : 𝐴}] 𝐴, we cannot
derive Γ, 𝛼 ⊢ 𝐴, which is the insurance with respect to the correctness of substitution during theproof. Meanwhile, since we introduce labelled types, as rule wft-label shows, a labelled type iswell-formed if its inner type is well-formed.
Subtyping. The bottom of Figure 9 shows the definition of subtyping with the nominal unfolding
rule. We denote subtyping for nominal unfoldings as Γ ⊢𝑛 𝐴 ≤ 𝐵. Rules SN-nat, SN-top, SN-var,
and SN-arrow are the same as the corresponding double unfolding subtyping rules. Rule SN-rcd
is new, stating that a labelled type is a subtype of another labelled type if the two types are labelledwith the same name and 𝐴 ≤ 𝐵.
Rule SN-rec, the nominal unfolding rule, is the most interesting one. This rule follows an idea
quite similar to the double unfolding rule. The body of the recursive type is unfolded twice. However,for the innermost unfolding, the type that we substitute is not the type of the body directly. Instead,
we use a labelled type, where the label has the same name as the recursive variable 𝛼, and thetype that is labelled is the body of the recursive type. In other words, instead of using the double
unfolding [𝛼 ↦→ 𝐴] 𝐴 we use [𝛼 ↦→ {𝛼 : 𝐴}] 𝐴. The label is crucial to avoid spurious subtyping
derivations, and it is also the reason why in the nominal unfolding formulation we do not need tocheck the subtyping of single unfoldings as well. In the double unfolding rule, there is an extra
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:29

Γ⊢𝐴

(Well-Formed Type, Selected Rules)
wft-label

wft-nominalΓ⊢AΓ, 𝛼 ⊢ A

Γ, 𝛼 ⊢ [𝛼 ↦→ {𝛼 : A}] AΓ ⊢ {𝛼 : A}Γ ⊢ 𝜇𝛼 . AΓ ⊢𝑛 𝐴 ≤ 𝐵(Nominal Subtyping)SN-natSN-varSN-top⊢Γ⊢ΓΓ ⊢𝑛 nat ≤ natΓ⊢AΓ ⊢𝑛 A ≤ ⊤⊢ΓSN-arrow𝛼∈ΓΓ ⊢𝑛 𝛼 ≤ 𝛼Γ ⊢𝑛 B1 ≤ A1

Γ ⊢𝑛 A2 ≤ B2

Γ ⊢𝑛 A1 → A2 ≤ B1 → B2
SN-rcdSN-recΓ, 𝛼 ⊢𝑛 [𝛼 ↦→ {𝛼 : A}] A ≤ [𝛼 ↦→ {𝛼 : B}] BΓ ⊢𝑛 A ≤ BΓ ⊢𝑛 𝜇𝛼 . A ≤ 𝜇𝛼 . BΓ ⊢𝑛 {𝛼 : A} ≤ {𝛼 : B}

Fig. 9. Well-formedness and subtyping rules for nominal unfoldings.

premise that checks the single unfolding and prevents certain cases of spurious subtyping. The
absence of this extra premise also makes some of the metatheory simpler.
Basic properties. All the proofs about reflexivity, transitivity and unfolding lemma for nominal
unfoldings are almost the same as double unfoldings, since both subtyping rules are based on twotimes finite unfoldings. We list all the theorems here and skip the details (the reader can consult
our mechanized proofs for full details).
Theorem 25. Reflexivity.
If Γ ⊢ 𝐴 then Γ ⊢𝑛 𝐴 ≤ 𝐴.
Theorem 26. Transitivity.
If Γ ⊢𝑛 𝐴 ≤ 𝐵 and Γ ⊢𝑛 𝐵 ≤ 𝐶 then Γ ⊢𝑛 𝐴 ≤ 𝐶.
Lemma 27. Unfolding Lemma.
If Γ ⊢𝑛 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then Γ ⊢𝑛 [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
Another important property is that, from the nominal unfolding rules, we can derive 1-time
finite unfoldings. This lemma is important to show that nominal unfoldings subsume the double
unfolding rule:Lemma 28. If Γ, 𝛼 ⊢𝑛 [𝛼 ↦→ {𝛼 : 𝐴}] 𝐴 ≤ [𝛼 ↦→ {𝛼 : 𝐵}] 𝐵 then Γ, 𝛼 ⊢𝑛 𝐴 ≤ 𝐵.
4.6

Equivalence between Nominal Unfoldings and Double Unfoldings

The subtyping relation presented in Section 4.5 is equivalent to a subtyping relation that uses
the double unfolding rules for recursive types. This equivalence is not surprising, since nominal
unfoldings are essentially the double unfolding rule with an extra label and without the one time
finite unfolding premise. Lemma 28 and some other similar auxiliary lemmas are used to formulate
the equivalence between the two encodings. The most interesting aspect of the equivalence proofis that we need to translate types for the nominal unfolding formulation into types of the doubleunfolding formulation. Such a translation is necessary because nominal unfoldings require labelledtypes, which do not exist in the double unfolding formulation. Thus, the translation simply erases
the labels.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:30

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Definition 29. The erase (↘) function is defined as:
nat↘
=
nat
⊤↘
=
⊤
𝛼↘
=
𝛼
(𝐴 → 𝐵)↘ = 𝐴↘ → 𝐵 ↘
(𝜇𝛼 . 𝐴)↘ =𝜇𝛼 . 𝐴↘
{𝛼 : 𝐴}↘ =𝐴↘
With the erasure function we can conclude that our nominal unfoldings are equivalent to double
unfoldings with the following two lemmas:
Theorem 30. If Γ ⊢𝑛 𝐴 ≤ 𝐵 then Γ ⊢𝑎 𝐴↘ ≤ 𝐵 ↘ .
Theorem 31. If Γ ⊢𝑎 𝐴 ≤ 𝐵 then Γ ⊢𝑛 𝐴 ≤ 𝐵.
For Theorem 30 we wish to show that all valid subtyping statements using nominal unfoldings
are also valid under the double unfolding formulation. To show this result we have to apply theerasure function to the types, since the types in the nominal unfolding formulation may containlabels. For Theorem 31 no erasure function is necessary since the types in the double unfolding
formulation are a subset of those in the nominal unfolding formulation. Thus, they can be directly
mapped. As a consequence of the two theorems above, our nominal unfoldings are also sound andcomplete with respect to our specification using finite unfoldings.
Corollary 32. If Γ ⊢𝑛 𝐴 ≤ 𝐵 then Γ ⊢ 𝐴↘ ≤ 𝐵 ↘ .
Corollary 33. If Γ ⊢ 𝐴 ≤ 𝐵 then Γ ⊢𝑛 𝐴 ≤ 𝐵.
4.7

Decidability

Our subtyping rules are decidable. We have already proved the equivalence between the rules
employing nominal, double and finite unfoldings. Since both the nominal and the double unfolding
rules are syntax directed, they provide a useful foundation to prove decidability. We have proved
decidability based on our nominal rule and a measure that is based on the depth of the unfolded
tree. A similar proof should be possible using the double unfolding rule, except that with the double
unfolding rule there is some extra work because of the extra 1-time finite unfolding premise.
Our subtyping rules are based on substitution, which can increase the size of types after an
unfolding. Therefore, a straightforward induction on the size of types will not work. A first idea
may be doing induction lexicographically on a pair with the number of nesting of recursive binders,
and the size of types. The logic is that, after a nominal unfolding, the recursive binder that we aregoing to unfold will not reappear again. However, this does not quite work because the bodies ofrecursive types can contain other recursive types and the substitutions may introduce new copiesof those recursive types. Thus, the subtyping rule for recursive types does not necessarily reduce
the number of recursive binders. Consider, for instance, the following example:
𝜇𝛼 . 𝜇𝛽. 𝛼 → 𝛽After the nominal unfolding and 𝛼-conversion, the type will become:𝜇𝛽. {𝛼 : 𝜇𝛽 ′ . 𝛼 → 𝛽 ′ } → 𝛽which does not decrease the number of recursive binders. Nevertheless, if we continue to process
the types using nominal unfolding, we will finally reach a type without any recursive binders. Aftera few more steps in the subtyping derivation, we obtain:{𝛼 : 𝜇𝛽 ′ . 𝛼 → 𝛽 ′ } → {𝛽 : {𝛼 : 𝜇𝛽 ′ . 𝛼 → 𝛽 ′ } → 𝛽}
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:31

and the inner recursive types 𝜇𝛽 ′ . 𝛼 → 𝛽 ′ no longer contain recursive types in their bodies, andwe will finally obtain types free of recursive types after another round of nominal unfolding.
Measure based on the depth of the unfolded tree. To provide a measure that decreases at every
nominal unfolding, we define a function based on the depth of the expanded tree of a type. Thisfunction essentially simulates the unfolding process of the tree using nominal unfoldings and allow
us to obtain an (over-)approximation of the depth of the (fully) unfolded tree.
Definition 34. The height of a type 𝐴 in a context Ψ (Ψ := · | Ψ, 𝛼 ↦→ 𝑖, where 𝑖 represents anatural number), written ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝐴), is defined as follows:ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (nat)ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (⊤)ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝐴1 → 𝐴2 )ℎ𝑒𝑖𝑔ℎ𝑡 Ψ ({𝛼 : 𝐴})ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝛼)ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝛼)ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝜇𝛼 . 𝐴)

=
=
=
=
=
=
=

0
0
𝑚𝑎𝑥 (ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝐴1 ), ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝐴2 )) + 1ℎ𝑒𝑖𝑔ℎ𝑡 Ψ (𝐴) + 1
Ψ(𝛼)(𝛼 ∈ Ψ)0(𝛼 ∉ Ψ)let 𝑖 = ℎ𝑒𝑖𝑔ℎ𝑡 Ψ, 𝛼↦→0 (𝐴) in ℎ𝑒𝑖𝑔ℎ𝑡 Ψ, 𝛼↦→𝑖+1 (𝐴) + 1

The two interesting cases in the height function are for recursive variables and recursive types.
For a recursive variable, if it can be found in the context, we retrieve the corresponding heightassociated with the recursive variable from the context, whereas we return 0 if 𝛼 is not in thecontext. Note that, when performing subtyping on two closed types (which is always the casein the subsumption rule) the latter case never happens. However, to make height total we haveto consider this case too, and therefore our height function applies even to types which are notwell-formed. For a recursive type, we firstly compute the height of its body by assuming that theheight of its binder is 0. In other words 𝑖 is the height of the one time finite unfolding. Then wecompute the height of the body again, but this time assuming that the height of its binder is 𝑖 + 1(i.e. the size of the one-time unfolding plus 1). This basically computes the overall height of thenominal unfolding. Since we compute the height two times for a recursive type, our height function
is convex: its second derivative with respect to the number of recursive types is non-negative thus
a linear over-approximation is impossible.
Finally, the measure of a type 𝐴 is defined as ℎ𝑒𝑖𝑔ℎ𝑡 (𝐴), which is the height of expanded tree
when the context Ψ is empty.
Decidability. With the new measure, now we can prove the decidability lemma. For a nonrecursive type, it is obvious that the height of a conclusion from any inputs is strictly greater thanthe height of its any premises. For a recursive type, the measure will decrease by 1 after a nominal
unfolding. In other words, what we want to show isℎ𝑒𝑖𝑔ℎ𝑡 (𝜇𝛼 . 𝐴) − 1 = ℎ𝑒𝑖𝑔ℎ𝑡𝛼↦→ℎ𝑒𝑖𝑔ℎ𝑡𝛼 ↦→0 (𝐴)+1 (𝐴) = ℎ𝑒𝑖𝑔ℎ𝑡 ( [𝛼 ↦→ {𝛼 : 𝐴}] 𝐴).
Firstly, it is easy to observe that ℎ𝑒𝑖𝑔ℎ𝑡𝛼↦→0 (𝐴) = ℎ𝑒𝑖𝑔ℎ𝑡 (𝐴), because for a variable, it is either
found at the context, which is Ψ(𝛼) = 0, or not found at the context, which will return 0. Then,
when we try to compute ℎ𝑒𝑖𝑔ℎ𝑡 ( [𝛼 ↦→ {𝛼 : 𝐴}] 𝐴), since 𝛼 is substituted by {𝛼 : 𝐴} and 𝛼 is notin the context, the formula can be rewritten as ℎ𝑒𝑖𝑔ℎ𝑡𝛼↦→ℎ𝑒𝑖𝑔ℎ𝑡 ( {𝛼 :𝐴 }) (𝐴), in which we do not try
to proceed with the substitution, but just return the result from the context. We can continue torewrite this formula as ℎ𝑒𝑖𝑔ℎ𝑡𝛼↦→ℎ𝑒𝑖𝑔ℎ𝑡 (𝐴)+1 (𝐴). Through ℎ𝑒𝑖𝑔ℎ𝑡𝛼↦→0 (𝐴) = ℎ𝑒𝑖𝑔ℎ𝑡 (𝐴), the formula isequal to ℎ𝑒𝑖𝑔ℎ𝑡𝛼↦→ℎ𝑒𝑖𝑔ℎ𝑡𝛼 ↦→0 (𝐴)+1 (𝐴). Therefore, we have proven our proposition. Next we can provethat this measure suffices to show the termination of subtyping with nominal unfoldings:
Lemma 35. If 𝑚𝑎𝑥 (ℎ𝑒𝑖𝑔ℎ𝑡 (𝐴), ℎ𝑒𝑖𝑔ℎ𝑡 (𝐵)) ≤ 𝑘, then Γ ⊢𝑛 𝐴 ≤ 𝐵 or not Γ ⊢𝑛 𝐴 ≤ 𝐵.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:32

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Proof. Do induction on 𝑘, 𝐴 and 𝐵, respectively.

□

Let 𝑘 = 𝑚𝑎𝑥 (ℎ𝑒𝑖𝑔ℎ𝑡 (𝐴), ℎ𝑒𝑖𝑔ℎ𝑡 (𝐵)), we obtain:
Theorem 36. Termination:
For any inputs Γ, 𝐴 and 𝐵, we either have Γ ⊢𝑛 𝐴 ≤ 𝐵 or not Γ ⊢𝑛 𝐴 ≤ 𝐵.
Finally, from termination and the soundness and completeness of subtyping based on nominal unfoldings with respect to subtyping based on finite unfoldings we can conclude that our specificationof iso-recursive subtyping is decidable.
Corollary 37. Decidability: Our specification for iso-recursive subtyping is decidable.
5

EQUIVALENCE TO THE AMBER RULES

This section shows a variant of the Amber rules that is equivalent, in terms of expressive power,
to our new formulation of subtyping. We prove the equivalence via soundness and completenesstheorems between the two formulations of subtyping. The soundness lemma implies that if two
types are subtypes under the Amber rules, they are subtypes under our new formulation. The
completeness lemma implies that if two types are subtypes under our new formulation, they are
subtypes under the Amber rules. With both lemmas we can conclude that our formulation and theAmber rules have the same expressiveness. To establish the soundness and completeness results
we have to impose some well-formedness conditions. These conditions have been omitted in early
formulations of the Amber rules (as mentioned in Section 2.5), but are necessary here to come up
with precise results regarding the metatheory.
5.1

The Challenges of Well-Formedness for the Amber Rules

In the original Amber rules by Amadio and Cardelli [1993] (Figure 3) there are no well-formedness
constraints. Unfortunately, defining such well-formedness constraints is not entirely trivial. Furthermore, for those interested in mechanical formalization using theorem provers (as we are),such details need to be spelled out clearly. Well-formedness usually plays an important role in themetatheory, since some proofs can be more easily proved by considering well-formed types andenvironments only. One typical property of subtyping that we may hope to have is the so-called
regularity of subtyping:If Γ ⊢ 𝐴 ≤ 𝐵 then ⊢ Γ ∧ Γ ⊢ 𝐴 ∧ Γ ⊢ 𝐵.
which states that if a subtyping statement is valid then the context and types are well-formed.
Regularity is typically used in many other proofs, such as the proof of transitivity in algorithmic
formulations. Note that, in the Amber rules, the rule for recursive types uses two distinct typevariables 𝛼 and 𝛽 in the recursive types. The use of such distinct type variables is a crucial featureof the Amber rules and is used to prevent subderivations of the form Γ ⊢ 𝛽 ≤ 𝛼, where Γ only
contains 𝛼 ≤ 𝛽 but not 𝛽 ≤ 𝛼. Otherwise, if such subderivations would be accepted, type soundness
would be broken.
With the Amber rules an intuitive idea is that the subtyping environment consists of a sequenceof pairs of type variables 𝛼 ≤ 𝛽 and that the 𝛼’s are in scope on the type at the left-side of thesubtyping relation (𝐴), while the 𝛽’s are in scope in the type at the right-side of the subtyping
relation (𝐵). Sadly, this idea is not that simple to realise. Note that in the subtyping rule of function
types (rule Amber-arrow), the input arguments are swapped, so without any changes in theenvironment the type variables in the types would go out-of scope, and this breaks the regularity
lemma. Furthermore, trying to perhaps swap the variables in the environment to keep them inscope changes the meaning of the environment (𝛼 ≤ 𝛽 becomes 𝛽 ≤ 𝛼). Trying to ensure that the
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:33

𝛼’s are only in scope in one side of the relation, while the 𝛽’s are only in scope in the other side,turns out to be quite tricky. Therefore, to make progress, we propose a weaker restriction in thissection: we allow both 𝛼’s and 𝛽’s to be in scope for both types. Thus, the following subtyping
statement is valid with our variant of the Amber rules: 𝛼 ≤ 𝛽 ⊢ 𝛼 → 𝛽 ≤ ⊤. In other words, we
accept some subtyping statements that one would perhaps expect to be ill-formed or rejected. Thatis, in the Amber rules, if we have 𝛼 ≤ 𝛽 in Γ, we would not expect that 𝛼 and 𝛽 appear in thesame type. Rather we would expect that the 𝛼 appears in one of the types, and 𝛽 in the other one.
However, accepting such subtyping statements is not harmful: we can still prove the soundness
and completeness of this variant with respect to our new formulation of subtyping.
5.2

Well-Formedness and Subtyping

In the Amber rules, the subtyping context stores pairs of distinct type variables. We use:
Δ := · | Δ, 𝛼 ≤ 𝛽
to denote the context for Amber rules. Figure 10 shows a set of standard Amber rules with a built-in
reflexivity rule.
Well-formedness. A well-formed environment ( ⊢ Δ) requires that all pairs of variables (𝛼 ≤ 𝛽)in the environment Δ are distinct. Well-formed types are almost standard, except that both 𝛼 and 𝛽
are considered declared by a pair (𝛼 ≤ 𝛽) in the context (rule WFAmber-varl and rule WFAmbervarr), and rule WFAmber-rec introduces a pair of fresh variables into the context, although thesecond variable is never used. Rule WFAmber-rec simply mimics the left-hand side derivationof rule Amber-rec of the Amber subtyping relation, as we shall see next. With our definition ofwell-formed types regularity is easy to obtain:
Lemma 38. Regularity: If Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵 then ⊢ Δ and Δ ⊢ 𝐴 and Δ ⊢ 𝐵.
Subtyping. The subtyping relation is almost the same as the original rules by Amadio and Cardelli[1993] in Figure 3. The noticeable difference is the addition of various well-formedness checks invarious rules. For instance, base cases such as rule Amber-nat and rule Amber-top check whether
the environments are well-formed. Moreover, in rule Amber-self we require the recursive type tobe well-formed (Δ ⊢ 𝜇𝛼 . 𝐴).
5.3

A Third Subtyping Relation Based on a Weakly Positive Restriction

To prove the soundness and completeness with respect to our own formulation of subtyping wecreate an intermediate subtyping relation to make the proof easier. This intermediate relation,
presented in Figure 11, is equivalent to the Amber rules in Figure 10. The key idea in this relation is tohave a rule for recursive types (rule PosRes-rec), which only accepts weakly positive subtyping. This
formulation is inspired by the existing positive formulation of subtyping for recursive types [Amadio
and Cardelli 1993; Appel and Felty 2000; Backes et al. 2014], but it is more general.
In essence, what we mean by weakly positive subtyping is that we can never find a contravariant
subderivation 𝛼 ≤ 𝛼, where 𝛼 is a recursive type variable, for non-equal recursive types. For instancethis excludes 𝜇𝛼 .𝛼 → nat ≤ 𝜇𝛼 .𝛼 → ⊤, since here 𝛼 is used contravariantly, and 𝛼 ≤ 𝛼 would
appear as a subderivation. Notice, however, that weakly positive subtyping still allows subtypingof recursive types with negative occurrences of the recursive type variable in two cases:• Equal types: If the recursive types are equal, then weakly positive subtyping still considers
the two types to be subtypes. For instance 𝜇𝛼 .𝛼 → nat ≤ 𝜇𝛼 .𝛼 → nat, is a valid subtyping
statement.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:34

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. OliveiraΔ⊢𝐴(Well-Formed Type of Amber Rules)

WFAmber-nat

WFAmber-Top

WFAmber-varl

WFAmber-varr

⊢Δ

⊢Δ

⊢Δ

⊢Δ

Δ ⊢ nat

Δ⊢⊤

𝛼≤𝛽∈Δ

𝛼≤𝛽∈Δ

Δ⊢𝛼

Δ⊢𝛽

WFAmber-arrow

WFAmber-rec

Δ ⊢ A1Δ, 𝛼 ≤ 𝛽 ⊢ A

Δ ⊢ A2Δ ⊢ A1 → A2

𝛽 is freshΔ ⊢ 𝜇𝛼 . A

Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵(Amber Rules)

Amber-nat⊢Δ
Δ ⊢𝑎𝑚𝑏 nat ≤ nat

Amber-top

Amber-arrow⊢Δ

Δ ⊢𝑎𝑚𝑏 B1 ≤ A1

Δ⊢A

Δ ⊢𝑎𝑚𝑏 A ≤ ⊤Amber-var

Amber-rec⊢Δ

Δ, 𝛼 ≤ 𝛽 ⊢𝑎𝑚𝑏 A ≤ B

𝛼≤𝛽∈Δ

Δ ⊢𝑎𝑚𝑏 𝛼 ≤ 𝛽Δ ⊢𝑎𝑚𝑏 A2 ≤ B2

Δ ⊢𝑎𝑚𝑏 A1 → A2 ≤ B1 → B2

Δ ⊢𝑎𝑚𝑏 𝜇𝛼 . A ≤ 𝜇𝛽. 𝐵

Amber-self⊢ΔΔ ⊢ 𝜇𝛼 . A

Δ ⊢𝑎𝑚𝑏 𝜇𝛼 . A ≤ 𝜇𝛼 . A

Fig. 10. A variant of the Amber rules, including well-formedness of types.

• The recursive type variable is a subtype of ⊤: If a recursive type variable appears
negatively, but the only (negative) subderivations are of the form 𝛼 ≤ ⊤, then that is allowed
in weakly positive subtyping. For instance 𝜇𝛼 .⊤ → 𝛼 ≤ 𝜇𝛼 .𝛼 → 𝛼 is a valid weakly positive
subtyping statement.
These two exceptions are why we use the term “weakly” to characterize such formulation ofsubtyping. In contrast, existing formulations of positive subtyping, such as that described in
Section 2.4 or originally described by Amadio and Cardelli [1993] do not make such exceptions andwould reject the subtyping statements that we have described above.
Well-formedness and weakly positive relation. Well-formed types are the same as in Figure 6. To
examine whether a type variable occurs positively in a subtyping relation, we define a weakly
positive restriction relation 𝛼 ∈𝑚 𝐴 ≤ 𝐵 at the top of Figure 11. Here, 𝛼 ∈𝑚 𝐴 ≤ 𝐵 means that: typevariable 𝛼 occurs in the derivation 𝐴 ≤ 𝐵 with a mode 𝑚, where a mode 𝑚 is either positive (+) or
negative (-)4 . This relation checks that every instance of 𝛼 ≤ 𝛼 in the proof derivation of 𝐴 ≤ 𝐵 isfound in a positive position inside the proof (rule Pos-varx). Moreover, for every subderivation of𝐴 ≤ 𝐵 with shape 𝜇𝛽. 𝐴 ′ ≤ 𝜇𝛽. 𝐵 ′ either 1) 𝐴 ′ = 𝐵 ′ and 𝛼 is not free in 𝐴 ′ (rule Posvar-recself),or 2) 𝛽 ∈+ 𝐴 ′ ≤ 𝐵 ′ (rule Posvar-rec).
For example, 𝛼 ∈+ ⊤ → 𝛼 ≤ 𝛼 → 𝛼 holds, since the only instance of 𝛼 ≤ 𝛼 occurs positively
and there are no recursive types inside, so the second condition does not apply. To see the need forthe second condition, consider:𝛽 ∈+ 𝜇𝛼 . 𝛼 → 𝛽 ≤ 𝜇𝛼 . 𝛼 → 𝛽which might seem to hold according to the syntax, since 𝛽 appears only in positive positions.
However, it is rejected by both rule Posvar-rec and rule Posvar-recself. Rule Posvar-rec requiresthat 𝛼 also appears positively in subderivations, which does not hold in this example. The reason
4 Note that ∈ is just part of the syntax of the relation, rather than a separate operator.
𝑚

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:35

𝛼 ∈𝑚 𝐴 ≤ 𝐵(Weakly Positive Restriction)
Posvar-arrow

Posvar-nat

Posvar-topl

Posvar-topr

𝛼 ∈m nat ≤ nat

𝛼 ∈m A ≤ ⊤𝛼 ∈m ⊤ ≤ A
Posvar-vary

𝛼 ∈m B1 ≤ A1

𝛼 ∈m A2 ≤ B2

𝛼 ∈m A1 → A2 ≤ B1 → B2
Posvar-recself

Posvar-varx

𝛼≠𝛽𝛽 ∉ 𝑓 𝑣 (A)𝛼 ∈+ 𝛼 ≤ 𝛼𝛼 ∈m 𝛽 ≤ 𝛽𝛽 ∈m 𝜇𝛼 . A ≤ 𝜇𝛼 . A

Posvar-rec

𝛽 ∈m A ≤ B

𝛼 ∈+ A ≤ B𝛼≠𝛽𝛽 ∈m 𝜇𝛼 . A ≤ 𝜇𝛼 . B
Γ ⊢ 𝐴 ≤+ 𝐵
PosRes-nat⊢ΓΓ ⊢ nat ≤+ nat(Weakly Positive Subtyping)
PosRes-top

PosRes-var

PosRes-arrow⊢Γ⊢ΓΓ ⊢ B1 ≤+ A1

Γ⊢AΓ ⊢ A ≤+ ⊤𝛼∈ΓΓ ⊢ 𝛼 ≤+ 𝛼Γ ⊢ A2 ≤+ B2

Γ ⊢ A1 → A2 ≤+ B1 → B2
PosRes-self

PosRes-rec

Γ, 𝛼 ⊢ A ≤+ B

𝛼 ∈+ A ≤ BΓ ⊢ 𝜇𝛼 . A ≤+ 𝜇𝛼 . B⊢ΓΓ ⊢ 𝜇𝛼 . AΓ ⊢ 𝜇𝛼 . A ≤+ 𝜇𝛼 . A

Fig. 11. Weakly Positive Subtyping Rules.

we pose such restriction is because unfolding both types results in the following judgment
𝛽 ∈+ (𝜇𝛼 . 𝛼 → 𝛽) → 𝛽 ≤ (𝜇𝛼 . 𝛼 → 𝛽) → 𝛽
where a negative occurrence of 𝛽 ≤ 𝛽 would appear in a subderivation. A similar issue happens
whenever 𝛼 ≤ 𝛼 appears negatively and the recursive types are not equal to each other.
There are also some noteworthy points in the other rules for the weakly positive restriction
relation. In rule Posvar-arrow, for the contravariant types, we switch their mode by a flip operation¯ + = − and − = +. Rule Posvar-vary states that if 𝛼 is not equal to 𝛽, we do not care what the𝑚:mode for 𝛽 is. Rule Posvar-topr, at first glance, looks suspicious, since it seems to indicate that
⊤ ≤ 𝐴 is valid. In this rule the choice of notation for the relation, using ≤, may be a little misleading.
Although normally we follow the derivation of the subtyping relation, the mode is determined by
the position and not by whether the two types are subtypes. The addition of rule Posvar-topr is
not harmful: the relation is always accompanied by weakly positive subtyping derivations, and⊤ ≤ 𝐴 never occurs in such subtyping derivations. The reason to include rule Posvar-topr is that
we wish that our weakly positive restriction relation is symmetric: if 𝛼 ∈𝑚 𝐴 ≤ 𝐵 then 𝛼 ∈𝑚 𝐵 ≤ 𝐴.
This symmetry property is important for the proof of Lemma 47.
Subtyping. Most subtyping rules are identical to those of the Amber rules, and the only differences
are rule PosRes-var, rule PosRes-rec and rule PosRes-self. The rule PosRes-var is similar to
our formulations, checking whether two variables are same. The latter two rules state that: 1)
two recursive types are subtypes if they are equal (rule PosRes-self); or 2) the recursive variablesatisfies the weakly positive restriction and the two bodies are subtypes (rule PosRes-rec).
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:36

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Basic properties. Reflexivity is straightforward since we have explicit reflexivity built-in forrecursive types.
Theorem 39. Reflexivity.
If ⊢ Γ and Γ ⊢ 𝐴 then Γ ⊢ 𝐴 ≤+ 𝐴.
As for transitivity, because we have the weakly positive restriction for recursive subtyping, theproof is a bit complex. We need to prove an auxiliary lemma in advance:
Lemma 40. If(1) Γ ⊢ 𝐴 ≤+ 𝐵;(2) Γ ⊢ 𝐵 ≤+ 𝐶;(3) 𝛼 ∈𝑚 𝐴 ≤ 𝐵;(4) 𝛼 ∈𝑚 𝐵 ≤ 𝐶,
then Γ ⊢ 𝐴 ≤+ 𝐶 and 𝛼 ∈𝑚 𝐴 ≤ 𝐶.
Proof. Induction on Γ ⊢ 𝐵.

□

Then we can have the transitivity theorem.
Theorem 41. Transitivity.
If Γ ⊢ 𝐴 ≤+ 𝐵 and Γ ⊢ 𝐵 ≤+ 𝐶 then Γ ⊢ 𝐴 ≤+ 𝐶.
Proof. Induction on Γ ⊢ 𝐵. For the recursive case, apply lemma 40, we have all premises.

□

Finally, it is also possible to prove the unfolding lemma for weakly positive subtyping:
Lemma 42. Unfolding Lemma.
If Γ ⊢ 𝜇𝛼 . 𝐴 ≤+ 𝜇𝛼 . 𝐵 then Γ ⊢ [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤+ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
The proof employs similar techniques to those used for the soundness lemma (Lemma 49). We skip
the details here.
5.4

The Soundness Theorem

To show that Amber subtyping is sound with respect to weakly positive subtyping and the double
unfolding rules, we need to translate the environments and types used in the Amber formulation,
since they have different forms.
Definition 43. Translation of environments and types from the Amber rules.
|·|=·(·) (𝐴) = 𝐴|Δ, 𝛼 ≤ 𝛽 | = |Δ|, 𝛼(Δ, 𝛼 ≤ 𝛽) (𝐴) = (Δ) ( [𝛽 ↦→ 𝛼] 𝐴)

The translation functions, | · | and (·) (𝐴), simply drop every second variable defined in thecontext Δ. For example, a subtyping judgment in the Amber system 𝛼 ≤ 𝛽 ⊢ 𝛼 → ⊤ ≤ 𝛽 → ⊤ istranslated to 𝛼 ⊢ 𝛼 → ⊤ ≤ 𝛼 → ⊤.
Before showing the relationship between the Amber subtyping and our subtyping with thepositive restriction, we must prove an important auxiliary lemma:
Lemma 44. If Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵 and (𝛼 ≤ 𝛽) ∈ Δ, then(1) 𝛼 ∉ 𝑓 𝑣 (𝐵) and 𝛽 ∉ 𝑓 𝑣 (𝐴) implies 𝛼 ∈+ (Δ) (𝐴) ≤ (Δ) (𝐵) and(2) 𝛼 ∉ 𝑓 𝑣 (𝐴) and 𝛽 ∉ 𝑓 𝑣 (𝐵) implies 𝛼 ∈− (Δ) (𝐴) ≤ (Δ) (𝐵).
Proof. Do induction on Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:37• Rule Amber-var: In such case 𝐴 = 𝛼 ′ and 𝐵 = 𝛽 ′.
★ Goal (1): If 𝛼 ≠ 𝛼 ′, we achieve the goal (recall that 𝛼 ∈𝑚 𝛼 ′ ≤ 𝛼 ′ always holds for any mode𝑚). Otherwise, we know that 𝛼 = 𝛼 ′. Since (𝛼 ≤ 𝛽) ∈ Δ, the goal becomes 𝛼 ∈+ 𝛼 ≤ 𝛼.
★ Goal (2): 𝛼 ∉ 𝑓 𝑣 (𝐴) implies 𝛼 ≠ 𝛼 ′.
• Rule Amber-rec: Assume 𝐴 = 𝜇𝛼 ′ . 𝐴 ′ and 𝐵 = 𝜇𝛽 ′ . 𝐵 ′, then the goal becomes 𝛼 ∈𝑚(Δ) (𝜇𝛼 ′ . 𝐴 ′) ≤ (Δ) (𝜇𝛽 ′ . 𝐵 ′) (𝑚 is + and −, respectively, for two goals), which can be rewritten
as 𝛼 ∈𝑚 𝜇𝛼 ′ . (Δ) (𝐴 ′) ≤ 𝜇𝛽 ′ . (Δ) (𝐵 ′). Note that here, in the new goal, we use different boundvariables 𝛼 ′ and 𝛽 ′ in the 𝜇 binders to match with the names of the free variables that areadded to the environment Δ next. However, we can freely rename the bound variables to thesame variable, and we will indeed rename 𝛽 ′ below to 𝛼 ′, since the rules for recursive types
in the weakly positive subtyping require the same bound variable names5 .
For convenience, let us denote Δ, (𝛼 ′ ≤ 𝛽 ′) as Δ ′. Then the induction hypotheses become:(1) ∀𝛼 𝛽, (𝛼 ≤ 𝛽) ∈ Δ ′ ⇒ 𝛼 ∉ 𝑓 𝑣 (𝐵 ′) ⇒ 𝛽 ∉ 𝑓 𝑣 (𝐴 ′) ⇒ 𝛼 ∈+ (Δ ′) (𝐴 ′) ≤ (Δ ′) (𝐵 ′) and(2) ∀𝛼 𝛽, (𝛼 ≤ 𝛽) ∈ Δ ′ ⇒ 𝛼 ∉ 𝑓 𝑣 (𝐴 ′) ⇒ 𝛽 ∉ 𝑓 𝑣 (𝐵 ′) ⇒ 𝛼 ∈− (Δ ′) (𝐴 ′) ≤ (Δ ′) (𝐵 ′).
★ For goal (1): we apply rule Posvar-rec, then we need to check if 𝛼 ′ ∈+ (Δ ′) (𝐴 ′) ≤ (Δ ′) (𝐵 ′)and 𝛼 ∈+ (Δ ′) (𝐴 ′) ≤ (Δ ′) (𝐵 ′). Both cases can be solved by applying induction hypothesis(1).
★ For goal (2): we apply rule Posvar-rec, then we need to check if 𝛼 ′ ∈− (Δ ′) (𝐴 ′) ≤ (Δ ′) (𝐵 ′)and 𝛼 ∈+ (Δ ′) (𝐴 ′) ≤ (Δ ′) (𝐵 ′). For the former one we apply induction hypothesis (2), andfor the latter one we apply induction hypothesis (1).
• Rule Amber-self: Assume 𝐴 = 𝐵 = 𝜇𝛼 ′ . 𝐴 ′. From the condition of the goal, we know that𝛼 ∉ 𝑓 𝑣 (𝐴 ′) always holds, thus 𝛼 ∈𝑚 (Δ) (𝐴) ≤ (Δ) (𝐵) is true for any mode 𝑚.
□
With the help of Lemma 44, we can prove that if two types are subtypes under the Amber rules,
they are also subtypes under weakly positive subtyping:
Theorem 45. If Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵 then |Δ| ⊢ (Δ) (𝐴) ≤+ (Δ) (𝐵).
Proof. Do induction on Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵. We show only the more interesting case for recursive
types.
• Rule Amber-rec: Assume 𝐴 = 𝜇𝛼 ′ . 𝐴 ′ and 𝐵 = 𝜇𝛽 ′ . 𝐵 ′. The goal becomes |Δ| ⊢ (Δ) (𝜇𝛼 ′ . 𝐴 ′) ≤(Δ) (𝜇𝛽 ′ . 𝐵 ′), which can be rewritten as |Δ| ⊢ 𝜇𝛼 ′ . (Δ) (𝐴 ′) ≤ 𝜇𝛽 ′ . (Δ) (𝐵 ′). Apply rule PosResrec, the first premise |Δ, 𝛼 ≤ 𝛽 | ⊢ (Δ) (𝐴 ′) ≤ (Δ) (𝐵 ′) can be solved by induction hypothesis.
Since we know Δ, 𝛼 ′ ≤ 𝛽 ′ ⊢𝑎𝑚𝑏 𝐴 ′ ≤ 𝐵 ′, we apply Lemma 44 to it. By obtaining 𝛼 ′ ∈+(Δ) (𝐴 ′) ≤ (Δ) (𝐵 ′), we can solve the second premise.
□
We are now one step away from the soundness theorem: to prove that the weakly positive
subtyping implies double unfolding subtyping. The main difference is on rule PosRes-rec, whichcorresponds to rule SA-rec in the double unfolding subtyping. The proof requires the following
lemma which reveals an important property to prove that the weakly positive subtyping implies
double unfolding subtyping:
Lemma 46. If 𝛼 ∈𝑚 𝐴 ≤ 𝐵 and 𝛽 ∈+ 𝐴 ≤ 𝐵 then 𝛼 ∈𝑚 [𝛽 ↦→ 𝐴] 𝐴 ≤ [𝛽 ↦→ 𝐵] 𝐵.
This lemma tells us that the positive restriction respects the mode on non-negative substitutions.
5 In Coq, using the locally nameless representation, bound variables are represented as De Bruijn indices, and only freevariables use names. Thus renaming is unnecessary.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:38

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

The proof of Lemma 46, as other substitution lemmas that we have showed before, requires
a generalization. Such a generalization is a bit tricky, since we allow equal types in the positive
restriction. For readers interested in the details of the generalization, we refer to our mechanized
proof. This lemma is important because it shows that, with Lemma 46 proved, we can derive thefollowing lemma, which relates weakly positive subtyping to our algorithmic subtyping relation in
the double unfolding form:
Lemma 47. If Γ ⊢𝑎 𝐴 ≤ 𝐵 and Γ ⊢𝑎 𝐶 ≤ 𝐷, then(1) 𝛼 ∈+ 𝐴 ≤ 𝐵 implies Γ ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝐵 and(2) 𝛼 ∈− 𝐵 ≤ 𝐴 implies Γ ⊢𝑎 [𝛼 ↦→ 𝐷] 𝐴 ≤ [𝛼 ↦→ 𝐶] 𝐵.
Proof. Do induction on Γ ⊢𝑎 𝐴 ≤ 𝐵. We only show how to prove the function case.
• Rule SA-arrow: Assume 𝐴 = 𝐴1 → 𝐴2 and 𝐵 = 𝐵 1 → 𝐵 2 .
★ Goal (1):∗ The goal becomes Γ ⊢𝑎 [𝛼 ↦→ 𝐶] (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝐷] (𝐵 1 → 𝐵 2 ), which can be
rewritten as Γ ⊢𝑎 ( [𝛼 ↦→ 𝐶] 𝐴1 ) → ( [𝛼 ↦→ 𝐶] 𝐴2 ) ≤ ( [𝛼 ↦→ 𝐷] 𝐵 1 ) → ( [𝛼 ↦→ 𝐷] 𝐵 2 ).
∗ The condition from Goal (1) becomes 𝛼 ∈+ 𝐴1 → 𝐴2 ≤ 𝐵 1 → 𝐵 2 . By inversion, we
obtain 𝛼 ∈− 𝐵 1 ≤ 𝐴1 and 𝛼 ∈+ 𝐴2 ≤ 𝐵 2 .
∗ Apply rule SA-arrow on the goal, we need to prove: Γ ⊢𝑎 [𝛼 ↦→ 𝐷] 𝐵 1 ≤ [𝛼 ↦→ 𝐶] 𝐴1
and Γ ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴2 ≤ [𝛼 ↦→ 𝐷] 𝐵 2 .
∗ For the latter one, we apply the induction hypothesis (1).
∗ For the former one, we apply the induction hypothesis (2). However, we need to prove𝛼 ∈− 𝐴1 ≤ 𝐵 1 . Recall that the positive restriction is commutative, so from 𝛼 ∈− 𝐵 1 ≤ 𝐴1
we can prove 𝛼 ∈− 𝐴1 ≤ 𝐵 1 .
★ Goal (2):∗ The goal becomes Γ ⊢𝑎 [𝛼 ↦→ 𝐷] (𝐴1 → 𝐴2 ) ≤ [𝛼 ↦→ 𝐶] (𝐵 1 → 𝐵 2 ), which can be
rewritten as Γ ⊢𝑎 ( [𝛼 ↦→ 𝐷] 𝐴1 ) → ( [𝛼 ↦→ 𝐷] 𝐴2 ) ≤ ( [𝛼 ↦→ 𝐶] 𝐵 1 ) → ( [𝛼 ↦→ 𝐶] 𝐵 2 ).
∗ The condition from Goal (1) becomes 𝛼 ∈− 𝐵 1 → 𝐵 2 ≤ 𝐴1 → 𝐴2 . By inversion, we
obtain 𝛼 ∈+ 𝐴1 ≤ 𝐵 1 and 𝛼 ∈− 𝐵 2 ≤ 𝐴2 .
∗ Apply rule SA-arrow on the goal, we need to prove: Γ ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐵 1 ≤ [𝛼 ↦→ 𝐷] 𝐴1
and Γ ⊢𝑎 [𝛼 ↦→ 𝐷] 𝐴2 ≤ [𝛼 ↦→ 𝐶] 𝐵 2 .
∗ For the latter one, we apply the induction hypothesis (2).
∗ For the former one, we apply the induction hypothesis (1). However, we need to prove𝛼 ∈+ 𝐵 1 ≤ 𝐴1 . Because the positive restriction is commutative, from 𝛼 ∈+ 𝐴1 ≤ 𝐵 1 wecan prove 𝛼 ∈+ 𝐵 1 ≤ 𝐴1 .
□Corollary 48. If 𝛼 ∈+ 𝐴 ≤ 𝐵 and Γ ⊢𝑎 𝐴 ≤ 𝐵 then Γ ⊢𝑎 [𝛼 ↦→ 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝐵] 𝐵.
With the Corollary 48, the relation between positive restriction and the algorithmic double
unfolding subtyping is easy to establish:
Theorem 49. If Γ ⊢ 𝐴 ≤+ 𝐵 then Γ ⊢𝑎 𝐴 ≤ 𝐵.
Combining Lemmas 21, 45 and 49, we have
Corollary 50. Soundness of the Amber rules with respect to the declarative formulation.
If Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵 then |Δ| ⊢ (Δ) (𝐴) ≤ (Δ) (𝐵).
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

5.5

1:39

The Completeness Theorem

The completeness theorem, to some degree, is more difficult than soundness theorem. Because theAmber rules are more complex in terms of shape than the double unfolding rule, more cases need
to be discussed when we do induction on a simpler formulation.
Firstly, let us consider how to convert the double unfolding rule to weakly positive subtyping.
The double unfolding rule and weakly positive subtyping share the same context, which means
the only source of difference comes from the treatment of recursive types. For weakly positive
subtyping, the following inversion lemma is useful:Lemma 51. If Γ ⊢ 𝐴 ≤+ 𝐵 and Γ ⊢ 𝐶 ≤+ 𝐷, then(1) Γ ⊢ [𝛼 ↦→ 𝐶] 𝐴 ≤+ [𝛼 ↦→ 𝐷] 𝐵 implies 𝛼 ∈+ 𝐴 ≤ 𝐵 or 𝐶 = 𝐷;(2) Γ ⊢ [𝛼 ↦→ 𝐷] 𝐴 ≤+ [𝛼 ↦→ 𝐶] 𝐵 implies 𝛼 ∈− 𝐴 ≤ 𝐵 or 𝐶 = 𝐷.
This lemma states that if after substitution the subtyping relation is preserved, then either 𝐶 and
𝐷 are equal; or the type variable respects the weakly positive restriction.
Now we can prove that weakly positive subtyping is complete with respect to the double unfolding
formulation.
Theorem 52.
If Γ ⊢𝑎 𝐴 ≤ 𝐵 then Γ ⊢ 𝐴 ≤+ 𝐵.
Proof. Induction on Γ ⊢𝑎 𝐴 ≤ 𝐵. All cases are straightforward except when 𝐴 is 𝜇𝛼 . 𝐴 ′ and 𝐵 is
𝜇𝛼 . 𝐵 ′. By induction hypothesis, we know that Γ ⊢ 𝐴 ′ ≤+ 𝐵 ′. By applying lemma 51 with 𝐴 := 𝐴 ′,𝐵 := 𝐵 ′, 𝐶 := 𝐴 ′, 𝐷 := 𝐵 ′, and mode +, we get that either 𝛼 ∈+ 𝐴 ′ ≤ 𝐵 ′ or 𝐴 ′ = 𝐵 ′. For the former
case, we apply rule PosRes-rec. For the latter case, we apply reflexivity.
□
The translation from weakly positive subtyping to the Amber rules is quite tricky due to the different shapes of the contexts. To illustrate the difficulty consider the following subtyping statement
using weakly positive subtyping:Γ, 𝛼 ⊢ ⊤ → 𝛼 ≤+ nat → 𝛼
where the environment binds the type variable 𝛼. For proving the subtyping relationship, we needto prove:Γ, 𝛼 ⊢ 𝛼 ≤+ 𝛼
However, if we want to prove the same statement using the Amber rules, we need to change therelationship to:Δ, 𝛼 ≤ 𝛽 ⊢𝑎𝑚𝑏 ⊤ → 𝛼 ≤ nat → 𝛽
andΔ, 𝛼 ≤ 𝛽 ⊢𝑎𝑚𝑏 𝛼 ≤ 𝛽Note that, in weakly positive subtyping, we only need to store the free variables in the environment,
while in the Amber rules, we have more variables and store the subtyping relationship between
those variables as well.
The recipe of the conversion is to first generate a bundle of variables and match them to existing
variables. Then we determine the mode for each variable in weakly positive subtyping, which helps
us to allocate every pair of generated variables. After converting the context and types to the formof Amber rules, we prove that they preserve the subtyping relationship under the Amber rules.
As a second example, assume that we want to convert the following judgment into an Amber
judgment𝛼, 𝛽 ⊢ 𝛽 → 𝛼 ≤+ 𝛽 → 𝛼
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:40

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. OliveiraΓ ⊢ 𝐴 ≤+ 𝐵 ▷ Π(Position Allocation)mono-consmono-nil𝛼 ∈m A ≤ B· ⊢ A ≤+ B ▷ ·Γ ⊢ A ≤+ B ▷ ΠΓ, 𝛼 ⊢ A ≤+ B ▷ Π, m

Fig. 12. Position Allocation for Weakly Positive Subtyping

we first generate new variables 𝛼 ′, 𝛽 ′ and assume the subtyping relations 𝛼 ≤ 𝛼 ′, 𝛽 ≤ 𝛽 ′. Then we
examine the positivity of both variables and find out that these relations hold𝛼 ∈+ 𝛽 → 𝛼 ≤ 𝛽 → 𝛼 and 𝛽 ∈− 𝛽 → 𝛼 ≤ 𝛽 → 𝛼In the next step, we substitute the variables in the typing judgment, according to the mode andlocation. If the variable is in the left-hand side and occurs positively, or right-hand side and occurs
negatively, we keep the variable as it is. Otherwise, we substitute the variable with its corresponding
one (𝛼 ↦→ 𝛼 ′ and 𝛽 ↦→ 𝛽 ′). After these steps, the final result becomes a normal Amber judgment,
which has the same meaning of the initial judgment:𝛼 ≤ 𝛼 ′, 𝛽 ≤ 𝛽 ′ ⊢𝑎𝑚𝑏 𝛽 ′ → 𝛼 ≤ 𝛽 → 𝛼 ′We prove that this subtyping relation holds under the Amber rules.
Position Allocation. As Figure 12 shows, we define a relation that relates each variable to a mode.
The mode in Π has a one-to-one correspondence to the variables in Γ in the same order. The
definition of Π is
Π := · | Π, + | Π, −Note that it is not necessarily the case that Π is unique. For example, a variable that never occurs
can be accepted by both modes, therefore its corresponding element in Π can be any mode.
Definition 53. Generation of a bundle of fresh variables.
⟨Γ⟩ := {(𝛼 ≤ 𝛽) | ∀𝛼 ∈ Γ, 𝛽 is fresh}
After we have a list of pairs of variables (denoted as ⟨Γ⟩) and the mode for each variable, we
design a function that converts the types according to our information. Note that ⟨Γ⟩ has same
form as the contexts in the Amber setting.
Definition 54. We design a function 𝑐𝑜𝑛𝑣𝑒𝑟𝑡 (Δ, Π, 𝐴, 𝑚) for converting types from weakly positive
subtyping setting to the Amber setting, which takes four inputs: a context for Amber formulation,a stack of modes, a type 𝐴 and a mode. This function returns the converted type as output. Notethat the Π is computed as Figure 12 shown, thus its length is equal to the length of Δ.
𝐴
If Δ and Π are empty.



′
′
𝑐𝑜𝑛𝑣𝑒𝑟𝑡 (Δ, Π, 𝐴, 𝑚) = 𝑐𝑜𝑛𝑣𝑒𝑟𝑡 (Δ , Π , [𝛼 ↦→ 𝛽] 𝐴, 𝑚)
If Δ = Δ ′, 𝛼 ≤ 𝛽 and Π = Π ′, 𝑚′′𝑐𝑜𝑛𝑣𝑒𝑟𝑡 (Δ , Π , 𝐴, 𝑚)
If Δ = Δ ′, 𝛼 ≤ 𝛽 and Π = Π ′, flip 𝑚
We can now state the completeness theorem with Definition 54, where the subtyping relation of
weakly positive subtyping preserves under the Amber rules.
Theorem 55. Completeness of the Amber rules: If Γ ⊢ 𝐴 ≤+ 𝐵 and Γ ⊢ 𝐴 ≤+ 𝐵 ▷ Π, denoted ⟨Γ⟩as Δ, thenΔ ⊢𝑎𝑚𝑏 𝑐𝑜𝑛𝑣𝑒𝑟𝑡 (Δ, Π, 𝐴, −) ≤ 𝑐𝑜𝑛𝑣𝑒𝑟𝑡 (Δ, Π, 𝐵, +).
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:41

For simplicity, we skip the procedure of the proof for this theorem. Theorem 55 has the longest
mechanized proof in the presented paper, which relies on plenty of auxiliary lemmas distinguishingwhether two recursive types are equal carefully.
The theorem involves some manipulation of the context and types, due to the inconsistency ofcontexts between our system and the Amber rules. However, it is very easy to obtain a simple formof corollary where the contexts are empty:
Corollary 56.
If · ⊢ 𝐴 ≤+ 𝐵 then · ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵.
The statement is less general than Theorem 55, but it does reveal that the programmer cannot
distinguish between our algorithm and the Amber one, since in the subsumption rule, the subtyping
judgment always starts with an empty subtyping context. That is, type variables in the double
unfolding formulations, and subtyping relations between type variables in the Amber formulations
are only introduced by the subtyping relation, and not by the typing relation. The only informationthat should be in the context during the subsumption rule is the type information for variables.
Combining Lemmas 17, 52 and 56, we have
Corollary 57. Completeness of the Amber rules with respect to the declarative formulation.
If · ⊢ 𝐴 ≤ 𝐵 then · ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵.
Finally, with the equivalence theorems, transitivity and unfolding lemma for our formulations(Lemmas 57, 50, 6 and 24), we can claim the Amber rules are transitive and satisfy the unfolding
lemma.
Corollary 58. Transitivity of the Amber rules.
If · ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵 and · ⊢𝑎𝑚𝑏 𝐵 ≤ 𝐶 then · ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐶.
Corollary 59. Unfolding lemma for the Amber rules.
If · ⊢𝑎𝑚𝑏 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then · ⊢𝑎𝑚𝑏 [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
Notably, for transitivity, it is interesting to observe that transitivity holds under an empty environment. In Section 2, we discussed the issues with transitivity and showed a counter-example. That
counter-example does not apply to our transitivity lemma because it uses non-empty environments.
Therefore a possible “fix” to the declarative formulation in Figure 3 is to restrict the transitivity
rule to use only empty environments.
6

A CALCULUS WITH RECORDS

So far we considered calculi where the subtyping relation is antisymmetric. For instance, for the
calculus presented in Section 4, Lemmas 19 and 22 hold. Both the Amber rules and the new rules
proposed by us work well for antisymmetric subtyping relations. However, as explained in Section 2,
applying the Amber rules in subtyping relations that are not antisymmetric is non-trivial due tothe built-in reflexivity rule. The purpose of this section is to show that, unlike the Amber rules,
the double unfolding rules can be easily applied to subtyping relations that are not antisymmetric.
In this section we show the type-soundness for an extension of the calculus in Sections 3 and 4
with records and records types, which leads to a subtyping relation that is not antisymmetric whenrecord types are represented as a sequence of pairs of labels and types.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:42

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Types𝐴, 𝐵, 𝐶, 𝐷
Expressions 𝑒FFValuesF𝑣

nat | ⊤ | 𝐴1 → 𝐴2 | 𝛼 | 𝜇𝛼 . 𝐴 | {𝒍 𝒊 : 𝑨𝒊 𝒊 ∈1 ···𝒏 }𝑥 | i | 𝑒 1 𝑒 2 | 𝜆𝑥 : 𝐴. 𝑒 | unfold [𝐴] 𝑒 | fold [𝐴] 𝑒 |{𝒍 𝒊 = 𝒆 𝒊 𝒊 ∈1 ···𝒏 } | 𝒆.𝒍i | 𝜆𝑥 : 𝐴. 𝑒 | fold [𝐴] 𝑣 | {𝒍 𝒊 = 𝒗 𝒊 𝒊 ∈1 ···𝒏 }Γ⊢𝐴(Well-Formed Type (with Record Types))
wft-rcd

wft-recur

Γ, 𝛼 ⊢ A

Γ ⊢ A𝑖Γ, 𝛼 ⊢ [𝛼 ↦→ A] AΓ ⊢ 𝜇𝛼 . AΓ ⊢ {𝑙𝑖 : A𝑖 𝑖 ∈1 ···𝑛 }Γ ⊢𝑎 𝐴 ≤ 𝐵
SA-nat⊢ΓΓ ⊢a nat ≤ nat(Subtyping)SA-varSA-top

⊢Γ

Γ⊢A

⊢Γ

Γ ⊢a A ≤ ⊤SA-arrow𝛼∈ΓΓ ⊢a B1 ≤ A1

Γ ⊢a 𝛼 ≤ 𝛼Γ ⊢a A2 ≤ B2

Γ ⊢a A1 → A2 ≤ B1 → B2

SA-recΓ, 𝛼 ⊢a A ≤ BΓ, 𝛼 ⊢a [𝛼 ↦→ A] A ≤ [𝛼 ↦→ B] BΓ ⊢a 𝜇𝛼 . A ≤ 𝜇𝛼 . B

SA-rcd{𝑙𝑖 𝑖 ∈1 ···𝑛 } ⊆ {𝑘 𝑗 𝑗 ∈1 ···𝑚 }Γ ⊢a {𝑘 𝑗 : A 𝑗𝑗 ∈1 ···𝑚𝑘 𝑗 = 𝑙𝑖 implies Γ ⊢𝛼 A 𝑗 ≤ B𝑖
} ≤ {𝑙𝑖 : B𝑖 𝑖 ∈1 ···𝑛 }Fig. 13. Well-formedness and subtyping rules for record types.

6.1

Syntax, Well-Formedness and Subtyping

Syntax. The syntax of the calculus is:
Natural numbers, arrow types, the top type, type variables and recursive types are the same as
before (Section 3.1). The additional syntax related to records and record types is highlighted with abold font. The notation of record types is {𝑙𝑖 : 𝐴𝑖 𝑖 ∈1 ···𝑛 }. Every label has an associated a type andall labels are required to be distinct. A record expression has the form of {𝑙𝑖 = 𝑒𝑖 𝑖 ∈1 ···𝑛 }, and 𝑒.𝑙 is
the record projection expression.
Well-Formedness. In the type system with record types, we use Γ ⊢ 𝐴 to represent that 𝐴 is
well-formed. The rules of Γ ⊢ 𝐴 include most of the rules at the top of Figure 6. The rule wft-rcd is
new and ensures the well-formedness of record types. Similarly to Section 4, we use rule wft-recurfor recursive types.
Subtyping. Our subtyping rules follow the rules in Figure 8, but are extended with an algorithmic
formulation of record subtyping. The definition of record subtyping (rule SA-rcd) is standard [Pierce
2002]: a record type 𝐴 is a subtype of another record type 𝐵 when: 1) all the labels in 𝐴 are a subsetof the labels in 𝐵; and 2) the field types of the corresponding labels are subtypes.
6.2

Metatheory of Subtyping

Subtyping is reflexive, transitive and the unfolding lemma holds.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:43

Reflexivity and transitivity. After adding record types, reflexivity and transitivity are still preserved.
Theorem 60. Reflexivity
If Γ ⊢ 𝐴 then Γ ⊢𝑎 𝐴 ≤ 𝐴.
Theorem 61. Transitivity
If Γ ⊢𝑎 𝐴 ≤ 𝐵 and Γ ⊢𝑎 𝐵 ≤ 𝐶 then Γ ⊢𝑎 𝐴 ≤ 𝐶.
Unfolding lemma. Unlike the proof for the unfolding lemma in Section 4, we cannot rely on theantisymmetry lemma (Lemma 22) for proving the unfolding lemma. Instead of alpha-equivalenceor syntactic equality, we introduce a weaker form of equivalence.
Definition 62 (Equivalence).
Γ ⊢𝑎 𝐴 ∼ 𝐵 := Γ ⊢𝑎 𝐴 ≤ 𝐵 ∧ Γ ⊢𝑎 𝐵 ≤ 𝐴
With Definition 62, two record types {𝑥 : 𝐼𝑛𝑡, 𝑦 : 𝐵𝑜𝑜𝑙 } and {𝑦 : 𝐵𝑜𝑜𝑙, 𝑥 : 𝐼𝑛𝑡 } are considered tobe equivalent: the only difference of these two types is that one type is a permutation of the othertype. In other words, the equivalence shows that the order in which the labels appear in a record
type does not matter.
One essential lemma is
Lemma 63. If Γ ⊢𝑎 𝐴 ≤ 𝐵 and Γ ⊢𝑎 𝐶 ∼ 𝐷, then Γ ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝐵.
This lemma states that if two types are subtypes, then after substituting a recursive type variable
𝛼 with two equivalent types, the subtyping relationship is preserved. The proof of this lemma isstraightforward. With Lemma 63, we can prove our core lemma, as we did before.
Lemma 64. If(1) Γ1, 𝛼, Γ2 ⊢𝑎 𝐴 ≤ 𝐵;
(2) Γ1, 𝛼, Γ2 ⊢𝑎 𝐶 ≤ 𝐷;(3) Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤ 𝜇𝛼 . 𝐷;then(1) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝐷] 𝐵 implies Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐵 and(2) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐷] 𝐴 ≤ [𝛼 ↦→ 𝐶] 𝐵 implies Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐷] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐶] 𝐵.
Proof. By induction on Γ1, 𝛼, Γ2 ⊢𝑎 𝐴 ≤ 𝐵. Other cases are the same as proof of Lemma 23,
except for:• Case rule SA-var: In such case 𝐴 = 𝐵 = 𝛽. If 𝛼 ≠ 𝛽, the goal is trivial.
– Otherwise, for goal (1), we want to prove Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤ 𝜇𝛼 . 𝐷, which is actually premise(3).
– For goal (2), we have Γ1, 𝛼, Γ2 ⊢𝑎 𝐶 ≤ 𝐷 from premise (2), and Γ1, 𝛼, Γ2 ⊢𝑎 𝐷 ≤ 𝐶 fromthe condition of goal (2), thus Γ1, 𝛼, Γ2 ⊢𝑎 𝐶 ∼ 𝐷. By Lemma 63, we get Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→𝐷] 𝐷 ≤ [𝛼 ↦→ 𝐶] 𝐶. As a result, we have Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐷 ≤ 𝜇𝛼 . 𝐶.
□
Finally, we can prove the unfolding lemma:
Lemma 65. Unfolding Lemma
If Γ ⊢𝑎 𝜇𝛼 . 𝐴 ≤ 𝜇𝛼 . 𝐵 then Γ ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐵] 𝐵.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:44

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. OliveiraΓ ⊢𝑒 :𝐴
typing-nat⊢Γ(Typing)typing-var

typing-sub

⊢Γ

Γ⊢e:A

Γ ⊢ i : nat

𝑥 :𝐴∈Γ
Γ⊢x:A

typing-abs

Γ⊢A≤BΓ, 𝑥 : A1 ⊢ e : A2Γ⊢e:Btyping-app

Γ ⊢ 𝜆x : A1 . e : A1 → A2

typing-unfoldΓ ⊢ e1 : A1 → A2

Γ ⊢ e2 : A1

Γ ⊢ e : 𝜇𝛼 . AΓ ⊢ e1 e2 : A2

Γ ⊢ unfold [𝜇𝛼 . A] e : [𝛼 ↦→ 𝜇𝛼 . A] A
typing-rcd

typing-foldΓ ⊢ e : [𝛼 ↦→ 𝜇𝛼 . A] AΓ ⊢ 𝜇𝛼 . AΓ ⊢ e𝑖 : A𝑖for each 𝑖Γ ⊢ fold [𝜇𝛼 . A] e : 𝜇𝛼 . AΓ ⊢ {𝑙𝑖 = e𝑖𝑖 ∈1 ···𝑛} : {𝑙𝑖 : A𝑖 𝑖 ∈1 ···𝑛 }typing-projΓ ⊢ e : {𝑙𝑖 : A𝑖 𝑖 ∈1 ···𝑛 }Γ ⊢ e.𝑙𝑖 : A𝑖
(Reduction)𝑒 1 ↩→ 𝑒 2
step-appl

e1 ↩→ e1′e2 ↩→ e2′

e1 e2 ↩→ e1′ e2

v1 e2 ↩→ v1 e2′

step-beta(𝜆x : A. e1 ) v2 ↩→ [𝑥 ↦→ v2 ] e1

step-appr

step-unfold

unfold [A] (fold [B] v) ↩→ v

step-folde ↩→ e′e ↩→ e′unfold [A] e ↩→ unfold [A] e′

fold [A] e ↩→ fold [A] e′

step-fld

step-proje ↩→ e′step-projrcd{𝑙𝑖 = v𝑖 𝑖 ∈1 ···𝑛 }.𝑙 𝑗 ↩→ v 𝑗

e.𝑙 𝑗 ↩→ e′ .𝑙 𝑗

step-rcde 𝑗 ↩→ e′𝑗{𝑙𝑖 = 𝑣𝑖 𝑖 ∈1 ···𝑗−1, 𝑙 𝑗 = e 𝑗 , 𝑙𝑘 = 𝑒𝑘 𝑘 ∈𝑗+1 ···𝑛 } ↩→ {𝑙𝑖 = 𝑣𝑖 𝑖 ∈1 ···𝑗−1, 𝑙 𝑗 = e′𝑗 , 𝑙𝑘 = 𝑒𝑘 𝑘 ∈𝑗+1 ···𝑛 }Fig. 14. Typing and reduction rules for record types

A final remark is that the same technique that we employ here to prove the unfolding lemma
could have been used in the calculus in Section 4 as well. In other words, we do not need to rely on
the antisymmetry lemmas in Section 4. We opted to present the two techniques in the paper to alsoemphasize the difference between antisymmetric and non-antisymmetric relations, since for the
Amber rules such difference is quite important.
6.3

Type Soundness

We use the same typing and reduction rules as Section 3.4, extended with extra rules for records
and record types.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:45

Table 2. Paper-to-proofs correspondence guide (without record types).

Definition
Well-formed Type (Figure 6)
Well-formed Type (Definition 2)
Well-formed Type (Definition 13)
Well-formed Type (Figure 9)
Declarative subtyping (Figure 6)
Typing (Figure 7)
Reduction (Figure 7)
Double unfolding rule (Figure 8)
Nominal unfolding rule (Figure 9)
Well-formed Type (Figure 10)
Amber rules (Figure 10)
Weakly Positive restriction (Figure
11)
Weakly Positive subtyping (Figure
11)
Weakly Positive subtyping (Definition 69)

File (in src/ folder)
Rules.v
Rules.v
Rules.v
NominalUnfolding.v
Rules.v
Rules.v
Rules.v
Rules.v
NominalUnfolding.v
AmberBase.v
AmberBase.v
AmberBase.v

Name in Coq
Notation
WFA E AΓ⊢𝐴
WFS E AΓ⊢𝐴
WF E AΓ⊢𝐴
Nominal.WFS E AΓ⊢𝐴Sub E A BΓ⊢𝐴 ≤𝐵typing E e AΓ ⊢𝑒 :𝐴
step e1 e2
𝑒 1 ↩→ 𝑒 2
sub E A B
Γ ⊢𝑎 𝐴 ≤ 𝐵
Nominal.Sub E A B Γ ⊢𝑛 𝐴 ≤ 𝐵
wf_amber E A
Δ⊢𝐴
sub_amber E A B
Δ ⊢𝑎𝑚𝑏 𝐴 ≤ 𝐵
posvar m X A B
𝛼 ∈𝑚 𝐴 ≤ 𝐵

PositiveBase.v

wk_sub E A BΓ ⊢ 𝐴 ≤+ 𝐵

AmberBase.v

sub_amber2 E A BΓ ⊢𝑢 𝐴 ≤+ 𝐵

Typing. As the top of Figure 14 shows, we have two typing rules for record types. Rule typingrcd states that a record is well-typed if we know that all its fields are well-typed. Rule typing-proj
checks that the record that we are projecting from is well-typed, and contains the field label that
we are projecting.
Reduction. As the bottom of Figure 14 shows, we have three reduction rules for record types.
Rule step-projrcd retrieves a component of a record. Rule step-proj reduces the record expression
being projected. Rule step-rcd implements a left-to-right evaluation order to reduce a record.
Type Soundness. The proof technique of proving type-soundness is conventional, without any
special approach, except for the use of the unfolding lemma in preservation (just as in Section 3).
Therefore, we can directly prove preservation and progress.
Theorem 66. Preservation.
If Γ ⊢ 𝑒 : 𝐴 and 𝑒 ↩→ 𝑒 ′ then Γ ⊢ 𝑒 ′ : 𝐴.
Theorem 67. Progress.
If ⊢ 𝑒 : 𝐴 then 𝑒 is a value or exists 𝑒 ′, 𝑒 ↩→ 𝑒 ′ .
7

COQ PROOFS

We have chosen the Coq (8.13) proof assistant [The Coq Development Team 2019] to develop ourformalization. The whole Coq formalization is built with a third-party library Metalib6 , which
provides support for the locally nameless representation [Aydemir et al. 2008] to encode binders.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:46

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Table 3. Paper-to-proofs correspondence guide (with record types).

Definition
Well-formed Type (Figure 13)
Subtyping (Figure 13)
Typing (Figure 14)
Reduction (Figure 14)
7.1

File (in src_extension/ folder) Name in Coq Notation
definition.v
WF E A
Γ⊢𝐴
definition.v
Sub E A BΓ⊢𝐴 ≤𝐵definition.v
typing E e A Γ ⊢ 𝑒 : 𝐴
definition.v
step e1 e2
𝑒 1 ↩→ 𝑒 2

Definitions

Simply Typed Lambda Calculus (STLC) with iso-recursive types. The folder src includes all theCoq proofs about STLC extended with iso-recursive subtyping, which is the calculus describedin Sections 3, 4 and 5. All the definitions in the paper can be found in files Rules.v, AmberBase.v
and NominalUnfolding.v. Table 2 shows the correspondence of definitions between the paper andthe Coq artifacts. The file Rules.v contains the definitions for our type system. It has definitionsof well-formedness, subtyping (both finite and double unfoldings), typing, and reduction. The fileAmberBase.v, contains the definitions for the Amber rules and the intermediate subtyping relation
based on a weakly positive restriction presented in Section 5. The file NominalUnfolding.v contains
all the definitions and proofs involving nominal unfoldings, expect for the decidability proof, whichis contained in file Decidability.v.
For encoding variables and binders, we use the locally nameless representation to express all
the types and terms. In the paper, we use only substitution to represent unfolding of a recursive
type. In the Coq proof, due to the use of the locally nameless representation, we also use of opening
operation on pre-terms [Aydemir et al. 2008]. Furthermore, in the paper, we always use the same
notation for well-formedness with rule wft-rec, rule wft-inf, rule wft-recur and rule wftnominal. In the Coq formalization, we have four distinct definitions of well-formedness, which areproved to be equivalent.
Simply Typed Lambda Calculus (STLC) with iso-recursive types and record types. The folder
src_extension includes all the Coq proofs about STLC with iso-recursive subtyping and record types,
which corresponds to the calculus in Section 6. The folder structure is similar, except that we movethe unfolding lemma to a new file named unfolding.v. All the definitions in the paper can be foundin files definition.v. Table 3 shows the correspondence of definitions between the paper and the
Coq artifacts.
7.2

Lemmas and Theorems

Table 4 shows the descriptions for all the proof scripts in Section 3, Section 4 and Section 5. For
succinctness, we briefly describe all the lemmas and theorems, annotating them with related
subtyping formulation inside the brackets. In Table 4, Finite represents our specification, Double
represents the double unfolding rule, Nominal represents the nominal unfolding rule, Positive
represents the weakly positive subtyping, and Amber represents the Amber rules.
Table 5 shows the descriptions for all the proof scripts in Section 6.
An important difference between some of the lemma statements in the paper and the Coq
proofs is that we make more use of modes in Coq. This change is done for readability purposes.
In particular, all variants of the unfolding lemma in the paper are presented without modes in
the paper. Figure 15 illustrates the difference between the formulations with and without modes
6 https://github.com/plclub/metalib. Note that currently (February 2022), Metalib library only supports Coq (<=8.10), thus

some modifications are needed. More precisely, all omega tactics should be replaced by lia tactics.
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:47

Table 4. Descriptions for the proof scripts.

Theorems
Theorem 5
Theorem 6
Lemma 8
Theorem 11
Theorem 12
Theorem 15
Theorem 16
Theorem 17
Theorem 21
Lemma 24
Theorem 25
Theorem 26
Lemma 27
Theorem 30
Theorem 31
Corollary 32
Corollary 33
Theorem 36
Theorem 39
Theorem 41
Lemma 42
Theorem 45
Theorem 49
Corollary 50
Theorem 52
Theorem 55
Corollary 57
Corollary 58
Corollary 59

Description
Reflexivity (Finite)
Transitivity (Finite)
Unfolding lemma (Finite)
Preservation
Progress
Reflexivity (Double)
Transitivity (Double)
Completeness (Double)
Soundness (Double)
Unfolding lemma (Double)
Reflexivity (Nominal)
Transitivity (Nominal)
Unfolding lemma (Nominal)
Nominal to Double
Double to Nominal
Soundness (Nominal)
Completeness (Nominal)
Decidability
Reflexivity (Positive)
Transitivity (Positive)
Unfolding lemma (Positive)
Amber to Positive
Positive to Double
Soundness (Amber)
Double to Positive
Positive to Amber
Completeness (Amber)
Transitivity (Amber)
Unfolding lemma (Amber)

Files (in src/ folder)
FiniteUnfolding.v
FiniteUnfolding.v
FiniteUnfolding.v
Typesafety.v
Typesafety.v
FiniteUnfolding.v
FiniteUnfolding.v
FiniteUnfolding.v
DoubleUnfolding.v
DoubleUnfolding.v

Name in Coq
refl
Transitivity
unfolding_lemmapreservation
progress
refl_algotrans_algo
completenesssoundness
unfolding_lemma_version2

NominalUnfolding.v
NominalUnfolding.v
NominalUnfolding.v

Nominal.sub_refl
Nominal.Transitivity
Nominal.unfolding_lemma

NominalUnfolding.v
NominalUnfolding.v
NominalUnfolding.v
NominalUnfolding.v
Decidability.v
AmberBase.v
PositiveBase.v
PositiveBase.v

nominal_to_double
double_to_nominal
nominal_to_finite
finite_to_nominal
decidability
sub_amber2_refl
sub_amber2_transunfolding_for_pos

AmberBase.v
AmberSoundness.v
AmberSoundness.v
PositiveSubtyping.v
AmberCompleteness.v
AmberCompleteness.v
AmberCompleteness.v
AmberCompleteness.v

sub_amber_to_amber_2
sub_amber_2_to_sub
amber_soundness2
sub_to_amber2
amber_complete_aux
amber_complete2
amber_transitivity
amber_unfolding

for the unfolding lemma (note that the premise (2) is redundant since it is the inversion of thepremise (3), thus in the Coq code we drop this premise while in the paper presentation we keep it
for readability). Our Coq formalization uses some meta-functions on modes instead to formalize
the same result. Using meta-functions on modes (Definition 68), the same lemma would look likethe right part of Figure 15.
Definition 68. Mode selector.
𝐶 ⊕+ 𝐷 = 𝐶

𝐶 ⊕− 𝐷 = 𝐷

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:48

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Table 5. Descriptions for the proof scripts (complement).

Theorems
Description
Theorem 60 Reflexivity
Theorem 61 Transitivity
Lemma 64
Unfolding lemma
Theorem 66 Preservation
Theorem 67 Progress

Files (in src_extension/ folder)
subtyping.v
subtyping.v
unfolding.v
typesafety.v
typesafety.v

Lemma 23 in paper:If(1) Γ1, 𝛼, Γ2 ⊢𝑎 𝐴 ≤ 𝐵;
(2) Γ1, 𝛼, Γ2 ⊢𝑎 𝐶 ≤ 𝐷;(3) Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤ 𝜇𝛼 . 𝐷;then(1) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐶]𝐴 ≤ [𝛼 ↦→ 𝐷]𝐵implies Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶]𝐴 ≤[𝛼 ↦→ 𝜇𝛼 . 𝐷]𝐵 and(2) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐷]𝐴 ≤ [𝛼 ↦→ 𝐶]𝐵implies Γ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐷]𝐴 ≤[𝛼 ↦→ 𝜇𝛼 . 𝐶]𝐵.

Name in Coq
sub_refl
Transitivity
unfolding_lemmapreservation
progress

Lemma 23 in Coq:If(1) Γ1, 𝛼, Γ2 ⊢𝑎 𝐴 ≤ 𝐵;
(2) Γ1, Γ2 ⊢𝑎 𝜇𝛼 . 𝐶 ≤ 𝜇𝛼 . 𝐷;(3) Γ1, 𝛼, Γ2 ⊢𝑎 [𝛼 ↦→ 𝐶 ⊕𝑚 𝐷]𝐴 ≤ [𝛼 ↦→ 𝐷 ⊕𝑚 𝐶]𝐵thenΓ1, Γ2 ⊢𝑎 [𝛼 ↦→ 𝜇𝛼 . 𝐶 ⊕𝑚 𝐷]𝐴 ≤ [𝛼 ↦→ 𝜇𝛼 . 𝐷 ⊕𝑚 𝐶]𝐵

Fig. 15. Comparison between paper and Coq statements for Lemma 23.

In the Coq proof, we also defined some special notations for definitions representing 𝑛-times
finite unfolding, and for the meta-functions on modes. Those definitions can be found in the file
Rules.v.
Another important difference is in the decidability proof. Unlike the paper proof, where in thecontext we store the variable names as keys, in the Coq proof we employ De Bruijn indices torepresent all recursive variables stored in the context.
7.3

Alternative Weakly Positive Subtyping

During the proof of completeness of Amber rules, we found that the built-in reflexivity in the
weakly positive subtyping disturbs the computation of position allocation for recursive types. Thus,in the mechanized proof, we use an alternative (Definition 69) for weakly positive subtyping tocompute the mode more precisely: the default positive mode for equal recursive types.
The key idea is to unify rule PosRes-self and rule PosRes-rec into one rule, then we “hide” theproblematic reflexivity subtly by rule PosRes-recalt:
Definition 69. An alternative rule for checking if two recursive types are subtypes in weakly
positive subtyping:
PosRes-recalt

Γ, 𝛼 ⊢ A ≤+ B

𝛽 is fresh𝛽 ∈+ 𝜇𝛼 . A ≤ 𝜇𝛼 . BΓ ⊢ 𝜇𝛼 . A ≤+ 𝜇𝛼 . B
Denoting Γ ⊢𝑢 𝐴 ≤+ 𝐵 as the weakly positive subtyping with the alternative rule PosRes-recalt
for recursive types, we show that it has same expressiveness as the original definition of weakly
positive subtyping (Figure 11):
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:49

Lemma 70. The two representations of weakly positive subtyping are equivalent:Γ ⊢𝑢 𝐴 ≤+ 𝐵 ⇔ Γ ⊢ 𝐴 ≤+ 𝐵.
7.4

Variable Generation

Another difficulty worth mentioning is generating a bundle of variables in Definition 53. Suchdefinition actually does two things: (1) generate a set of fresh variables; (2) match every fresh
variable with an existing variable. This is a bit involved in Coq.
File src/AmberCompleteness.v gives the details showing how to solve this issue. We iterate eachvariable (denote as 𝛼) in context Γ, generate a fresh variable 𝛽 and store both variables. One
possibility is that the name of 𝛼 might be used in previous stored set of variables. In that case,
we generate one more fresh variable and store it. After that, we have a set of mixed variables
containing all variables in context Γ and the number of new fresh variables is the same as the sizeof context Γ. All the variables in the set are distinct. Then we filter variables that belong to Γ andmatch them with variables in Γ one by one. Finally, we have a valid ⟨Γ⟩, as Definition 53 describes.
8

DISCUSSION AND RELATED WORK

Throughout the paper we have already discussed some of the closest related work in detail. In thissection we discuss other work on recursive subtyping.
Iso-recursive Amber rules. In Sections 2 and 5, we discussed Amadio and Cardelli [1993]’s workon recursive types. Their work is about equi-recursive types, which is enabled by a very expressive
equivalence relation used in their reflexivity rule. Much of the follow-up work has employed amuch weaker alpha-equivalence relation in the Amber rules, leading to an iso-recursive formulationof subtyping.
With respect to the metatheory of iso-recursive subtyping with the Amber rules, Bengtson et al.
[2011]’s work is the closest to ours. They manually proved a full set of type safety properties,
including the transitivity lemma for subtyping and the unfolding lemma (as a part of their inversion
lemma). The transitivity lemma, “perhaps the most difficult” statement in their work, is proven witha complex inductive argument. For example, a subtyping chain of type variables, 𝛼 1 ≤ 𝛼 2 ≤ 𝛼 3 , isaccepted by their transitivity statement, by means of adapting variable bindings in the contexts
accordingly:Γ[𝛼 1 ≤ 𝛼 2 ] ⊢ 𝛼 1 ≤ 𝛼 2
Γ[𝛼 2 ≤ 𝛼 3 ] ⊢ 𝛼 2 ≤ 𝛼 3
Γ [𝛼 1 ≤ 𝛼 3 ] ⊢ 𝛼 1 ≤ 𝛼 3
In other words, the subtyping judgments of their transitivity statement (used for their proof) do notshare the same context, which subtly captures the nature of context elements (𝛼 ≤ 𝛽) in the Amber
rules. Such technique involving inconsistent contexts is an uncommon practice, and it complicatesthe proof. Backes et al. [2014] attempted to formalize this transitivity proof in Coq, but they failed,stating that: "The soundness of the Amber rule (Sub Rec) is hard to prove syntactically – in particularproving the transitivity of subtyping in the presence of the Amber rule requires a very complicatedinductive argument, which only works for “executable” environments”.
Many other works avoid some of the complexity in the metatheory of the Amber rules by
employing a declarative subtyping relation with transitivity built-in [Abadi and Cardelli 1996;
Cardone 1991; Duggan 2002; Lee et al. 2015; Pottier 2013]. However, this leaves open the question of
how to obtain a sound and complete algorithmic formulation, which as discussed in Sections 2 and5, is non-trivial. Chugh [2015] observes the lack of some desirable properties (such as decidability)and difficulties of implementing languages modelling foundational aspects of Object-Oriented
Programming when employing calculi with equi-recursive types. To address those difficulties
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:50

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

he proposes a source calculus with iso-recursive types using the Amber rules, which enables
decidability. He does not discuss transitivity of subtyping for the source calculus. Type-safety ofthe source calculus is shown via an elaboration into a target calculus with equi-recursive types
and F-bounded polymorphism [Canning et al. 1989]. In general, those works employ elaboration
and/or coercive subtyping, which leads to an alternative way to prove type-safety, and transitivity
is either built-in or not discussed. In contrast, our metatheory comes with transitivity proofs, aswell as a direct operational semantics for a calculus with iso-recursive types.
Complete Iso-Recursive Subtyping. Ligatti et al. [2017] propose an improvement to the Amber
rules for iso-recursive subtyping. They observe that the Amber rules are sound, but incompletewith respect to type-safety. Besides the complications due to the presence of a reflexivity rule, theyfind that a source of incompleteness of the Amber rules comes from complications with recursivetype unrolling. The two rules for subtyping recursive types employed by Ligatti et al. are:𝑆, 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵 ⊢ [𝛼 ↦→ 𝜇𝛼 . 𝐴] 𝐴 ≤ [𝛽 ↦→ 𝜇𝛽. 𝐵] 𝐵
L17-rec1
𝑆 ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵(𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵) ∈ 𝑆
L17-rec2𝑆 ⊢ 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵
The basic idea is that subtyping environments 𝑆 track all subtyping relations between recursive
types that have already been observed. Rule L17-rec1 is the rule that is triggered if 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵
has not been observed yet. In that case 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵 is simply added to the environment and therecursive type variables are directly replaced by the recursive types in the bodies. In rule L17-rec2,
if 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵 is already in the environment, then we know that the two recursive types are in a
subtyping relation and we can terminate. One similarity to the double unfolding and the nominal
unfolding rules is that both Ligatti et al.’s rules and our rules employ one substitution for each type.
However, in Ligatti et al.’s rules we substitute the recursive type variable with the recursive typedirectly, whereas in our rules we use a finite unfolding: that is we use the body of the recursivetype instead. Ligatti et al.’s rules are more powerful than both the Amber rules and all the rules
presented in this paper, including our declarative formulation with finite unfoldings, as well as the
double and nominal unfolding rules. The simplest example that illustrates the different expressive
power between our rules and the rules by Ligatti et al. [2017] is perhaps 𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼). With
Ligatti et al.’s rules this is a valid subtyping statement, as illustrated by the following derivation:
𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼) ∈ {𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼), 𝜇𝛼 . 𝛼 ≤ 𝜇𝛽. (𝜇𝛼 . (𝜇𝛽. 𝛼))}L17-rec2
𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼), 𝜇𝛼 . 𝛼 ≤ 𝜇𝛽. (𝜇𝛼 . (𝜇𝛽. 𝛼)) ⊢ 𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼)L17-rec1
𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼) ⊢ 𝜇𝛼 . 𝛼 ≤ 𝜇𝛽. (𝜇𝛼 . (𝜇𝛽. 𝛼))
L17-rec1⊢ 𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼)
In contrast, the rules based on finite unfoldings reject such subtyping statement. For instance, hereis the failed derivation with the double unfolding rules:
Derivation fails here
Derivation fails here𝛼 ⊢ 𝛼 ≤ 𝜇𝛽. 𝛼
𝛼 ⊢ 𝛼 ≤ 𝜇𝛽. (𝜇𝛽. 𝛼)SA-rec⊢ 𝜇𝛼 . 𝛼 ≤ 𝜇𝛼 . (𝜇𝛽. 𝛼)The source of the difference in terms of expressive power between our rules (as well as the Amber
rules) and Ligatti et al.’s rules is related to the treatment of subtyping between type variables
and recursive types. In the failed derivation with the double unfolding rule we can see that thederivation fails when we encounter a subtyping statement of the form 𝛼 ≤ 𝜇𝛽. 𝐴. That is when wetry to compare a recursive type variable with a recursive type. In both our rules and the Amber
rules, such statements are always rejected, since the recursive type variables are opaque and the
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:51

structure of the recursive type denoted by the type variable is not known. In some sense with theAmber rules and our rules recursive type variables act similarly to nominal types, and comparing
them with a recursive type that happens to have a structurally compatible shape will fail. In Ligatti
et al.’s rules, because type variables are always replaced by the recursive type, the structure of therecursive type is known (or transparent) and then the subtyping rules for recursive types can beused instead. In addition to the simple example that we describe above, Ligatti et al. [2017] haveidentified two larger examples that demonstrate that their rules can derive subtyping statementsthat the Amber rules cannot:• 𝜇𝑛.{sub : (𝜇𝑖 ′ .{sub : 𝑖 ′ → unit}) → unit, min : unit → int} ≤ 𝜇𝑖.{sub : 𝑖 → unit};• 𝜇𝑎.(((𝜇𝑏.((𝑏 + nat) + 𝑎)) + nat) + 𝑎) ≤ 𝜇𝑐.((𝑐 + real) + 𝑐).
As they observe, accepting such subtyping statements does not violate type-safety. The two examples
above are also rejected by our rules, for similar reasons to the simpler example above. The failure
to derive such subtyping statements is expected since we proved that our rules are equivalent interms of expressive power to the Amber rules, which reject them as well.
In addition to rules L17-rec1 and L17-rec2, some non-standard subtyping rules for valueuninhabited types are also needed for achieving the completeness of subtyping with respect to typesafety. If a type is value-uninhabited then every expression of that type diverges. In other words,
value-uninhabited types are treated as bottom types (⊥). As Ligatti et al. explained, if we do notcare about subtyping completeness with respect to type-safety, we can ignore the extra subtyping
rules for value-uninhabited types, and still get additional expressive power over the Amber rules.
From the point of view of type-safety, the new formulations of subtyping proposed by us are also
incomplete, since they have the same expressive power as the Amber rules.
Our declarative formulation of subtyping is essentially following a syntactic approach to subtyping, whereas a formulation based on completeness with respect to type-safety is closer in spirit tosemantic subtyping [Castagna and Frisch 2005]. While syntactic formulations are generally lessexpressive, their metatheory is usually simpler, and such formulations are also generally more
extensible. To achieve their goal of a complete formulation of subtyping with respect to typesafety, Ligatti et al. [2017] had to develop several new proof techniques to accomplish this goal.
For instance one of the techniques developed in their work is induction on failing derivations,which requires defining an explicit relation that captures failed derivations of subtyping. A further
complicating factor is the non-standard form of environments 𝑆 required by rules L17-rec1 andL17-rec2, which must contain entries of the form 𝜇𝛼 . 𝐴 ≤ 𝜇𝛽. 𝐵. This is in contrast to our rules,
which all employ standard environments with type variables only. Both of these mean that thesubtyping metatheory is significantly different from conventional formulations of subtyping. In
Ligatti et al.’s work, most important theorems, such as transitivity or reflexivity, are proved bydoing induction on failing derivations. For example, their transitivity theorem is proved via an
auxiliary theorem called strong subtyping transitivity of the form:𝑆 ⊢ 𝜏1 ≤ 𝜏3 is not derivable⊢ 𝜏1 ≤ 𝜏2⊢ 𝜏2 ≤ 𝜏3 is not derivable
This theorem relies on the failed derivations relation and leads to a transitivity proof that is quite
different from conventional transitivity proofs for subtyping. In contrast, our transitivity theorem(as well as other lemmas such as reflexivity) and proofs are standard. For instance, as we show in
Theorem 6, our transitivity proof is modular in the sense that proofs for the cases of non-recursivetype constructs (such as function types) are essentially the same as for a subtyping relation without
recursive types. In other words the addition of recursive types using our rules has little impact on
ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:52

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

existing proofs7 . This is not the case in Ligatti et al.’s work since their rules for recursive subtyping
as well as their proof techniques for showing completeness of subtyping with respect to type-safety
require new proof techniques and proofs, and even new theorem statements. In addition, all our
proofs have been formalized in a theorem prover, whereas Ligatti et al.’s proofs have not beenmechanically formalized yet.
Other approaches to iso-recursive subtyping. For solving the conflict between contravariant types
and recursive types, Hofmann and Pierce [1996] proposed an approach where only covariant types
are allowed. In their subtyping rules, the inputs of function types must be the same. Later, Hosoya
et al. [1998] gave an algorithm to prove transitivity and type soundness, but it still relies on acomplicated environment where all of the components are pairs of structural recursive types. Thus,
they have extra rules for contexts to obtain enough information for the subtyping assumptions.
Featherweight Java [Igarashi et al. 2001], is another calculus that supports a form of iso-recursive
types. Although there are no specific recursive type constructs, recursive types appear because
class declarations can be recursive. An advantage of the Featherweight Java design is that recursive
types are fairly easy to model, and modeling mutually recursive types is straightforward. However,structural iso-recursive types, such as those in the Amber rules, allow for nested recursive types,
which are not directly supported in Featherweight Java. Featherweight Java does support mutually
recursive classes, so perhaps there is some general way to support such nested recursive types via
an encoding.
Equi-recursive subtyping. Equi-recursive subtyping has been widely used in various calculi. Withequi-recursive subtyping a recursive type is equivalent to its unfoldings. Amadio and Cardelli[1993]’s work provided the first theoretical foundation for equi-recursive types. Subsequent workby Brandt and Henglein [1997] and Gapeyev et al. [2003] improved and simplified the theory of
Amadio and Cardelli [1993]’s study. In particular, they advocated for the use of coinduction forthe metatheory of equi-recursive subtyping. Equi-recursive types play an important role in many
areas. They have been employed for session types [Castagna et al. 2009; Chen et al. 2014; Gay andHole 2005; Gay and Vasconcelos 2010], and Siek and Tobin-Hochstadt [2016] applied equi-recursive
types in gradual typing. Dependent object types (DOT), the foundation of Scala, also considers a
special form of equi-recursive type [Amin et al. 2016; Rompf and Amin 2016]. With conventional
recursive types 𝜇𝛼 . 𝐴, 𝛼 stands for the recursive type itself. In DOT, the recursive type is of theform 𝜇 𝑡ℎ𝑖𝑠. 𝐴, where 𝑡ℎ𝑖𝑠 is the (run-time) self-reference. This construct, in combination withthe form of dependent types supported in DOT allows for interesting applications that cannot bemodelled with conventional recursive types. Nonetheless, DOT has to impose some contractivenessrestrictions on the form of the recursive types for soundness, while no such restrictions are neededwith iso-recursive types.
Mechanical formalizations with recursive subtyping. While to our knowledge there are no mechanical formalizations with the Amber rules, there are a few works trying to formalize other variantsof recursive subtyping. Closest to our work is the Coq formalization by Backes et al. [2014]. Theyshow a Coq proof for refinement types with a positive restriction for iso-recursive types. In fact,
our positive subtyping formulation (Figure 11) is close to Backes et al. [2014]’s definition. However,our definition is more general since equal types with negative recursive occurrences are considered
subtypes, whereas in their formulation recursive types with negative occurrences of recursive
variables are forbidden. Appel and Felty [2000] gave a related Twelf proof of positive subtyping,where function types are invariant with respect to the input types of functions. Recently, based on
7 Our locally nameless [Charguéraud 2011] based Coq proofs follow a similar style to Chargueraud’s proofs for System 𝐹in https://www.chargueraud.org/softs/ln.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

<:

Revisiting Iso-Recursive Subtyping

1:53

big-step semantics, Amin and Rompf [2017] gave a formalization of DOT, which employs a special
form of equi-recursive type. Danielsson and Altenkirch [2010], mixes induction and coinduction
for proving properties of equi-recursive subtyping in Agda.
9

CONCLUSION

The Amber rules have been around for many years. They have been adapted and widely employed
for iso-recursive formulations of subtyping. However, the metatheory of Amber-style iso-recursive
subtyping is not very well understood. In this work, we revisit the problem of iso-recursive subtyping
and come up with novel declarative and algorithmic formulations of subtyping. We pay special
attention to the metatheory, which is fully formalized in the Coq theorem prover. We believe that
our work significantly improves the understanding of iso-recursive subtyping, and provides aplatform for further developments in this area. More practically, the double unfolding rule andnominal unfolding rule are easy to integrate in existing calculi and this work presents the proof
techniques needed to prove standard properties (such as transitivity and type soundness). Moreover,
we show that it is easy to employ our algorithmic subtyping rules to subtyping relations that are
not antisymmetric.
Investigating the use of our novel formulation of iso-recursive subtyping in more complex
subtyping relations is an interesting direction for future work. For instance, it will be interesting
to explore calculi with polymorphism, intersection/union types as well as calculi with bounded
quantification. Investigating optimal algorithms for Amber-style iso-recursive subtyping is also
an interesting direction for future work. Finally, another direction is to have a closer look at thealternative formulation of iso-recursive subtyping by Ligatti et al. [2017], and see whether thetechniques developed in this paper can also help with a mechanical formalization of their work.
ACKNOWLEDGMENTS
We are grateful to the anonymous OOPSLA and TOPLAS reviewers for their valuable commentsthat helped to improve the presentation of our work. John Tang Boyland provided us with valuable
feedback and he produced an alternative formalization for the calculus presented in Sections 3
and 4 in the SASyLF prover [Aldrich et al. 2008]. His SASyLF formalization is included in our
supplementary materials. We also thank Litao Zhou for his helpful discussion about the decidability
proof, that helped us finally propose a good measure for the expanded tree. This work has beensponsored by Hong Kong Research Grant Council projects number 17209519 and 17209520.
REFERENCES
Martin Abadi and Luca Cardelli. 1996. A theory of objects. Springer Science & Business Media.
Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. 1991. Explicit Substitutions. J. Funct. Program. 1, 4
(1991), 375–416.
Jonathan Aldrich, Robert J. Simmons, and Key Shin. 2008. SASyLF: an educational proof assistant for language theory. In
Functional and Declarative Programming in Education (FDPE’08). ACM, 31–40.
Roberto M Amadio and Luca Cardelli. 1993. Subtyping recursive types. ACM Transactions on Programming Languages andSystems (TOPLAS) 15, 4 (1993), 575–631.
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The essence of dependent object types.
In A List of Successes That Can Change the World. Springer, 249–272.
Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages. 666–679.
Andrew W Appel and Amy P Felty. 2000. A semantic model of types and machine instructions for proof-carrying code. In
Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 243–253.
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.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

1:54

Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira

Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2014. Union, intersection and refinement types and reasoning abouttype disjointness for secure protocol implementations. Journal of Computer Security 22, 2 (2014), 301–353.
Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. Intersection and Union Types: Syntax and
Semantics. Information and Computation 119, 2 (June 1995), 202–230.
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.
Michael Brandt and Fritz Henglein. 1997. Coinductive axiomatization of recursive type equality and subtyping, Vol. 1210.
63–81. Full version in Fundamenta Informaticae, 33:309–338, 1998.
Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John C. Mitchell. 1989. F-Bounded Polymorphism for ObjectOriented Programming. In Proceedings of the Fourth International Conference on Functional Programming Languages andComputer Architecture (Imperial College, London, United Kingdom) (FPCA 1989). 8 pages.
Luca Cardelli. 1985. Amber. In LITP Spring School on Theoretical Computer Science. Springer, 21–47.
Felice Cardone. 1991. Recursive types for Fun. Theoretical Computer Science 83, 1 (1991), 39–56.
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.
Giuseppe Castagna and Alain Frisch. 2005. A Gentle Introduction to Semantic Subtyping. In Proceedings of the 7th ACM
SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’05).
Arthur Charguéraud. 2011. The Locally Nameless Representation. Journal of Automated Reasoning (2011), 1–46.
10.1007/s10817-011-9225-2.
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.
Ravi Chugh. 2015. IsoLATE: A type system for self-recursion. In European Symposium on Programming. Springer, 257–282.
Dario Colazzo and Giorgio Ghelli. 1999. Subtyping recursive types in kernel fun. In Proceedings. 14th Symposium on Logic in
Computer Science (Cat. No. PR00158). IEEE, 137–146.
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Mathematical Logic Quarterly 27, 2-6 (1981), 45–58.
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 (PLDI ’99).
Nils Anders Danielsson and Thorsten Altenkirch. 2010. Subtyping, declaratively. In International Conference on Mathematics
of Program Construction. Springer, 100–118.
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.
Vladimir Gapeyev, Michael Levin, and Benjamin Pierce. 2003. Recursive Subtyping Revealed. Journal of Functional
Programming 12, 6 (2003), 511–548. Preliminary version in International Conference on Functional Programming (ICFP),
2000. Also appears as Chapter 21 of Types and Programming Languages by Benjamin C. Pierce (MIT Press, 2002).
Simon Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. Acta Informatica 42, 2-3 (2005), 191–225.
Simon J Gay and Vasco T Vasconcelos. 2010. Linear type theory for asynchronous session types. Journal of Functional
Programming 20, 1 (2010), 19–50.
Giorgio Ghelli. 1993. Recursive types are not conservative over F≤. In International Conference on Typed Lambda calculi andApplications. Springer, 146–162.
Martin Hofmann and Benjamin C Pierce. 1996. Positive subtyping. Information and Computation 126, 1 (1996), 11–33.
Haruo Hosoya, Benjamin C Pierce, David N Turner, et al. 1998. Datatypes and subtyping. Unpublished manuscript. Available
http://www. cis. upenn. edu/˜ bcpierce/papers/index. html (1998).
Atsushi Igarashi, Benjamin C Pierce, and Philip Wadler. 2001. Featherweight Java: a minimal core calculus for Java and GJ.
ACM Transactions on Programming Languages and Systems (TOPLAS) 23, 3 (2001), 396–450.
Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. 2015. A Theory of Tagged Objects. In European Conference on
Object-Oriented Programming (ECOOP).
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.
Benjamin C. Pierce. 2002. Types and programming languages. MIT press.
François Pottier. 2013. Syntactic soundness proof of a type-and-capability system with hidden state. Journal of functional
programming 23, 1 (2013), 38–144.
Garrel Pottinger. 1980. A type assignment for the strongly normalizable 𝜆-terms. To HB Curry: essays on combinatory logic,
lambda calculus and formalism (1980), 561–577.
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.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.

Revisiting Iso-Recursive Subtyping

1:55

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. Springer, 388–410.
Marvin Solomon. 1978. Type definitions with parameters. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on
Principles of programming languages. 31–38.
Chris Stone and Robert Harper. 1996. A Type-Theoretic Account of Standard ML 1996. Technical Report CMU-CS-96-136.
School of Computer Science, Carnegie Mellon University, School of Computer Science, Carnegie Mellon University,
Pittsburgh, PA 15213-3891.
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure
Distributed Programming with Value-Dependent Types. In Proceedings of the 16th ACM SIGPLAN International Conference
on Functional Programming (ICFP 2011).
The Coq Development Team. 2019. Coq. https://coq.inria.fr
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, and Perry Cheng. 2003. Typed Compilationof Recursive Datatypes. In Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design
and Implementation. 98–108.
Yanpeng Yang and Bruno C. d. S. Oliveira. 2019. Pure iso-type systems. Journal of Functional Programming 29 (2019).
Yaoda Zhou, Bruno C. d. S. Oliveira, and Jinxu Zhao. 2020. Revisiting Iso-Recursive Subtyping. Proc. ACM Program. Lang. 4,
OOPSLA, Article 223 (Nov. 2020), 28 pages.

ACM Trans. Program. Lang. Syst., Vol. 1, No. 1, Article 1. Publication date: January 2022.