Revisiting Iso-Recursive Subtyping
YAODA ZHOU, The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
JINXU ZHAO, 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 that we believe captures the “spirit” of Amber-style iso-recursive subtyping. Informally,
the specification states that two recursive types are subtypes if all their finite unfoldings are subtypes. The
Amber rules are shown to be sound with respect to this declarative specification. We then derive a sound,complete and decidable algorithmic formulation of subtyping that employs a novel double unfolding rule.
Compared to the Amber rules, the double unfolding rule has the advantage of: 1) being modular; 2) not
requiring reflexivity to be built in; and 3) leading to an easy proof of transitivity of subtyping. This work sheds
new insights on the theory of subtyping iso-recursive types, and the new double unfolding rule has important
advantages over the original Amber rules for both implementations and metatheoretical studies involving
recursive types. All results are mechanically formalized 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 atheorem 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, Bruno C. d. S. Oliveira, and Jinxu Zhao. 2020. Revisiting Iso-Recursive Subtyping. Proc. ACM
Program. Lang. 4, OOPSLA, Article 223 (November 2020), 28 pages. https://doi.org/10.1145/3428291

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; Bruno C. d. S. Oliveira, Department of Computer Science, The University of Hong Kong, Hong Kong,
China, bruno@cs.hku.hk; Jinxu Zhao, Department of Computer Science, The University of Hong Kong, Hong Kong, China,
jxzhao@cs.hku.hk.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2020 Copyright held by the owner/author(s).
2475-1421/2020/11-ART223
https://doi.org/10.1145/3428291

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223

223:2

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

data 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. 1. Recursive types in Haskell (left) and Java (right).

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].
Many languages adopt an iso-recursive formulation. The inconvenience of iso-recursive types ismostly eliminated by “hiding” the explicit folding and unfolding in other constructs. For example,
in functional languages, such as Haskell or ML, iso-recursive types are provided via datatypes.
Figure 1 (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 then be
defined by pattern matching. While there are no explicit folding or unfolding operations in the
program above, 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 1. 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
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].
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 [Bengtson et al. 2011; Chugh 2015; Duggan 2002; Lee et al. 2015; Swamy et al.
2011]. From this point onwards, in the context of this paper, whenever we use the term Amber
rules we refer to a subtyping relation, modelling iso-recursive subtyping, with at least the following
rules:
Γ, α ≤ β ⊢ A ≤ B
S-AmberΓ ⊢ µα . A ≤ µβ . B

α ≤β∈Γ
S-AssumptionΓ⊢α ≤βΓ⊢A≤A

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

S-ReflRevisiting Iso-Recursive Subtyping

223:3

These rules are found in nearly all the literature modelling subtyping for iso-recursive types with
the Amber rules. The first rule states that two recursive types are subtypes if their bodies are
subtypes under the assumption that the two distinct recursive variables α and β are subtypes. The
second rule states that two recursive variables are subtypes if they are related in the environment.
We also consider the reflexivity rule to be an essential part of the formulation of iso-recursive style
Amber rules for two different reasons. Without the reflexivity rule (or some similar rule) built-in,reflexivity cannot be proved. Indeed, it is well-known [Amadio and Cardelli 1993] that equal types
with negative (or contravariant) recursive occurrences cannot be shown to be subtypes without
reflexivity. A concrete example is µα . α → nat <: µα . α → nat. Secondly, the reflexivity rule is themain difference to an equi-recursive formulation employing the Amber rules. In an equi-recursive
formulation, reflexivity is replaced by a much more powerful rule that employs an equivalence
relation on types where two types are considered equal if their infinite unfoldings are equal. This
enables showing, for instance, that µα . nat → α <: µα . nat → nat → α holds in an equi-recursive
formulation, while this clearly fails if we only employ syntactic equality as in the reflexivity rule.
The Amber rules are appealing due to their apparent simplicity, but their metatheory is not wellstudied. Clearly, from an implementation point of view, the Amber rules are rather simple andeasy to implement. However, 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 a coinductive
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 Amber rules are lacking or are quite difficult to prove. In
particular, there is very little work in the literature regarding proof of transitivity for algorithmic
formulations of the Amber rules. Indeed, the only proof for transitivity that we are aware of is by
Bengtson et al. [2011]. However, the proof relies on a complex inductive argument, and attempts
to formalize the proof in a theorem prover have been unsuccessful so far [Backes et al. 2014].
Finally, a fundamental lemma that arises in proofs of type preservation for calculi with iso-recursive
subtyping is:
If µα . A ≤ µα . B then [α 7→ µα . A] A ≤ [α 7→ µα . B] B
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
a novel declarative specification that we believe captures the “spirit” of 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:Γ, α ⊢ [α 7→ A]n A ≤ [α 7→ B]n BΓ ⊢ µα . A ≤ µα . B∀n = 1 · · · ∞S-RecHere the notation [α 7→ A]n denotes the n-times finite unfolding of a type. Essentially, n times
unfolding applies n −1 substitutions to the type A, and the rule checks that all n-times unfoldings are
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:4

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

subtypes. Such a declarative formulation plays a similar role to Amadio and Cardelli’s declarative
specification for equi-recursive types. Because the specification is defined with respect to the finite
unfoldings, this naturally leads to an inductive treatment of the theory. For example, the proof oftransitivity of subtyping is fairly straightforward, with the more significant challenge being theunfolding lemma. With all the metatheory in place, proving subject-reduction for a typed lambda
calculus with recursive types is a routine exercise. Furthermore, the Amber rules are shown to besound with respect to this declarative specification.
The declarative specification of subtyping is not directly implementable because it has to consider
all finite unfoldings. Furthermore, showing completeness of the Amber rules is hindered by thecomplexities involved their formalization. Therefore, to obtain a sound, complete and decidable
algorithmic formulation, we follow a different route. We employ a novel double unfolding rule:
Γ, α ⊢ A ≤ BΓ, α ⊢ [α 7→ A] A ≤ [α 7→ B] B
S-DoubleΓ ⊢ µα . A ≤ µα . B

This rule says that for determining if two recursive types are subtypes, checking 1-time and 2-times
finite unfolding is enough. This rule accepts all valid subtyping statements that the Amber rules
accept, but it has important advantages. In particular, the rule is modular in the sense that it does
not require changes to other rules or definitions involved in subtyping. The environments are just astandard collection of type variables, and the rule for type variables is also standard. Consequently,
proofs for properties such as transitivity only need to account for the new recursive case, while
all the other cases remain essentially the same as in a subtyping relation without recursive types.
In contrast, 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. Moreover, an additional benefit isthat reflexivity does not have to be built in, but it can be derived instead. Built-in reflexivity canbe problematic in some settings, including calculi with record subtyping or intersection types.
Such calculi can have “isomorphic” subtyping where two syntactically different types A and B canbe subtypes of each other. For instance, in calculi with records, the types {x : Int, y : Bool } and{y : Bool, x : Int } are subtypes of each other. Avoiding built-in reflexivity makes the rules easier toapply in such settings. The main difficulty with the algorithmic formulation is proving soundness
with respect to the declarative specification. For getting over this difficulty, we employ an inductive
relation that captures valid subtyping subderivations.
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:
• 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 (Section 3).
• Algorithmic subtyping with the double unfolding rule: We show a sound, complete
and decidable algorithmic formulation of subtyping employing a new double-unfolding rule
(Section 4).
• Induction on subderivations: As part of the soundness proof for our algorithmic formulation we employ a novel technique of induction over subderivations of subtyping, which is
independently useful as a proof technique (Section 4).
• Soundness of the Amber rules: We prove that the Amber rules are sound with respect toour new formulation of subtyping (Section 5).
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:5• Subject-reduction for a typed lambda calculus with recursive types: To illustrate theapplicability of our results we formalize a typed lambda calculus with recursive types andprove type preservation and progress (Section 3).
• Mechanical formalization: All the results are formalized in the Coq theorem prover andcan be found at: https://github.com/juda/Iso-Recursive-Subtyping
2

OVERVIEWThis section provides an overview of the problem of iso-recursive subtyping and our approach. We
first 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 double unfolding rule.
2.1

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 µα . A usually contains
itself as a subpart, represented by the type variable α. Therefore, a subtyping relation (or otherform 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 A, B, C, or
D may refer to the primitive nat type, the top type ⊤, a function type A → B, a type variable α or arecursive type µα . A. The subtyping relations for the top type, primitive types and function types
are standard:
B 1 ≤ A1A2 ≤ B 2A≤⊤nat ≤ nat
A1 → A2 ≤ B 1 → B 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, including• µα . α → α ≤ µα . α → α,
• µα . α → nat ≤ µα . α → nat,
• µα . nat → α ≤ µα . nat → α.
An important aspect to pay attention 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 come back to this point in Section 2.4.
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, A → nat ≤ A → ⊤ holds for any
type A. But that does not imply that µα . α → nat ≤ µα . α → ⊤, because the binder α on different
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:6

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

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 µα . A ≤ µα . B then [α 7→ µα . A] A ≤ [α 7→ µα . B] B
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.2

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:Γ, α ⊢ A ≤ Bα∈ΓΓ ⊢ µα . A ≤ µα . BΓ⊢α ≤α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
types and recursive type variables occurring in negative positions may allow unsound subtyping
derivations, as shown above.
2.3

The Positive Restriction Rule

To fix the unsound rule in the presence of contravariant subtyping, we might restrict it withpositivity checks on the types:
Γ, α ⊢ A ≤ B
non-neg(α, A)
non-neg(α, B)Γ ⊢ µα . A ≤ µα . B
where non-neg(α, A) is false when α occurs in negative positions of A. 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 thesubderivations which encounter α ≤ α (for some recursive type variable α) are valid. Since such
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:7

subderivations only occur in positive (or covariant) positions, the left α represents µα . A, and theright α represents µα . B. Since the subtyping is covariant, the derivation µα . A ≤ µα . B is valid,
and all subderivations α ≤ α 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.4

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 2. 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 A = B (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:µα . A = [α 7→ µα . A] A
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 syntactic equality in reflexivity, which is less powerful,
but is enough to express iso-recursive subtyping. In what follows we consider the folklore rules,
where the equality (A = B) used in rule OAmber-refl is simplified by just considering syntactic
equality. The iso-recursive rules can deal correctly with all the examples illustrated so far, accepting
the various examples that we have argued should be accepted, and rejecting the other ones. Perhaps
a small nitpicking point is the absence of well-formedness constraints in the subtyping rules.
By modern day standards, this may look a little suspicious, but then again well-formedness ofenvironments 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 come back tothis issue in Section 5. Setting the issue of well-formedness aside for the moment, the Amber rules
have some other important issues:
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:8

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

Γ⊢A≤B

(Original Amber Rules)

OAmber-refl

A=B
Γ⊢A≤B

OAmber-transΓ⊢A≤B

OAmber-assmp

Γ⊢B≤C

Γ⊢A≤C

α ≤β∈Γ

OAmber-topΓ⊢α ≤βΓ⊢A≤⊤

OAmber-arrowΓ ⊢ B1 ≤ A1
Γ ⊢ A2 ≤ B2

OAmber-rec

Γ, α ≤ β ⊢ A ≤ B

Γ ⊢ A1 → A2 ≤ B1 → B2

Γ ⊢ µα . A ≤ µβ . B

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

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.2.
The reflexivity rule, if present in the subtyping relation, depends on a specific equivalence
judgment. Simple systems might use syntactic equivalence or alpha-equivalence, yet those might
be insufficient for other systems. For example, permutation of fields on record types should beconsidered as equivalent types, thus we may accept the following subtypesµα . {x : α, y : nat } → nat ≤ µα . {y : nat, x : α } → nat
However, if the built-in reflexivity employs only alpha-equivalence, such a subtyping derivationis rejected. To fix this it is natural to define the equivalence relation by requiring two types to be
subtypes of each other. However, such definition would immediately lead to a circular dependency
for recursive types. Therefore, one would need to explicitly define a reasonable set of equivalencerules (e.g. including alpha-equivalence and field permutations), with the sacrifice of simplicity andextensibility of a subtyping relation. The reader may refer to work from Ligatti et al. [2017] for amore extended discussion on the complications of having the reflexivity rule built-in.
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

α 1 ≤ α 2, α 2 ≤ α 3 ⊢ α 1 ≤ α 3

does not hold!

Such 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.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:9

Proofs of transitivity and other lemmas are hard. A related problem is proving that transitivityof an algorithmic system 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 rules withtransitivity built-in [Cardone 1991; Lee et al. 2015; Pottier 2013]. The only proof that we are awareof 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, and it requires a “very complicatedinductive argument”. Thus, they finally adopt the positive restriction, as we discussed in Section 2.3.
We also tried to directly prove some of these properties in Coq with variations 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 proofs.
2.5

Our Solution: A New Declarative Specification and the Double Unfolding Rule

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. Therefore, to provide a
detailed account of the metatheory for iso-recursive subtyping we propose alternative definitions(both declarative and algorithmic) for subtyping of recursive types. The new formulation of subtyping has 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 prove that the Amber rules are sound 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.2. 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?
The answer to this question is yes! Let us have a second look at the unsound counter-example
that was presented in Section 2.2:
µα . α → nat ≤ µα . α → ⊤As we have argued, this subtyping statement should fail because unfolding the recursive typetwice leads to an invalid subtyping derivation. However, with the 1-time finite unfolding used by
the rules in Section 2.2, all that is checked is whether α ⊢ α → nat ≤ α → ⊤ holds. Since suchderivation does indeed hold, the rule unsoundly accepts µα . α → nat ≤ µα . α → ⊤. The problem
is that while the 1-time unfolding works, other n-times unfoldings do not. Therefore, an idea is tocheck whether other n-times unfoldings work as well to recover soundness.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:10

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

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 n-times finite
unfoldings are subtypes for any positive integer n:Γ, α ⊢ [α 7→ A]n A ≤ [α 7→ B]n BΓ ⊢ µα . A ≤ µα . B∀n = 1 · · · ∞S-RecIn comparison to the rules showed in Section 2.2, our subtyping rule S-rec has a stricter condition,by checking the subtyping relation for all n-times finite unfoldings, instead of only the 1-time finite
unfolding. Such restriction eliminates the false positives on contravariant recursive types. The
definition of n-times finite unfolding used in the rule is as follows:
Definition 1 (n-times finite unfolding).
[α 7→ A]n B := [α 7→ A][α 7→ A] · · · [α 7→ A] B|{z}(n−1) times

By definition, [α 7→ A]n A is the n-times finite unfolding of µα . A. In other words, we execute (n − 1)times substitution of its body to itself. For example, [α 7→ A]1A = A, [α 7→ A]2 A = [α 7→ A] A,[α 7→ A]3 A = [α 7→ A][α 7→ A] A, etc. We also slightly generalize the definition, to unfold a type
B with another type A multiple times. This generalization is mainly used for proofs.
Algorithmic Subtyping. An infinite amount of conditions is impossible to check algorithmically.
However, it turns out that we only need to check 1-time and 2-times finite unfoldings to obtainan algorithmic formulation that is sound, complete and decidable with respect to the declarative
formulation of subtyping. We can informally explain why 1-time and 2-times finite unfoldings areenough by looking again at the counter-example. 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:
Γ, α ⊢ A ≤ BΓ, α ⊢ [α 7→ A] A ≤ [α 7→ B] B
S-DoubleΓ ⊢ µα . A ≤ µα . B
As a final note, 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 derivation 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.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping
3

223:11A 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
A, B, C, D
Expressions e
Valuesv
Contexts
Γ

F
F
F
F

nat | ⊤ | A1 → A2 | α | µα . A
x | i | e 1 e 2 | λx : A. e | unfold [A] e | fold [A] ei | λx : A. e | fold [A] v· | Γ, α | Γ, x : A

Meta-variables A, B, C, D range over types. These types consist of: natural numbers (nat), thetop type (⊤), function types (A → B), type variables (α) and recursive types (µα . A). Expressions,denoted as e, include: natural numbers (i), applications (e 1 e 2 ), lambda expressions (λx : A. e). The
expression unfold [A] e is used to unfold the recursive type of an expression e; while fold [A] e
is used to fold the recursive type of an expression e. Some expressions are also values: natural
numbers (i), lambda expressions (λx : A. e) as well as fold expressions (fold [A] v) if their inner
expressions are also values. The context is used to store variables with their type and type variables.
Well-Formedness. The definition of a well-formed environment ⊢ Γ is standard, ensuring that all
variables in the environment are distinct. The top of Figure 3 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-rec states that if the body of a recursive type is well-formed
under an extended context then the recursive type is well-formed.
3.2

Subtyping

The bottom of Figure 3 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 wellformed type A 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 the 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 most significant: it tells us that a recursive type µα . A is a subtype ofµα . B, if all their corresponding finite unfoldings are subtypes. Both [α 7→ A]n A and [α 7→ B]n B
are used to denote n-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 a suitable
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:12

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

Γ⊢A

(Well-formed Type)wft-varwft-arrowΓ ⊢ A1

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

wft-recΓ ⊢ A2Γ, α ⊢ A

Γ ⊢ A1 → A2Γ⊢A≤BΓ ⊢ µα . A(Declarative subtyping)S-arrow
S-nat

⊢Γ

⊢Γ

Γ ⊢ nat ≤ natΓ ⊢ B1 ≤ A1
Γ ⊢ A2 ≤ B2

S-var

S-top

Γ⊢A

⊢Γ

Γ⊢A≤⊤

α∈Γ

Γ⊢α ≤αΓ ⊢ A1 → A2 ≤ B1 → B2

S-rec

Γ, α ⊢ [α 7→ A]n A ≤ [α 7→ B]n B∀n = 1 · · · ∞Γ ⊢ µα . A ≤ µα . B
Fig. 3. Well-formedness and subtyping rules.

induction principle. A first idea to prove both reflexivity and transitivity is to use induction 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 hypothesis that we
get from rule wft-rec gives us a statement that works on 1-time finite unfoldings, whereas in thesubtyping 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

Γ, α ⊢ [α 7→ A]n A ∀n = 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 Γ ⊢ A ≤ B then ⊢ Γ and Γ ⊢ A and Γ ⊢ B.
Thanks to our standard context, the proofs of both reflexivity, 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 4. Reflexivity.
If Γ ⊢ A then Γ ⊢ A ≤ A.
Theorem 5. Transitivity.
If Γ ⊢ A ≤ B and Γ ⊢ B ≤ C then Γ ⊢ A ≤ C.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:13

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. This lemma
plays a crucial role in the proof of type preservation as we shall see in Section 3.5. However, thelemma cannot be proved directly: we need to prove a generalized lemma first.
Lemma 6. If(1) Γ, α ⊢ A ≤ B;
(2) Γ ⊢ µα . C and Γ ⊢ µα . D;(3) Γ, α ⊢ [α 7→ C]n A ≤ [α 7→ D]n B holds for all n,then Γ ⊢ [α 7→ µα . C] A ≤ [α 7→ µα . D] B.
Proof. Induction on Γ, α ⊢ A ≤ B. Cases rules S-nat, S-top, and S-arrow are simple.
• Rule S-var. Assume that both A and B are variable β. If β , α, then the goal is proven directly.
Otherwise, the third premise is still Γ, α ⊢ [α 7→ C]n α ≤ [α 7→ D]n α, where n is arbitrary.
The goal becomes Γ ⊢ µα 1 . C ≤ µα 1 . D. Then apply the rule for recursive types. The goal isequal to the third premise after alpha-conversion.
• Rule S-rec. Assume the A’s shape is µα 1 . A′ and B’s shape is µα 1 . B ′. Then the third premise
becomes Γ, α ⊢ [α 7→ C]n µα 1 . A′ ≤ [α 7→ D]n µα 1 . B ′, which can be rewritten to Γ, α ⊢µα 1 . [α 7→ C]n A′ ≤ µα 1 . [α 7→ D]n B ′. The goal becomes Γ ⊢ [α 7→ µα 2 . C] µα 1 . A′ ≤ [α 7→µα 2 . D] µα 1 . B ′, which can be rewritten to Γ ⊢ µα 1 . [α 7→ µα 2 . C] A′ ≤ µα 1 . [α 7→ µα 2 . D] B ′.
By induction hypothesis, this goal is proven.
□
Lemma 6 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 A = C and B = D, one
easily obtains the unfolding lemma.
Lemma 7. Unfolding Lemma.
If Γ ⊢ µα . A ≤ µα . B then Γ ⊢ [α 7→ µα . A] A ≤ [α 7→ µα . B] B.
3.4

Typing and Reduction Rules

Typing rules. As the top of Figure 4 shows, the typing rules are quite standard. Noteworthy are
the rules involving recursive types. Rule typing-unfold reveals that if e has type µα . A then, after
unfolding, its type becomes [α 7→ µα . A] A. Rule typing-fold says if e has type [α 7→ µα . A] A,
after folding, its type becomes µα . A, with an additional type well-formedness check on µα . A. 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 4 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 A and B are not necessary 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.
Firstly, we need a conventional substitution lemma to deal with beta reduction in preservation:
Lemma 8. Substitution lemma. If Γ1, x : B, Γ2 ⊢ e : A and Γ2 ⊢ e ′ : B then Γ1, Γ2 ⊢ [x 7→ e ′] e : A.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:14

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

typing-var

typing-sub

⊢Γ

Γ⊢e:A

⊢Γ
Γ ⊢ i : nat

x :A∈Γ
Γ⊢x:A

typing-abs

Γ⊢A≤B

Γ⊢e:B

typing-app

Γ ⊢ e1 : A1 → A2
Γ ⊢ e2 : A1
Γ ⊢ e1 e2 : A2

Γ, x : A ⊢ e : A2
Γ ⊢ λx : A. e : A1 → A2
typing-foldΓ ⊢ e : µα . AΓ ⊢ e : [α 7→ µα . A] AΓ ⊢ µα . AΓ ⊢ unfold [µα . A] e : [α 7→ µα . A] AΓ ⊢ fold [µα . A] e : µα . Atyping-unfold

e 1 ,→ e 2(Reduction)
step-appl
step-beta(λx : A. e1 ) v2 ,→ [x 7→ v2 ] e1

e1 ,→ e1′e2 ,→ e2′

e1 e2 ,→ e1′ e2

v1 e2 ,→ v1 e2′

step-unfold
step-fld

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

step-appr

step-fold

e ,→ e′e ,→ e′unfold [A] e ,→ unfold [A] e′

fold [A] e ,→ fold [A] e′

Fig. 4. Typing and Reduction Rules

Then we can proceed to the preservation and progress theorems.
Theorem 9. Preservation.
If Γ ⊢ e : A and e ,→ e ′ then Γ ⊢ e ′ : A.
Proof. By induction on Γ ⊢ e : A. Other cases are trivial, except for• Rule typing-app. In this case, e is decomposed into e 1 → e 2 . By inversion of (e 1 → e 2 ) ,→ e ′,we will get three sub-cases. Two of them are trivial, and for rule step-beta, Lemma 8 helps
finish the case.
• Rule typing-unfold. In this case, e is decomposed into unfold [α . A] e. By inversion, we will
get two sub-cases. Case rule step-unfold is trivial. As for case rule step-fld, we do inversion
again, raising two sub-cases (rule step-fold and rule step-fld). The former one is trivial. In
latter case, we have premises Γ ⊢ fold [A] v : B, Γ ⊢ B ≤ µα . C and goal Γ ⊢ v : [α 7→ µα . C] C.
Doing induction on Γ ⊢ fold [A] v : B, by unfolding lemma (Lemma 7), we obtain a type C ′such that Γ ⊢ v : [α 7→ µα . C ′] C ′ and Γ ⊢ [α 7→ µα . C ′] C ′ ≤ [α 7→ µα . C] C. By applying
rule typing-sub, we prove our goal.
□
Theorem 10. Progress.
If ⊢ e : A then e is a value or exists e ′, e ,→ e ′ .
4

ALGORITHMIC SUBTYPING WITH THE DOUBLE UNFOLDING RULE

In last section we introduced a declarative formulation of subtyping with recursive types. Unfortunately, such formulation is not directly implementable since the rule of subtyping for recursive
checks against an infinite number of conditions (that all finite unfoldings are subtypes). In thissection, we present a sound and complete algorithmic formulation of subtyping. This formulation
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:15Γ ⊢a A ≤ B(Algorithmic subtyping)SA-arrow

SA-nat⊢Γ⊢ΓΓ ⊢a nat ≤ natΓ ⊢a B1 ≤ A1
Γ ⊢a A2 ≤ B2

SA-varSA-topΓ⊢AΓ ⊢a A ≤ ⊤

⊢Γ

α∈Γ

Γ ⊢a α ≤ αΓ ⊢a A1 → A2 ≤ B1 → B2

SA-recΓ, α ⊢a A ≤ BΓ, α ⊢a [α 7→ A] A ≤ [α 7→ B] BΓ ⊢a µα . A ≤ µα . B

Fig. 5. Subtyping Rules for Algorithmic Type System

replaces the declarative rule S-rec by the double unfolding rule, which unfolds the recursive types
1-time and 2-times, respectively.
4.1

Syntax, Well-Formedness and Subtyping

The syntax and well-formedness of the algorithmic system share the same definition as the declarative system presented in Section 3.
Subtyping. Figure 5 shows the algorithmic subtyping judgment. All rules, except one for recursive
types, remain the same as the declarative system. In the algorithmic subtyping, two recursive types
are subtypes when: 1) their bodies are subtypes; and 2) unfolding the bodies one additional timepreserves subtyping. In other words, checking 1-time and 2-times finite unfoldings rather than all
finite unfoldings (as what rule S-rec does) 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 as the declarative system.
Lemma 11. Regularity: If Γ ⊢a A ≤ B then Γ ⊢ A and Γ ⊢ B.
Theorem 12. Reflexivity.
If Γ ⊢ A then Γ ⊢a A ≤ A.
Theorem 13. Transitivity.
If Γ ⊢a A ≤ B and Γ ⊢a B ≤ C then Γ ⊢a A ≤ C.
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 is has the same conditions of the algorithmic system (plus a few more).
Theorem 14. Completeness of algorithmic subtyping: If Γ ⊢ A ≤ B then Γ ⊢a A ≤ B.
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 Γ ⊢a A ≤ B then Γ ⊢ A ≤ B.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:16

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

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.
An overview of the key idea. The key idea to prove that 1-time and 2-times finite unfolding implies
n-times finite unfolding is to capture this informal idea formally as a lemma:Γ ⊢ A ≤ B ∧ Γ ⊢ [α 7→ A] A ≤ [α 7→ B] B ⇒ Γ ⊢ [α 7→ A]n A ≤ [α 7→ B]n B.
As we shall see this lemma is true but, unfortunately, it cannot be proved directly. The obvious
attempt would be to do induction on Γ ⊢ A ≤ B. The essential problem is that we wish to analyse
the different subcases for A and B, but we still want to use the original A and B in the substitutions.
For instance, suppose that we have A := nat → A1 → A2 and B := nat → B 1 → B 2 . Here
A1 → A2 and B 1 → B 2 are contained in the type A and B. Now consider the case for function types
Γ ⊢ A1 → A2 ≤ B 1 → B 2 , which would occur in the proof. What we would like to have is theconclusion Γ ⊢ [α 7→ A]n (A1 → A2 ) ≤ [α 7→ B]n (B 1 → B 2 ). However, what we get instead isΓ ⊢ [α 7→ (A1 → A2 )]n (A1 → A2 ) ≤ [α 7→ (B 1 → B 2 )]n (B 1 → B 2 ). Therefore it is clear that weneed some generalization of this lemma. A first idea is to generalize it as follows:⇒Γ ⊢ A ≤ B ∧ Γ ⊢ C ≤ D ∧ Γ ⊢ [α 7→ C] A ≤ [α 7→ D] BΓ ⊢ [α 7→ C]n A ≤ [α 7→ D]n B.

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

In this counter-example we choose n = 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.
Further analysis of the counter-example reveals an important problem of our first idea: the types
A and C, and B and D are completely unrelated. However, we know that they ought to have somerelationship. Indeed, we know that Γ ⊢ A ≤ B should be a subderivation of Γ ⊢ C ≤ D. This is
not the case in the counter-example. Thus, to capture such relationship precisely, we introduce a
subderivation relation:
Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ DThis relation is key to obtain a suitable generalization of the lemma, without losing the relationshipbetween A and C, and B and D. The relation states that Γ1, Γ2 ⊢ A ≤ B is a positive or negative
subderivation of Γ1 ⊢ C ≤ D. A positive subderivation is a subderivation that arises from covariant
uses of the subtyping relation. Conversely, a negative subderivation is a subderivation that arises
from contravariant uses of the subtyping relation. The polarity of the subderivation is captured by
the mode m, which can either be + or − denoting, respectively, a positive or negative subderivation.
The following 3 examples illustrate the subderivation relation:(1) Γ1, · ⊢ α ≤ α ∈+ ⊤ → α ≤ nat → α(2) Γ1, · ⊢ nat ≤ ⊤ ∈− ⊤ → α ≤ nat → α(3) Γ1, · ⊢ α → nat ≤ α → ⊤ <m ⊤ → α ≤ nat → α
The first example captures the fact that Γ1 ⊢ α ≤ α is a positive subderivation of Γ1 ⊢ ⊤ → α ≤nat → α. The second example illustrates a negative subderivation: Γ1 ⊢ nat ≤ ⊤ is a subderivationof Γ1 ⊢ ⊤ → α ≤ nat → α. Note that, because of contravariance, the nat and ⊤ types occur inProc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:17

Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ D(Subtyping Subderivation)
Der-funl

Der-refl

Γ1 ⊢ A ≤ B

Γ1, Γ2 ⊢ A1 → A2 ≤ B1 → B2 ∈m C ≤ D

Γ1, · ⊢ A ≤ B ∈+ A ≤ B

Γ1, Γ2 ⊢ B1 ≤ A1 ∈m C ≤ D

Der-funr

Der-recΓ1, Γ2 ⊢ A1 → A2 ≤ B1 → B2 ∈m C ≤ D

Γ1, Γ2 ⊢ µα . A ≤ µα . B ∈m C ≤ D

Γ1, Γ2 ⊢ A2 ≤ B2 ∈m C ≤ D

Γ1, Γ2, α ⊢ [α 7→ A]n A ≤ [α 7→ B]n B ∈m C ≤ D

α A ≤ BΓ ⊢m(Negative Subtyping)NTyp-funlΓ ⊢αm B1 ≤ A1

NTyp-funrΓ ⊢αm A1 → A2 ≤ B1 → B2

Γ ⊢αm A1 → A2 ≤ B1 → B2

Γ, α ⊢αm [α 7→ A]n A ≤ [α 7→ B]n B∀n = 1 · · · ∞NTyp-varΓ ⊢α− α ≤ αΓ ⊢αm A2 ≤ B2

NTyp-rec′′Γ ⊢αm µα . A ≤ µα . B

Fig. 6. The subtyping derivation relation and negative subtyping relation.

a different side in the subderivation. Finally, the last example shows why the previous counterexample fails to be a subderivation: it is not possible to derive that Γ1 ⊢ α → nat ≤ α → ⊤ is asubderivation of Γ1 ⊢ ⊤ → α ≤ nat → α.
An important special case of subderivations is: Γ1, Γ2 ⊢ α ≤ α ∈− C ≤ D. That is when one of thenegative subderivations of Γ1 ⊢ C ≤ D is Γ1, Γ2 ⊢ α ≤ α, for some α. In particular if C := µα . A and
D := µα . B, and Γ1, Γ2 ⊢ α ≤ α occurs in a negative subderivation of Γ1 ⊢ µα . A ≤ µα . B then wecan conclude that A = B (i.e. the two recursive types must be equal). In essence 1-time and 2-times
finite unfolding on types where α ≤ α occurs negatively will need to eventually check both thatA ≤ B and B ≤ A hold, which can only be true when A = B.
The idea of subderivations of subtyping and the special case of negative subderivations containing
Γ1, Γ2 ⊢ α ≤ α plays a fundamental role in the proof of soundness, which we explain in detail next.
Subtyping subderivation. The full definition of the subtyping subderivation relation is shownin the top of Figure 6. Note in such relation we have two contexts: Γ1 and Γ2 . Γ1 is the originalcontext for relation Γ1 ⊢ C ≤ D, and Γ2 is used to record new variables that appear in subderivations.
The rule Der-refl is the base case: if types A and B are in subtyping relation, then the derivation
tree starts from Γ1 ⊢ A ≤ B. The rule Der-funl and rule Der-funr denote the cases where thesubderivations arise from the contravariant and covariant cases of subtyping two function types,
respectively. Note that in the contravariant case (rule Der-funl) the mode is flipped. The notationm denotes a simple function that flips the mode (+ ≡ − and − ≡ +). The rule Der-rec deals withrecursive case, which is the most interesting one. If two recursive types are in subtyping relation
then unfolding the bodies n times (for some n) is a subderivation of subtyping. The subtyping
subderivation relation has the following useful (and expected) property:
Lemma 15. If Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ D then Γ1 ⊢ C ≤ D and Γ1, Γ2 ⊢ A ≤ B.
Negative subtyping. Before we finalize the discussion of the soundness lemma, we need anotherauxiliary definition for capturing the notion of negative subtyping. Negative subtyping captures
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:18

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

subtyping derivations where types contain a free variable α and the subtyping derivation Γ ⊢ α ≤ αoccurs negatively. This relation is useful to prove lemmas about subtyping with such subderivations.
The relation is shown in the bottom of Figure 6. The rule NTyp-var is the base case: a subderivationΓ ⊢ α ≤ α occurs negatively. The rule NTyp-funr states that if variable α occurs in some modem in Γ ⊢ A2 ≤ B 2 , then it occurs in Γ ⊢ A1 → A2 ≤ B 1 → B 2 in the same mode. The rule NTypfunl, similarly, states that if variable α occurs in Γ ⊢ A2 ≤ B 2 in mode m, then it occurs inΓ ⊢ A1 → A2 ≤ B 1 → B 2 in the reverse mode. The rule NTyp-rec is the rule for recursive types.
The subtyping derivation preserves the mode. The more interesting aspect of rule NTyp-rec is thatit adds a new variable α ′ to the context (which is assumed to be distinct from α). One useful lemma
about negative subtyping is:Lemma 16. (Properties of negative subtyping)(1) If Γ ⊢α+ A ≤ B and Γ ⊢ [α 7→ C] A ≤ [α 7→ D] B, then Γ ⊢ D ≤ C.
(2) If Γ ⊢α− A ≤ B and Γ ⊢ [α 7→ D] A ≤ [α 7→ C] B, then Γ ⊢ D ≤ C.
If a derivation has negative subtyping derivations of α then we know that substitutions of α will
actually be performed in matching positions in the type. Furthermore, because we know the polarity
at which Γ ⊢ α ≤ α occurs, then we can conclude that there is a subtyping relationship between
the substituted types.
Another important property of the subtyping relation is:
Lemma 17. If Γ ⊢ A ≤ B and Γ ⊢ B ≤ A then A = B.
Equipped with both negative subtyping and the subtyping subderivation relations we can prove
an important lemma:
Lemma 18. If(1) Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ D;
α A ≤ B;(2) Γ1, Γ2 ⊢m(3) α occurs in both C and D;(4) Γ2 ⊢ [α 7→ C]n C ≤ [α 7→ D]n D;(5) Γ2 ⊢ [α 7→ C] C ≤ [α 7→ D] D,
then Γ2 ⊢ [α 7→ D]n D ≤ [α 7→ C]n C.
Proof. By induction on Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ D. The cases for function and recursive types(rule Der-funl, rule Der-funr and rule Der-rec) are proven by applying hypothesis, respectively.
Thus we only talk about case rule Der-refl. In such case, we know that m := +, A = C and B = D.
Therefore, we have that Γ1 ⊢ A ≤ B. Next, apply Lemma 16 to Γ1 ⊢α+ A ≤ B, getting Γ1 ⊢ B ≤ A.
Thus, we conclude A = B by Lemma 17 and accordingly C = D. Finally, apply reflexivity.
□
Soundness, Finally! Having set up the basic infrastructure regarding the subtyping derivationand negative subtyping relations, we can finally focus on the goal of soundness. Lemma 18 is an
important lemma that covers cases appearing in the soundness lemma when we have negative
subtyping derivations. However, we still need a lemma dealing with subtyping derivations ingeneral. With the help of Lemma 18, we prove:
Lemma 19. If(1) Γ1, Γ2 ⊢ A ≤ B;
(2) Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ D;(3) α occurs in both C and D
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping(4) Γ1 ⊢ [α 7→ C]n C ≤ [α 7→ D]n D;(5) Γ1 ⊢ [α 7→ C] C ≤ [α 7→ D] D,
then(1) Γ1, Γ2 ⊢ [α 7→ C]n+1 A ≤ [α 7→ D]n+1 B(2) Γ1, Γ2 ⊢ [α 7→ D]n+1 A ≤ [α 7→ C]n+1 B

223:19when m := +;when m := −.

Now we can finally prove that 1-time and 2-times finite unfolding implies arbitrary unfolding:Lemma 20. If Γ ⊢ A ≤ B and Γ ⊢ [α 7→ A] A ≤ [α 7→ B] B then Γ ⊢ [α 7→ A]n A ≤ [α 7→ B]n B.
+.

Proof. By induction on n. For inductive step, apply Lemma 19 with C := A, D := B, Γ2 := ·, m :=□The form of Lemma 20 is close to the shape of the infinite unfolding rule (rule S-rec) in declarative
recursive types. Finally, we can prove the soundness theorem:
Theorem 21. Soundness of algorithmic subtyping.
If Γ ⊢a A ≤ B then Γ ⊢ A ≤ B.
4.4

Decidability

Our subtyping rules are syntax-directed, leading to a relatively simple proof of decidability. We
found that doing the proof/induction directly on the declarative system would lead to fewer cases in
the proof of decidability. The reason is that the algorithmic rule for recursive types has 2 premises,
whereas the declarative system has only 1. Thus, some surgical uses of soundness/completeness inthe proof were enough to make it work, while saving us from dealing with extra cases compared toa proof using the algorithmic system instead.
Theorem 22. Decidability.
If ⊢ Γ, Γ ⊢ A and Γ ⊢ B then Γ ⊢ A ≤ B or Γ ⊢ A ̸ ≤ B.
Proof. By nested induction on Γ ⊢ A and Γ ⊢ B (using the variant with rule wft-inf).
5□

SOUNDNESS OF THE AMBER RULES

This section shows a variant of the Amber rules that is sound with respect to our new formulationof subtyping. The soundness lemma implies that if two types are subtypes under the Amber rules,
they are subtypes under our new formulation. In other words our new subtyping relation is atleast as good as the Amber rules in terms of expressiveness. To establish the soundness result wehave to impose some well-formedness conditions. These conditions have been omitted in early
formulations of the Amber rules (as mentioned in Section 2.4), 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 2) there are no well-formedness
constraints. Unfortunately, defining such well-formedness constraints is not entirely trivial. Furthermore, for those interested in mechanical formalizations 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 Γ ⊢ A ≤ B then Γ ⊢ A ∧ Γ ⊢ B.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:20

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

which states that if a subtyping derivation is valid then the 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 subtypes uses two distinct type variables α
and β in the recursive types. The use of such distinct type variables is crucial feature of 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 sequence ofpairs of types α ≤ β and that the α’s are in scope on the type at the left-side of the subtyping relation(A), while the β’s are in scope on the type at the right-side of the subtyping relation (B). Sadly, thisidea is not that simple to realise. Note that in the subtyping rule of function types (rule Amberarrow), the input arguments are swapped, so without any changes on the environment the typevariables 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 in-scope changes the meaningof the environment (α ≤ β becomes β ≤ α). Trying to ensure that the α’s are only in scope in one
side of the relation, while the β’s are only in scope on the other side, turns out to be quite tricky.
Therefore, to make progress, we propose a weaker restriction in this section: we allow that both α’s
and β’s are in scope for both types. Thus, the following derivation is valid with our variant of theAmber rules: α ≤ β ⊢ α → β ≤ ⊤. In other words, we accept some subtyping derivations that one
would perhaps expect to be rejected. That is, in the Amber rules, if we have α ≤ β in Γ, we would
not expect that α and β appear on the same type. Rather we would expect that the α appears in oneof the types, and β on the other one. However, accepting such subtyping derivations is not harmful:
we can still prove the soundness 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 7 shows a set of standard Amber rules witha built-in reflexivity rule.
Well-formedness. A well-formed environment ( ⊢ ∆) requires that all pairs of variables (α ≤ β) inthe 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 derivation ofrule Amber-rec of the Amber subtyping relation, as we shall see next.
Subtyping. The subtyping relation is almost the same as the original rules by Amadio and Cardelli[1993] in Figure 2. 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 (∆ ⊢ µα . A).
5.3 Towards Soundness: A Third Subtyping Relation Based on a Positive Restriction
To prove soundness with respect to our own formulation of subtyping we create an intermediate
subtyping relation to make the proof easier. This intermediate relation, presented in Figure 8, isequivalent to the Amber rules in Figure 7. The key idea in this relation is to have two rules forrecursive types: one rule (rule PosRes-rec) only accepts positive subtyping, which is inspired bymonotonicity on recursive types [Amadio and Cardelli 1993; Appel and Felty 2000; Backes et al.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:21∆⊢A(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∆ ⊢amb A ≤ B(Amber rules)

Amber-nat

Amber-top

Amber-var

⊢∆

⊢∆

⊢∆
∆ ⊢amb nat ≤ nat∆⊢A

α ≤β∈∆∆ ⊢amb A ≤ ⊤∆ ⊢amb α ≤ βAmber-rec

Amber-self

Amber-arrow∆ ⊢amb B1 ≤ A1
∆ ⊢amb A2 ≤ B2⊢∆∆, α ≤ β ⊢amb A ≤ B∆ ⊢amb A1 → A2 ≤ B1 → B2

∆ ⊢amb µα . A ≤ µβ . B∆ ⊢ µα . A∆ ⊢amb µα . A ≤ µα . A

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

α ∈m A ≤+ B

(Positive restriction)
Posvar-vary

Posvar-nat

Posvar-topl

Posvar-topr

Posvar-varx

α ,βα ∈m nat ≤+ nat

α ∈m A ≤+ ⊤α ∈m ⊤ ≤+ A

α ∈+ α ≤ + α

α ∈m β ≤+ β

Posvar-rec

Posvar-arrowα ∈m B1 ≤+ A1
α ∈m A2 ≤+ B2

β ∈m A ≤+ B
α ∈+ A ≤ + B
α ,βPosvar-recself

α ∈m A1 → A2 ≤+ B1 → B2

β ∈m µα . A ≤+ µα . B

β ∈m µα . A ≤+ µα . A

β < f v(A)Γ ⊢ A ≤+ B

(Positive subtyping)

PosRes-nat⊢ΓΓ ⊢ nat ≤+ nat

PosRes-top

PosRes-var

PosRes-self

⊢Γ

⊢Γ

⊢Γ

Γ⊢A

Γ ⊢ A ≤+ ⊤PosRes-arrowΓ ⊢ B1 ≤+ A1α∈ΓΓ ⊢ α ≤+ αΓ ⊢ µα . AΓ ⊢ µα . A ≤+ µα . A

PosRes-recΓ ⊢ A2 ≤+ B2

Γ ⊢ A1 → A2 ≤+ B1 → B2

Γ, α ⊢ A ≤+ B

α ∈+ A ≤+ B

Γ ⊢ µα . A ≤+ µα . B

Fig. 8. Positive Subtyping Rules2014]; while the second rule (rule PosRes-self) is a reflexivity rule that accepts recursive types
with negative recursive variables as well.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:22

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

Most subtyping rules are identical to those of the Amber rules, and the only differences arerule PosRes-var and rule PosRes-rec. Rule PosRes-rec checks that the recursive type variable αsatisfies the positive restriction relation α ∈+ A ≤+ B, while maintaining the same behavior as
the Amber rules. This subtle relation may be interpreted as follows: α ∈+ A ≤+ B means 1) α ≤ αdoes not appear in subderivations of A ≤ B, or 2) α ≤ α appears in subderivations of A ≤ B only inpositive positions. For example, α ∈+ ⊤ → α ≤+ α → α holds; yet α ∈+ µβ . β → α ≤+ µβ . β → αdoes not hold, since after unfolding for several times, α’s on both sides appear on the same negative
position. The following lemma reveals an important property that relates the positive restriction to
double unfolding:Lemma 23. If α ∈m A ≤+ B and β ∈+ A ≤+ B then α ∈m [β 7→ A] A ≤+ [β 7→ B] B.
This lemma tells us that the positive restriction respects the mode on non-negative substitutions.
As a result, the positive restriction not only reflects the Amber rules but also connects to ourdouble-unfolding formulation of subtyping.
5.4

The Soundness Theorem

To show that the Amber subtyping is sound with respect to our subtyping relations, we need totranslate the environments and types of Amber rules, as they are defined under different forms inour systems.
Definition 24. Translation of environments and types from the Amber rules.
|·|=·|∆, α ≤ β | = |∆|, α(·)(A) = A(∆, α ≤ β)(A) = (∆)([β 7→ α] A)

The translation functions, | · | and (·)(A), simply drop every second variable defined in the context∆. For example, a subtyping judgment in the Amber system α ≤ β ⊢ α → ⊤ ≤ β → ⊤ is translated
to α ⊢ α → ⊤ ≤ α → ⊤.
The relationship between the Amber subtyping and our subtyping with the positive restriction
is shown by the following lemma, which is relatively straightforward:
Lemma 25. If ∆ ⊢amb A ≤ B then |∆| ⊢ (∆)(A) ≤+ (∆)(B).
We are now one step away from the soundness theorem: to prove that positive subtyping implies
double unfolding subtyping. The main difference is on rule PosRes-rec, which corresponds torule SA-rec in the double unfolding subtyping. The proof is tricky at the first glance, yet with
Lemma 23, one can derive the following lemma:
Lemma 26. If α ∈+ A ≤+ B and Γ ⊢a A ≤ B then Γ ⊢a [α 7→ A] A ≤ [α 7→ B] B.
With the above lemma, the relation between positive subtyping and the algorithmic double
unfolding subtyping is easy to establish:
Lemma 27. If Γ ⊢ A ≤+ B then Γ ⊢a A ≤ B.
Combining Lemma 25, 26 and 27, we have
Theorem 28. Soundness of the Amber rules.
If ∆ ⊢amb A ≤ B then |∆| ⊢a (∆)(A) ≤ (∆)(B).
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping
Definition
Well-formed Type (Figure 3)
Well-formed Type (Definition 2)
Declarative subtyping(Figure 3)
Typing (Figure 4)
Reduction (Figure 4)
Algorithmic subtyping(Figure 5)
Subtyping Subderivation(Figure 6)
Negative Subtyping (Figure 6)
Well-formed Type of Amber rules (Figure 7)
Amber rules (Figure 7)
Positive restriction (Figure 8)
Positive subtyping (Figure 8)

223:23Filedefinition.v

Name in formalization
WF E A

Notation in the paperΓ⊢A

definition.v

WFS E A

Γ⊢A

definition.v

Sub E A B

Γ⊢A≤B

definition.v
definition.v
definition.v

typing E e A
step e1 e2
sub E A BΓ ⊢e :Ae 1 ,→ e 2
Γ ⊢a A ≤ B

definition.v

Der m E2 A B E1 C D

Γ1, Γ2 ⊢ A ≤ B ∈m C ≤ D

definition.v

NTyp E m X A B

α A ≤ BΓ ⊢mamber_part_1.v

wf_amber E A∆⊢Aamber_part_1.v sub_amber E A B
amber_part_1.v posvar m X A B∆ ⊢amb A ≤ B
α ∈m A ≤+ B

amber_part_1.v

Γ ⊢ A ≤+ B

sub_amber2 E A B

Table 1. Paper-to-proofs correspondence guide.

Completeness. We have not proved completeness of the Amber rules with respect to our new
formulation of subtyping. However, we conjecture that this result should hold. If completenessholds then our rules and the Amber rules have the same expressive power. However, showing thecompleteness of the Amber rules (or for that matter developing any of its associated metatheory)is quite challenging, and we have not managed to work out the proper formal argument forcompleteness. The soundness result that we have for the Amber rules is more important in practicethan completeness, since it entails that a language design using our rules would not lose any
expressive power compared to the Amber rules. Completeness would be a nice result to have (if itholds), but it does not have as much practical impact.
6

COQ PROOFS

We have chosen the Coq (8.10) proof assistant [The Coq Development Team 2019] to develop ourformalization. The whole Coq formalization is built with a third-party library Metalib 1 , which
provides support for the locally nameless representation [Aydemir et al. 2008] to encode binders.
6.1

Definitions

All the definitions in the paper can be found in files definition.v and amber_part_1.v. Table 1
shows the correspondence of definitions between paper and the Coq artifacts. The file definition.v
contains the definitions for STLC with an extension of iso-recursive types. It has definitions ofwell-formedness, subtyping (both declarative and algorithmic), typing, reduction, and additionally,
negative subtyping and subtyping subderivation. The file amber_part_1.v, contains the definitions
1 https://github.com/plclub/metalib

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:24
Coq File
definition.v

infra.v
subtyping.v
typesafety.v
decidability.v
amber_part_1.v

amber_part_2.v

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

Description
The definitions of the SLTC extended
with our recursive subtyping formulation.
17
Infrastructure for locally nameless.
3, 4, 5, 6, 7, 11, 12, 13, 14, 15, 16, 18, 19, Theorems about subtyping.
20, 218, 9, 10
Theorems about type soundness.
22
Theorems showing that our recursive
subtyping is decidable.
25
Definitions of Amber rules and positive restriction. Theorems showingthat amber rules is sound w.r.t to thepositive restriction.
23, 26, 27, 28
Theorems showing that amber rules
is sound w.r.t to our subtyping formulation.
Table 2. Descriptions for the proof scripts.

for the Amber rules and the intermediate subtyping relation based on a positive restriction presented
in Section 5.
For encoding variables and binders, we use the locally nameless representation to express all
the types and terms. In 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 or rule wft-inf. In the Coq formalization, we
have two distinct definitions of well-formedness, which are proved to be equivalent. WF E A is the
one relation containing rule wft-rec, and WFS E A is the other relation containing rule wft-inf.
6.2

Lemmas and Theorems

Table 2 shows the descriptions for all the proof scripts. The theorems in Section 3 can be foundat files subtyping.v and typesafety.v, the theorems in Section 4 can be found at files subtyping.v
and decidability.v. Finally, the theorems in Section 5 can be found at files amber_part_1.v andamber_part_2.v.
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
Lemma 16, 18 and 19 are stated without modes in the paper. For example, Lemma 16 is stated in
the paper as:(1) If Γ ⊢α+ A ≤ B and Γ ⊢ [α 7→ C] A ≤ [α 7→ D] B, then Γ ⊢ D ≤ C.
(2) If Γ ⊢α− A ≤ B and Γ ⊢ [α 7→ D] A ≤ [α 7→ C] B, then Γ ⊢ D ≤ C.
but our Coq formalization uses some meta-functions on modes instead to formalize the same result.
Using meta-functions on modes (Definition 29), the same lemma would look like:α A ≤ B and Γ ⊢ [α 7→ C ⊕ D] A ≤ [α 7→ D ⊕ C] B, then Γ ⊢ D ≤ C.
If Γ ⊢mm
m
Definition 29. Mode selector.
C ⊕+ D = C

C ⊕− D = D

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:25In the Coq proof, we defined some special notations for definitions representing n-times finite unfolding, and for the meta-functions on modes. Those definitions can be found in the filedefinition.v.
7

RELATED WORK

Throughout the paper we have already discussed some of the closest related work in detail. In thissection we discuss other works on recursive subtyping.
Iso-recursive Amber rules. In Sections 2 and 5, we discussed Amadio and Cardelli [1993]’s study
about 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 a much weaker alpha-equivalence relation in the Amber rules, leading to an iso-recursive
formulation of subtyping.
With respect to the metatheory of iso-recursive subtyping Amber rules, Bengtson et al. [2011]’s
work is the closest to ours. They manually proved a full set of type safety properties, including thetransitivity 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 with a complex
inductive argument. For example, a subtyping chain of type variables, α 1 ≤ α 2 ≤ α 3 , is accepted bytheir 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 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 [Cardone 1991; Duggan 2002;
Lee et al. 2015; Pottier 2013]. However, this leaves open the question of how to obtain a sound andcomplete algorithmic formulation, which as discussed in Sections 2 and 5, 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 whenemploying calculi with equi-recursive types. To address those difficulties he proposes a source calculus with iso-recursive types using the Amber rules, which enables decidability. He does not discusstransitivity of subtyping for the source calculus. Type-safety of the source calculus is shown via anelaboration 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, as well as a direct operational semantics
for a calculus with iso-recursive types.
Other approaches to 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
incomplete with respect to type-safety. For example, the Amber rules reject µα . {l : µβ . {l : β →nat}, { f : nat → nat}} <: µα . {l : α → nat}, but such a subtyping derivation does not violate
type-safety (we assume a subtyping relation with record subtyping). Ligatti et al. [2017] propose
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:26

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

a set of subtyping rules that is both sound and complete with respect to type-safety. The new
formulation of subtyping proposed by us is also incomplete from the point of view of type-safety,
since it remains close to the Amber rules. Our declarative formulation of subtyping is essentiallyfollowing a syntactic approach to subtyping, whereas a formulation based on completeness withrespect to type-safety is closer in spirit to semantic subtyping [Castagna and Frisch 2005]. Whilesyntactic formulations are generally less expressive, their metatheory is usually simpler, and suchformulations are also generally more modular. In particular, the new rules proposed by us forrecursive subtyping are quite modular and can be added to an existing (syntactic) formulation ofsubtyping with minimal impact. In contrast, the more complete rules by Ligatti et al. [2017] requirevery specific environments for subtyping, and they also require some non-standard subtyping
rules for value-uninhabited types. In terms of metatheory, their technique of failing derivations forproving reflexivity and transitivity is non-constructive and hard to formalize in a theorem prover.
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 toprove transitivity and type soundness, but it still relies on a complicated 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 specificrecursive 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, andmodeling mutually recursive datatypes 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 the use of coinduction for themetatheory 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 and Hole
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 µα . A, α stands for the recursive type itself. In DOT, the recursive type is of theform µ this. A, where this 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 othervariants of recursive subtyping. Closest to our work is the Coq formalization by Backes et al. [2014].
They show a Coq proof for refinement types with a positive restriction for iso-recursive types.
In fact, our positive subtyping formulation (Figure 8) is close to Backes et al. [2014]’s definition.
However, our definition is more general since equal types with negative recursive occurrences are
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

Revisiting Iso-Recursive Subtyping

223:27

considered subtypes, whereas in their formulation recursive types with negative occurrences ofrecursive variables are forbidden. One subtle difference is that in their expressions syntax, unlike
ours, unfold and fold expressions do not annotate a recursive type, which avoids the need forthe unfolding lemma in the preservation proof, but it likely makes the type system undecidable.
Appel and Felty [2000] gave a related Twelf proof of positive subtyping, where function types areinvariant with respect to the input types of functions. Recently, based on big-step semantics, Aminand 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.
8

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.
There are two interesting directions for future work. One obvious direction is to investigate theuse of our novel formulation of iso-recursive subtyping in more complex subtyping relations. For
instance it will be interesting to explore calculi with polymorphism, records, and intersection andunion types. Another direction is to have a closer look at the alternative formulation of iso-recursive
subtyping by Ligatti et al. [2017], and see whether the techniques developed in this paper can also
help with a mechanical formalization of their work.
ACKNOWLEDGMENTS
We are grateful to anonymous reviewers that helped improving the presentation of our work. This
work has been sponsored by Hong Kong Research Grant Council projects number 17210617 and
17209519.
REFERENCES
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.
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.
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 (FPCA 1989). 8.
Luca Cardelli. 1985. Amber. In LITP Spring School on Theoretical Computer Science. Springer, 21–47.
Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.

223:28

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

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).
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 Languages andSystems. 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.
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.
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.
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).

Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 223. Publication date: November 2020.