Recursive Subtyping for All
LITAO ZHOU∗ and YAODA ZHOU∗ , The University of Hong Kong, China
BRUNO C. D. S. OLIVEIRA, The University of Hong Kong, China
Recursive types and bounded quanti�cation are prominent features in many modern programming languages,
such as Java, C#, Scala or TypeScript. Unfortunately, the interaction between recursive types, bounded
quanti�cation and subtyping has shown to be problematic in the past. Consequently, de�ning a simple
foundational calculus that combines those features and has desirable properties, such as decidability, transitivityof subtyping, conservativity and a sound and complete algorithmic formulation has been a long time challenge.
`
This paper presents an extension of kernel  , called  , with iso-recursive types.  is a well-known`
polymorphic calculus with bounded quanti�cation. In  we add iso-recursive types, and correspondingly
extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding
rules. We also add two smaller extensions to  . The �rst one is a generalization of the kernel  rule forbounded quanti�cation that accepts equivalent rather than equal bounds. The second extension is the use of socalled structural folding/unfolding rules, inspired by the structural unfolding rule proposed by Abadi, Cardelli,and Viswanathan. The structural rules add expressive power to the more conventional folding/unfolding
rules in the literature, and they enable additional applications. We present several results, including: type`soundness; transitivity and decidability of subtyping; the conservativity of  over  ; and a sound and```complete algorithmic formulation of  . Moreover, we study an extension of  , called  , which includes
lower bounded quanti�cation in addition to the conventional (upper) bounded quanti�cation of  . All the
results in this paper have been formalized in the Coq theorem prover.
CCS Concepts: • Theory of computation ! Type theory; • Software and its engineering ! Object
oriented languages.
Additional Key Words and Phrases: Iso-Recursive Subtyping, Bounded Polymorphism, Object Encodings
ACM Reference Format:
Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira. 2023. Recursive Subtyping for All. Proc. ACM Program.
Lang. 7, POPL, Article 48 (January 2023), 32 pages. https://doi.org/10.1145/3571241

1

INTRODUCTION

Recursive types and bounded quanti�cation are two prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Bounded quanti�cation was introduced
by Cardelli and Wegner [1985] in the Fun language, and has been widely studied [Cardelli et al.
1994; Curien and Ghelli 1992; Pierce 1994]. Bounded quanti�cation addresses the interaction between parametric polymorphism and subtyping, allowing polymorphic variables to have subtyping
bounds. Recursive types are needed in practically all programming languages to model recursive
data structures (such as lists or trees), or recursive object types in Object-Oriented Programming∗ Both authors contributed equally to this work.

Authors’ addresses: Litao Zhou; Yaoda Zhou, Department of Computer Science, The University of Hong Kong, Hong Kong,
China, ltzhou@cs.hku.hk, ydzhou@cs.hku.hk; Bruno C. d. S. Oliveira, Department of Computer Science, The University ofHong Kong, Hong Kong, China, bruno@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 pro�t or commercial advantage and that copies bear this notice andthe full citation on the �rst page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/1-ART48
https://doi.org/10.1145/3571241
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48

48:2

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira(OOP) languages to encode binary methods [Bruce et al. 1995]. For adding recursive types to alanguage with subtyping, it is desirable to have recursive subtyping between recursive types. The
�rst rules for recursive subtyping, due to Cardelli [1985], are the well-known Amber rules. Recursive
subtyping has been studied in two di�erent forms: equi-recursive subtyping [Amadio and Cardelli
1993; Brandt and Henglein 1997; Gapeyev et al. 2003], and iso-recursive subtyping [Bengtson et al.
2011; Ligatti et al. 2017; Zhou et al. 2020, 2022]. In equi-recursive subtyping recursive types andtheir unfoldings are considered to be equal. In contrast, in iso-recursive subtyping they are onlyisomorphic and explicit fold/unfold operators are necessary to witness the isomorphism.
From the mid-80s and throughout the 90s there was a lot of work on establishing the typetheoretic foundations for OOP. Both recursive subtyping, as well as bounded quanti�cation playeda major part on this e�ort. The two features were perceived to be important to model objects
in some forms of object encodings. At that time the key ideas around  [Cardelli et al. 1994;
Cardelli and Wegner 1985; Curien and Ghelli 1992], which is a polymorphic calculus with bounded
quanti�cation (but no recursive types) were reasonably well understood due to the early work on
the Fun language by Cardelli and Wegner. Therefore  -like calculi were being used in foundational
work on OOP. Some landmark papers on the foundations of OOP, which established importantresults such as the distinction between inheritance and subtyping [Cook et al. 1989], f-bounded
quanti�cation [Canning et al. 1989], or encodings of objects [Abadi et al. 1996; Bruce et al. 1999;
Cook et al. 1989], essentially assumed some  variant with recursive types. Typically, recursive
subtyping was supported via the Amber rules. However, extensions of  with recursive types had
still not been developed and formally studied when many of those works were published.
After the �rst formalization of  [Curien and Ghelli 1992], Ghelli [1993] questioned this state-ofa�airs, which implicitly assumed that the extension of  with recursive types was straightforward.
He conducted the �rst formal study for such an extension, and showed a wide range of negative
results. Most importantly, he showed that equi-recursive types are not conservative over full  . In
other words, adding equi-recursive types to full  changes the expressive power of the subtyping
relation, even when the types being compared do not involve any recursive types. The simple additionof equi-recursive types allows well-formed, but invalid subtyping statements in  to be valid in
an extension with recursive types. Ghelli also shows that applying equi-recursive types to full 
invalidates transitivity elimination: we cannot drop the transitivity rule without losing expressive
power. In addition, while subtyping in full  is undecidable [Pierce 1994], the change in expressive
power reopens questions about the decidability or undecidability of the system.
Even if we choose the weaker form of bounded quanti�cation present in Fun language andkernel  , the natural extension of Amadio and Cardelli [1993]’s algorithm to kernel  is incomplete [Colazzo and Ghelli 2005]. Nevertheless, instead of Amadio and Cardelli’s meet 2 times rules,
Colazzo and Ghelli gave an alternative meet 3 times algorithm, accompanied by a very challenging
correctness proof, showing that the subtyping relation is transitive and complete, but did notprove conservativity. Based on an earlier draft from Colazzo and Ghelli, Je�rey [2001] extended thesystem and proved it correct and complete. By transferring the polar bisimulations [Sangiorgi and
Milner 1992] technique from concurrency theory, Je�rey’s system is more general than Colazzo
4@D8
4@D8
and Ghelli’s, but it is only partially decidable. It is decidable for kernel  , but for full  , only
when the algorithm terminates it returns the correct answer, but it may not terminate. Furthermore,
4@D8
although more powerful, Je�rey’s full  is not conservative over  either.
Table 1 summarizes the results of previous work on extending  with recursive types. Note that,in the table, the Type System row simply means whether the typing relation of the  extension
with recursive types has been studied/presented in the paper. For properties such as type soundness,
decidability or conservativity, there is a corresponding entry in the table, which states whether theProc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:3

Table 1. Comparison among di�erent works.
4@D8

Transitivity
Decidability
Conservativity
Type System
Algorithmic Type System
Type Soundness
Modularity
Mechanized Proofs

1993⇥

Kernel 
2005
X
X

4@D8

⇥

⇥
⇥

⇥
⇥

4@D8


2001
X
Xr
⇥

⇥
⇥

Kernel 
2001
X
X

4@D8

8B>


1996
built-in
X

⇥
⇥

⇥

`


present work
X
X
X
X
X
X
X
X

A ⇥ symbol denotes a negative result (the property or feature does not hold). A X denotes a positive result,while Xrdenotes a partial result (such as semi-decidability). Whitespace denotes that the property/feature has
not been studied or it is unknown.

property was proved or not. Modularity here means whether the original rules and de�nitions of are the same or they need to be modi�ed. The proofs in all the 4 systems with equi-recursive
types are complex because of the strong recursion. Adding equi-recursive subtyping requires majorchanges in existing de�nitions, rules and proofs compared to  , making most of the existing
metatheory on  not reusable. No prior work has proved the conservativity of  with equirecursive types. This result is likely to be hard to prove because of the numerous non-modular
changes in  induced by the introduction of equi-recursive subtyping. Furthermore, in those works
the full type systems are not provided. Perhaps motivated by the technical challenges and negative
results posed by equi-recursive types, some researchers set their sights on iso-recursive types. In
their work on object encodings, Abadi et al. [1996] proposed the <:` calculus, which supports
bounded universal types, bounded existential types and iso-recursive types via the Amber rules.
However, re�exivity and transitivity are built-in, so the system is not algorithmic. Furthermore,while they presented the typing, subtyping and reduction rules, they have not proved any properties,
including type soundness or the conservativity over full  . One potential reason for the absence oftechnical results is that the iso-recursive Amber rules are hard to work with formally [Backes et al.
2014; Ligatti et al. 2017; Zhou et al. 2020, 2022]: it is di�cult to prove results such as transitivity, orde�ne sound and complete algorithmic formulations.
``This paper presents an extension of kernel  , called  , with iso-recursive types. In  we add
iso-recursive subtyping using the recently proposed nominal unfolding rules [Zhou et al. 2022].
The nominal unfolding rules have been formally proved to be type sound, and shown to have thesame expressive power as the well-known iso-recursive Amber rules [Cardelli 1985]. Moreover, thenominal unfolding rules address the di�culties of working formally with the (iso-recursive) Amber
rules. With the nominal unfolding rules, proving transitivity and other properties is easy, alsoenabling developing algorithmic formulations of subtyping instead. Furthermore, a nice property of
the nominal unfolding rules is that they are modular, allowing an existing calculus to be extended
with recursive types without major impact on existing de�nitions and proofs. In other words
they allow reusing most existing metatheory and de�nitions that existed before the addition of
iso-recursive types. Our work shows that the nominal unfolding rules proposed by Zhou et al. canbe integrated modularly into  , while retaining desirable properties. In particular, we prove, forthe �rst time, the conservativity of an extension of  with recursive types over the original  .
We also add two smaller extensions to  . The �rst one is a generalization of the kernel  rulefor bounded quanti�cation that accepts equivalent rather than equal bounds. The second extension
is the use of so-called structural folding/unfolding rules, inspired by the structural unfolding rule
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:4

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

proposed by Abadi et al. [1996]. The structural rules add expressive power to the more conventional
folding/unfolding rules in the literature, and they enable additional applications. In particular, we
illustrate how the structural rules play an important role to model encodings of objects, as well as
encodings of algebraic datatypes with subtyping.
We present several results, including: type soundness; transitivity and decidability of subtyp``
ing; the conservativity of  over  ; and a sound and complete algorithmic formulation of  .
``Moreover, we also present an extension of  , called  , which has a bottom type and lower
bounded quanti�cation in addition to the conventional (upper) bounded quanti�cation of  . As weshow, lower bounded quanti�cation is particularly interesting to model the subtyping of algebraic
datatypes. All the results in this paper have been formalized in the Coq theorem prover.
In summary the contributions of this paper are:•`
 : an extension of kernel  with iso-recursive types and subtyping. We prove several`
important properties for  , including: type soundness; transitivity and decidability of subtyping;

and the unfolding lemma.
`• The conservativity of  over  . Conservativity is an expected, but non-trivial property, thathas eluded past work on the combination of bounded quanti�cation and recursive types. We
show that an extension of kernel  with iso-recursive subtyping based on the nominal unfolding
rules is conservative over kernel  .
• Type soundness for the structural folding/unfolding rules. We present the �rst formal
type soundness proof for the structural unfolding rule, and we also present a new structural
folding rule, together with its type soundness.
• Decidability for a generalization of the kernel  rule for bounded quanti�cation, which
compares the bounds for equivalence. A key property is that equivalent types have equal sizes,
enabling the decidability proof.
`• An extension of  with both upper and lower bounded quanti�cation: We present an`
extended calculus, called  , with both top and bottom types, and both upper and lower bounded
quanti�cation, and illustrate its applicability to encodings of datatypes with subtyping.
• Coq formalization: We have formalized all the calculi and proofs in this paper in Coq, andmade the formalization available online: https://github.com/juda/Recursive-Subtyping-for-All
2

OVERVIEWThis section provides an overview of our work. We �rst brie�y review basic concepts and some
applications. Then we show our key ideas and results.
2.1

Bounded �antification and Recursive Subtyping

Bounded Quanti�cation. Bounded quanti�cation allows types to be abstracted by type variables with a subtyping constraint (or bound). The standard calculus with bounded quanti�cation,
 [Cardelli et al. 1994; Cardelli and Wegner 1985; Curien and Ghelli 1992], has two common
variants when it comes to subtyping universal types. The full  variant [Cardelli et al. 1994; Curien
and Ghelli 1992] compares bounded quanti�ers with the following rule:S��������` A2  A1, U  A2 ` B  C` 8(U  A1 ). B  8(U  A2 ). C

The most signi�cant characteristic of full  is that it allows two bounded quanti�ers to becontravariant on their bound types 1 and 2 when being compared. However, the rich expressivityof full  results in an undecidable subtyping relation [Pierce 1994], which is undesirable. In addition,
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:5

as Ghelli [1993] demonstrates, the rule S�������� may even prevent conservative extensions of in the presence of additional features.
There are several ways to restrict bounded quanti�cation to a fragment with decidable subtyping, such as removing top types, or assuming no bounds when comparing type abstraction
bodies [Castagna and Pierce 1994]. Among those the most widely used variant is the kernel calculus. In kernel  bounded quanti�ers can only be subtypes when their bound types are
identical [Cardelli and Wegner 1985], which is stated in the rule S����������.
S����������

`AS��������

, U A`BC` A1  A2` A2  A1, U  A2 ` B  C` 8(U  A). B  8(U  A). C` 8(U  A1 ). B  8(U  A2 ). C
In the rest of the paper, we will focus on kernel  , in order to achieve decidable subtyping
with iso-recursive subtyping. However, di�erently from kernel  , we will generalize the rule S���������� to a rule S�������� that accepts equivalent bounds instead. The main motivation forusing rule S�������� is to enable more subtyping involving records. While typically kernel is presented without records, in this paper we include records in the calculus and we wish toconsider types such as {G : nat, ~ : nat} and {~ : nat, G : nat}, to be equivalent (despite being
syntactically di�erent). Note that, while in plain  the subtyping relation is antisymmetric [Baldan
et al. 1999] (i.e. if two types are equivalent then they must be equal), the addition of records breaks
antisymmetry since there are equivalent types that are not equal. The rule S�������� is moregeneral than the kernel rule with identical bounds, but retains decidability, as we shall see in §4.2.
Recursive Types. Recursive types `U . , can be traced back to Morris [1969]. There are twobasic approaches to recursive types: equi-recursive types and iso-recursive types. The essential
di�erence between them is how they consider the relationship between a recursive type `U . andits unfoldings [U 7! `U . ] . In equi-recursive types, a recursive type is equal to its unfolding. Thatis `U . = [U 7! `U . ] . In other words, recursive types and their unfoldings are interchangeable
in all contexts. In iso-recursive types, a recursive type and its one-step unfolding are not equal but
only isomorphic. To convert between `U . and [U 7! `U . ] back and forth we need explicit
unfold and fold operators. A fold expression constructs a recursive type, while an unfold expression
opens a recursive type, as rule ����������� and rule ������������� illustrate:�������������

` e : `U . A�����������

` unfold [`U . A] e : [U 7! `U . A] A

` e : [U 7! `U . A] A

` `U . A` fold [`U . A] e : `U . A

Recursive Subtyping. Subtyping between recursive types has been studied for many years [Amadio
and Cardelli 1993; Cardelli 1985; Ligatti et al. 2017]. The most widely used subtyping rules forrecursive types are the Amber rules [Cardelli 1985], which consist of three rules: rule S������,rule S������ and rule S�����.
S������

, U V`AB

S������UV2S�����

` `U . A  `V. ⌫
`U V
`AA
The Amber rules are simple, but their metatheory is troublesome. For example, transitivity is hardto prove [Bengtson et al. 2011; Zhou et al. 2020, 2022]. Furthermore, due to the reliance on there�exivity rule (rule S�����), the Amber rules are problematic for subtyping relations that are notantisymmetric [Ligatti et al. 2017]. Recently, Zhou et al. [2020, 2022] proposed a new speci�cation
for iso-recursive subtyping and some equivalent algorithmic variants. For this paper we use one ofthose algorithmic variants, called the nominal unfolding rules [Zhou et al. 2022]. The main reason
to choose the nominal unfolding rules is that are easy to work with formally and Zhou et al. haveProc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:6

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveiraa full Coq development, including proofs of decidability, that we reuse and extend. The nominal
unfolding rules are:S��������

, U ` [U 7! AU ] A  [U 7! BU ] BS������`AB` `U . A  `U . B` AU  BU
The key intuition for the nominal unfolding rules is that, in order to correctly deal with subtyping
for contravariant occurrences of recursive type variables, we must unfold the recursive bodies
twice to check the validity of the subtyping statement. For instance, the subtyping statement`U . U ! nat  `U . U ! > should be rejected. If we unroll the recursive types twice, we get thefollowing invalid subtyping statement:((`U . U ! nat) ! nat) ! nat  ((`U . U ! >) ! >) ! >which requires both that nat  > (which is true) and >  nat, which is false and is the reason
why the subtyping statement should fail. Note that unrolling this example one time only results in(`U . U ! nat) ! nat  (`U . U ! >) ! >, which does not expose >  nat and is the reason why
unrolling 1-time only is not enough. The rule S�������� mimics this double-unrolling process, but
we obtain the following subtyping statement instead:(U ! nat) U ! nat  (U ! >) U ! >where the recursive types are replaced by U (note that U  U trivially holds). This statement issu�cient to trigger enough subtyping comparisons to validate the correctness of the subtyping
statement. In particular, it also requires checking that >  nat, which is false and will reject thesubtyping statement. By using recursive variables instead of the recursive types in the (double)
unfolding process we obtain a terminating procedure. The nominal unfolding rules use labelledtypes AU , to ensure that we only compare types that arise from unfolding substitutions withrelated unfolded types. Labelled types are a syntactic devise used to prevent accepting subtyping
statements such as `U . nat ! U  `U . nat ! nat ! >, which would be unsound in an isorecursive formulation. They also provide a distinct nominal identity to the recursive types being
compared, so that they cannot be compared with other unrelated recursive types. Note that, in therule S��������, we have reused the recursive variable name for the label U. However, we used thered color to distinguish the label and type variable names. Labels U should be the same in bothsubstitutions, and distinct from any other labels and bound variables used elsewhere. Since in thepaper presentation we use a nominal approach to represent binders, the label U should be interpreted
as some unique freshly generated name1 . Zhou et al. proved that the nominal unfolding rules aretype sound, and have the same expressive power as the iso-recursive Amber rules. Moreover, unlike
the Amber rules, they are easy to work with formally and they can be easily used in subtyping
relations that are not antisymmetric.
2.2

Applications of Bounded �antification and Recursive Types

We now turn to applications of bounded quanti�cation and recursive types. In particular the classic
application for both features is encodings of objects [Bruce et al. 1999]. In addition, we also showthat the two features are useful to model encodings of algebraic datatypes with subtyping.
Object Encodings. A simple and well-known typed encoding of objects is the recursive records
encoding [Bruce et al. 1999; Canning et al. 1989; Cook et al. 1989]. In this encoding the idea is that
object types are encoded as recursive record types, and objects are encoded as records. We will use
1 In our Coq formalization we use a locally nameless representation [Aydemir et al. 2008], which distinguishes free andbound variables naturally. With a locally nameless representation we can reuse the free variable name U for the label U.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:7

a simpli�ed form of the encoding, where we do not deal with self-references. But self-references
could be dealt with in standard ways. For example, we can de�ne a type Point:
Point , ` pnt.{x : Int, y : Int, move : Int ! Int ! pnt}

which consists of its coordinates and a move function. We use a recursive type because move should
return an updated point. To implement Point we de�ne some auxiliary functions:function getX(p : Point ) = (unfold [Point] p ). xfunction getY(p : Point ) = (unfold [Point] p ). yfunction moveTo(p : Point , x : Int , y : Int ) = (unfold [Point] p ). move x ythen a constructor mkPoint can be de�ned as:function mkPoint(x1 : Int , y1 : Int ) = fold [Point] { x=x1 , y=y1 , move = _x2 y2 . mkPoint(x2 , y2 ) }Note that the auxiliary functions above would not be needed in a source language, since a source
language would treat p.x as syntactic sugar for (unfold [Point] p).x. Similarly, the source language
would automatically insert a fold in the object constructor. In other words, in a source languagewith iso-recursive subtyping the fold’s and unfold’s do not need to be explicitly written and areautomatically inserted by the compiler. For instance, this is what Abadi et al. [1996]’s translation ofa language with objects into an iso-recursive extension of  does.
With subtyping, we can develop subtypes of Point, such as:
ColorPoint , ` pnt.{x : Int, y : Int, move : Int ! Int ! pnt, color : String}
EqPoint , ` pnt.{x : Int, y : Int, move : Int ! Int ! pnt, eq : pnt ! Bool}Now we wish to translate the coordinates by one unit for a point, but we do not want to write sucha translation function for all subclasses of Point. This is achieved with a polymorphic function:function translate [P  Point] (p : P) = (unfold [Point] p ). move (getX p + 1) (getY p + 1)

The type of this translate function is 8(P  Point). P ! Point, which is obtained from the following
typing derivation (some parts omitted):
P  Point, p : P ` p : P
P  Point, p : P ` P  Point����������
P  Point, p : P ` p : Point�������������
⇢x : Int, y : Int,P  Point, p : P ` (unfold [Point] p) :move : Int ! Int ! Point...
` translate : 8(P  Point). P ! Point
However, this type is unsatisfying because it loses type precision: it returns a Point instead of aP. The type that we want instead is:8(P  Point). P ! P

Unfortunately, we cannot obtain this more general type with only bounded quanti�cation, and theusual unfolding rule �������������. In the rule �������������, the unfold annotation must be arecursive type. However, if we wish to return P, then we should use unfold with the annotation P,
which is not a recursive type, but a type variable. Some advanced techniques, such as f-bounded`
quanti�cation [Canning et al. 1989], address this issue.  uses a less intrusive approach to obtain
the desired typing for translate via the structural unfolding rules, which we discuss in §2.3.
Encoding positive f-bounded quanti�cation. Fortunately, with the structural rules, we can use atype variable as an annotation for unfold. This enables us to encode forms of f-bounded quanti�cation with positive occurrences of recursive variables, which is the case for Point. We can change
the unfold annotation in translate from the recursive type Point to its subtype, the type variable P:
function translate [P  Point] (p : P) = (unfold [P] p ). move (getX p + 1) (getY p + 1)
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:8

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

In §2.3 we discuss the typing of this program via the structural unfolding rule in detail. After thischange the type of translate is 8(P  Point). P ! P. Then we can apply translate to Point or anyof its subtypes, without losing static precision. Thus, if we call translate [EqPoint] (mkEqPoint 00), then we obtain an EqPoint object at (1, 1). Note also that here mkEqPoint is a constructor forobjects with type EqPoint, which contain a binary method [Bruce et al. 1995] eq.
function mkEqPoint(x1 : Int , y1 : Int ) = fold [EqPoint]{ x = x1 , y = y1 , move = _x2 y2 . mkEqPoint(x2 , y2 ), eq = _p. (getX p == x1 ) ^ (getY p == y1 ) }Encodings of Algebraic Datatypes with Subtyping. It is well-known that in the polymorphic lambda
calculus (System F) [Girard 1972; Reynolds 1974], we can use Church [1932] encodings to encode
algebraic datatypes [Böhm and Berarducci 1985]. However, Church encodings make it hard toencode some operations, or worst they prevent encoding certain operations with the correct timecomplexity. A well-known example [Church 1932] is the encoding of the predecessor function on
natural numbers, which is linear with Church encodings instead of being constant time.
An alternative encoding of datatypes in the untyped lambda calculus, which avoids the issuesof Church encodings, is due to Scott [1962]. Unfortunately, Scott encodings cannot be encodedin plain System F. However, the addition of recursive types to a polymorphic lambda calculus
allows a typed encoding for Scott encodings [Parigot 1992]. Moreover, in the presence of subtyping,
we can also encode algebraic datatypes with subtyping, enabling certain forms of reuse that are
not possible without subtyping. Oliveira [2009] has shown this assuming a  -like language withrecursive types and records, but he has not formalized such a language. Here we revisit Oliveira’s`
example. A similar encoding for datatypes can be achieved in  . For example, one may de�ne adatatype Exp1 for mathematical expressions, with numeric, addition, and subtraction constructors:
data Exp1 = Num Int | Add Exp1 Exp1 | Sub Exp1 Exp1

The encoding in` of this datatype can be de�ned as follows:

Exp1 , `E. 8A. {num : Int ! A, add : E ! E ! A, sub : E ! E ! A} ! A

If we unfold the recursive type, this encoding is a polymorphic higher order function that takes arecord with three �elds (num, add and sub) as input. Each �eld corresponds to a constructor in thedatatype de�nition. This encoding is particularly useful for case analysis, since the polymorphic
function essentially encodes case analysis directly. To write a function that performs case analysis
on this datatype, one can unfold the recursive type, instantiate A with the result type, and thenprovide a record that maps each case to its implementation function that takes the constructor
components as input and returns a result of type A. For example, given an expression e with typeExp1 , a case analysis-based evaluation function can be written as:function eval (e : Exp1 ) = (unfold [Exp1 ] e) [ Int ]{ num = _n. n, add = _e1 e2 . (eval e1 + eval e2 ), sub = _e1 e2 . (eval e1 − eval e2 ) }where we use [. . .] to represent type instantiation. Here Exp1 is instantiated with the evaluation
result type Int. A record of three functions is supplied to implement case analysis. The num �eld
implements a function that returns the integer n of the Num constructor directly, while the functionsin add and sub �elds perform the evaluation process recursively. To construct concrete instancesof the datatype, each constructor also comes with a corresponding encoding in the calculus:
function Num1 (n: Int) = fold [Exp1 ] (⇤ A. _ e. (e.num n))function Add1 (e1 : Exp1 , e2 : Exp1 ) = fold [Exp1 ] (⇤ A. _ e. (e.add e1 e2 ))function Sub1 (e1 : Exp1 , e2 : Exp1 ) = fold [Exp1 ] (⇤ A. _ e. (e.sub e1 e2 ))One can easily check, using rule �����������, that the result type of each constructor encoding
becomes Exp1 after a recursive type folding. Therefore, in this encoding, the use of constructors and case analysis functions is natural: one can construct the expression 1 + 2 directly with
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:9

the encoded constructors as Add1 (Num1 1) (Num1 2), and get its evaluation result by calling
eval (Add1 (Num1 1) (Num1 2)).
Subtyping between datatypes. Now consider a larger datatype Exp2 , which extends the Exp1
datatype with a new constructor Neg, for denoting negative numbers.
data Exp2 = Num Int | Add Exp2 Exp2 | Sub Exp2 Exp2 | Neg Exp2

This datatype is encoded in

`
 as:

Exp2 , `E. 8A. {num : Int ! A, add : E ! E ! A, sub : E ! E ! A, neg : E ! A} ! A

The datatype Exp2 di�ers from Exp1 only in the new constructor. However, other constructors are
just the same. To reduce code duplication, polymorphism on datatype constructors is desirable.
Note that Exp2 has more constructors than Exp1 , so it should be safe to coerce Exp1 expressions
into Exp2 expressions, i.e. Exp1  Exp2 . Therefore, we would like the constructor for Add to havethe following type, so that both Exp1 and Exp2 can use this constructor:
Add8 : 8(EExp1 ). E ! E ! E

There are two problems here. Firstly, similarly to the issue that we have faced in the translatefunction, we would like to use a type variable in the fold’s of the constructors. This way we canmake the constructors polymorphic. Secondly, as evidenced by the desired type for Add, we need`lower bounded quanti�cation, but in  (and  ) we only have upper bounded quanti�cation.

Polymorphic constructors with lower bounded quanti�cation. For applications such as encodingsof algebraic datatypes, the dual form of bounded quanti�cation (lower bounded quanti�cation)`
seems to be more useful. Thus we have an extended system, called  , that also supports lower
bounded quanti�cation. Polymorphic datatype constructors become typeable with the structural
folding rule. For example, we can encode the polymorphic Add constructor as:function Add 8 [EExp1 ] (e1 : E, e2 : E) = fold [E] (⇤ A. _ e. (e . add e1 e2 ))Other polymorphic constructors such as Num8 and Sub8 can be encoded similarly, enabling more
useful programming patterns. For example, if we want to implement a compiler that uses Exp1 as
its core language, but also want to support richer datatype constructors in a source language like
Exp2 does, we would like to be able to reduce code duplication across the two similar languages.
For instance, if we de�ne a pretty printer function for Exp2function print (4: Exp2 ) = (unfold [Exp2 ] 4) [string] {num = _ n. ( int_to_string n ), add = _ e1 e2 . ((print e1 ) ++ "+" ++ ( print e2 )),sub = _ e1 e2 . ((print e1 ) ++ "−" ++ ( print e2 )), neg = _ e. ( "−" ++ ( print e ))}we can use this function to print Exp1 expressions as well: all the constructors in Exp1 are also
in Exp2 and have their pretty printing methods de�ned in the above function. With subtyping
between algebraic datatypes, it holds that Exp1  Exp2 , so it is safe in our encodings to apply thisprint function to values of type Exp1 , without another pretty printing function for Exp1 .
Suppose also that we wish to implement a simple desugaring function that transforms Exp2 into
Exp1 , by transforming negative numbers = into subtractions 0 =. This function should do caseanalysis on Exp2 and use only the constructors in Exp1 to produce the result, i.e. it should have atype Exp2 ! Exp1 . The following code, with polymorphic constructors, has the desired typing:function desugar (4: Exp2 ) = (unfold [Exp2 ] 4) [Exp1 ] {num = _ n. Num 8 [Exp1 ] n,
add = _ e1 e2 . Add 8 [Exp1 ] (desugar e1 ) (desugar e2 ),sub = _ e1 e2 . Sub 8 [Exp1 ] (desugar e1 ) (desugar e2 ),neg = _ e. Sub 8 [Exp1 ] (Num 8 [Exp1 ] 0) (desugar e)}

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:10

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

In contrast, in many practical programming languages this task either involves code duplication
or loss of type precision. In a typical functional language, we can de�ne both Exp1 and Exp2 andalso obtain precise static typing guarantees for the desugar function. But this comes at the cost of
duplication, since the constructors for the two datatypes are di�erent, and many operations, such as`
pretty printing need to be essentially duplicated. In  , in addition to polymorphic constructors,
we would just need to de�ne the pretty printer for Exp2 , and that function would also work for Exp1 .
Alternatively, one could de�ne only Exp2 and type desugar with the imprecise type Exp2 ! Exp2 ,which does not statically guarantee that the Neg constructor has been removed. This solution avoids`
the duplication at the cost of static typing guarantees. In  we do not need such compromise:
we can avoid code duplication and preserve the static typing guarantees.
2.3

Key Ideas and Results

As Table 1 shows, no previous calculi with bounded quanti�cation and recursive types are fully
satisfactory in all dimensions. Equi-recursive types are quite problematic, since they can change
the expressive power of the subtyping relation in unexpected ways. More importantly, adding equirecursive subtyping to  requires novel algorithms, and the extension is non-modular, requiring
several changes to existing de�nitions and proofs.
Kernel  with iso-recursive types. Our type system directly combines kernel  and the nominal
unfolding rules together. The addition of the nominal unfolding rules has almost no e�ect in theoriginal proofs in kernel  . That is the proofs for important lemmas, such as transitivity, are nearly
the same as those in kernel  , except that we need a new case to deal with recursive types. Thus`
proofs that have been very hard in the past, such as transitivity, are very simple in  .
`The more challenging aspect in the metatheory of  lies in the unfolding lemma:` `U .

 `U . ⌫)` [U 7! `U . ] [U 7! `U . ⌫] ⌫which reveals an important property for iso-recursive types: if two iso-recursive types are subtypes,
then their one-step unfoldings are also subtypes. To prove the unfolding lemma, a generalized`
lemma is needed [Zhou et al. 2022]. In  , we show that the previous generalized approach isinsu�cient, due to bounded quanti�cation. Therefore, a more general lemma is proposed.
Another challenge is decidability. Although both kernel  and the nominal unfolding rules(for simple calculi) have been independently proved decidable, their decidability proofs use very
di�erent measures. A natural combination is problematic, thus we need a new approach.
`
After overcoming those challenges, as Table 1 shows,  performs well in various dimensions:
it is transitive, decidable, conservative and modular. Furthermore, there is a simple, sound andcomplete algorithmic type system to enable implementations, and to provide important help in the
proofs of results such as conservativity of typing.
Structural folding and unfolding rules. In our work, instead of standard rules for fold/unfold
expressions, we use structural rules:��������������`e:A` A  `U . B������������

` e : [U 7! B] A

` `U . A  B` unfold [A] e : [U 7! A] B
` fold [B] e : B
The key point about the structural rules is that the annotations are generalized to be a subtype/supertype of a recursive type, instead of exactly a recursive type. In particular, this generalization enables
annotating fold/unfold with a bounded type variable, which is a subtype/supertype of a recursive
type. This is forbidden in the traditional rules. In the rule ��������������, it is worthwhile tomention that when we have  `U . ⌫ where U appears negatively in ⌫, then there are very limited
choices to what can be. Essentially it can be `U . ⌫ itself and little else. In other words, negative
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:11

recursive types have very restricted subtyping, which is why the structural unfolding rule canbe type safe. Note also that, since the structural unfolding rules provide almost no �exibility for
negative recursive subtyping, they are insu�cient to fully express f-bounded quanti�cation for
negative recursive types.
The structural unfolding rule was presented by Abadi et al. [1996] for supporting structural
update in the object calculus that was being encoded into  with iso-recursive types. In their work,
the structural unfolding rule is presented with an informal explanation. We provide structural rules
for both expressions, together with the formalization of the type soundness for both rules. With thestructural unfolding rule we can, for instance, obtain the desired typing for the translate function.
��������������
...

P  Point, p : P ` p : P

P  Point, p : P ` P  Point⇢
x : Int, y : Int,P  Point, p : P ` (unfold [P] p) :move : Int ! Int ! P` translate : 8(P  Point). P ! P
Readers can compare this derivation to the one in §2.2, where the conventional unfolding ruleand the subsumption rule are used instead. The use of rule �������������� enables us to give amore precise type for the translate function.
Lower bounded quanti�cation and  . We have also formalized an extension of  with both``
upper and lower bounded quanti�cation, called  . All the same results that are proved for  are`also proved for  , including transitivity, decidability and type soundness. The structural folding`
rules become more useful in  . With lower bounded quanti�cation and the structural folding
rules we can get the correct typing for the polymorphic Add constructor:
`

`

···

E
������������

8
9>>< num : Int ! A,>=>
Exp1, e1 : E, e2 : E ` ⇤A. _e.(e.add e1 e2 ) : 8A. add : E ! E ! A, ! A>> sub : E ! E ! A >
>
:
;
...

3

E

Exp1, e1 : E, e2 : E ` fold [E] (⇤A. _e. (e.add e1 e2 )) : E` Add8 : 8(E Exp1 ). E ! E ! E

BOUNDED QUANTIFICATION WITH ISO-RECURSIVE TYPESThis section introduces a full calculus, called  , with bounded quanti�cation, records and recursive`
types.  is an extension of kernel  [Cardelli and Wegner 1985] with iso-recursive types.
`

3.1

Syntax and Well-Formedness

Syntax and Well-Formedness. The syntax of types and contexts for  is shown below.
Types, ⌫, . . . F nat | > | 1 ! 2 | U | `U . | U | 8(U  ). ⌫ | {;8 : 8 8 21···= }Expressions 4
F G | i | 4 1 4 2 | _G : . 4 | 4 | ⇤(U  ). 4
| unfold [ ] 4 | fold [ ] 4 | {;8 = 48 8 21···= } | 4.;
ValuesE
F i | _G : . 4 | fold [ ] E | ⇤(U  ). 4 | {;8 = E8 8 21···= }Contexts
F · | ,U  | ,G :Meta-variables , ⌫, ⇠, ⇡ range over types. Types consist of: natural numbers (nat), the top type (>),
function types ( ! ⌫), type variables (U), recursive types (`U . ), labelled types ( U ), universal
types (8(U  ). ⌫), and record types ({;8 : 8 8 21···= }). Labelled types are types that are annotatedwith a label. They enable distinguishing between otherwise structurally compatible types (equal
types or subtypes). That is if the two types being compared have di�erent labels or one of the types
is unlabelled, then the two types will not be related, even when (ignoring the labels) they would be`

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:12

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira`�������

����T��

` nat`>�������

�������

U A2

`A

`U

�������

�������` A8` A1 ! A2

for each 8` {;8 : A8 8 21···= }

U

`A

S����

`

`

` nat  nat

`A

`A>

S����

`

S������

` B1  A1`U, U  > ` [U 7! AU ] A  [U 7! BU ] BS���������

U B2` `U . A  `U . B` A2  A1

S������

, U  A2 ` B  C`AB` AU  BU` 8(U  A1 ). B  8(U  A2 ). C

` {: 9 : A 9 9 21···< }{;8 8 21···= } ✓ {: 9 9 21···< }` {: 9 : A 9

9 21···<}  {;8 : B8

8 21···=

`BA

`U A

S��������

` A1  A2` A2  B2` A1 ! A2  B1 ! B2

`U U

S����

`

` A2

(Subtyping)

⌫

S����

` A1

` 8(U  A). B`A` `U . AS����, U A`B

���������

, U >`A`(Well-formed Type)���������

: 9 = ;8 implies}` A 9  B8

Fig. 1. Well-formedness and subtyping rules.

structurally compatible types. They are used for dealing with subtyping of iso-recursive types aspart of the nominal unfolding approach. Expressions, denoted by meta-variable 4, include: term
variables (G), natural numbers (i), applications (4 1 4 2 ), abstractions (_G : . 4), type applications (4 ),type abstractions (⇤(U  ). 4), fold expressions (fold [ ] 4), unfold expressions (unfold [ ] 4),
records ({;8 = 48 8 21···= }) and record selection (4.;). Among them, natural numbers, abstractions andtype abstractions are values. Fold expressions and records can be values if their inner expressions
are also values. The context is used to store type variables with their bounds, and term variables with
their types. Note that it is unnecessary to distinguish recursive variables and universal variables.
The de�nition of a well-formed environment ` is standard, ensuring that all variables in theenvironment are distinct and all types in the environment are well-formed. A type is well-formed if
all of its free variables are in the context. The well-formedness rules for types are shown in Figure 1.
3.2

Subtyping

The bottom of Figure 1 shows the subtyping judgement. Our subtyping rules are mostly standard.
The rules essentially include the rules of the algorithmic version of kernel  [Cardelli et al. 1994;
Cardelli and Wegner 1985], but the rule for bounded quanti�cation is generalized. The rules S���� and S��������� are standard  rules. Note that since we do not distinguish universal andrecursive variables, those rules apply also to recursive type variables. The rule for function types(rule S������) is contravariant on the input types and covariant on the output types.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:13

Subtyping bounded quanti�cation. The rule for bounded quanti�cation is interesting, stating that
two universal types are subtypes if their bounds are equivalent (i.e. they are subtypes of each other)and the bodies are subtypes. Note that rule S�������� is more general than rule S����������
since the latter one requires the bounds are equal. The reason to have the more general rule using
equivalent bounds is that, for records, we wish to accept subtyping statements such as:8(U  {G : nat, ~ : nat}). U ! U  8(U  {~ : nat, G : nat}). U ! U

where the bounds can be syntactically di�erent, but equivalent types. In the presence of records
or other features (such as intersection and union types [Barbanera et al. 1995; Coppo et al. 1981;
Pottinger 1980]) we can have such equivalent, but not syntactically equal types. Therefore, weshould generalize the rule for bounded quanti�cation do deal with those cases. This generalization
to equivalent bounds retains decidable subtyping just as kernel  as we shall see in §4.2.

Subtyping recursive types. For dealing with iso-recursive subtyping we employ the recent nominal
unfolding rules [Zhou et al. 2022], which have equivalent expressive power to the well-known(iso-recursive) Amber rules [Cardelli 1985]. The nominal unfolding rules have been discussed in§2.1. The reason to choose the nominal unfolding rules is that they enable us to prove important
metatheoretical results, such as transitivity and develop an algorithmic formulation of subtyping.
`
We extend the rule S�������� to the rule S���� in  , by bounding recursive variables with
> when they are introduced into the context. Therefore, recursive variables are also treated as`universal variables, and we do not need to adjust the form of contexts in  for  . Apart from
this, no other changes are necessary, making the addition of recursive types mostly non-invasive.
Consequently, the proofs of narrowing, re�exivity and transitivity are the same as the original one
for  , except for the new cases dealing with recursive types and minor adjustments to the rule ofbounded quanti�cation due to the generalization to equivalent bounds.
Lemma 3.1 (Narrowing). If 1 ` ⇠  ⇠ 0 and 1, U  ⇠ 0, 2 `Theorem 3.2 (Re�exivity). If `Theorem 3.3 (Transitivity). If

and

`

`

then

`

 .

 ⌫ and` ⌫  ⇠ then

` `U .

 `U . ⌫ then ⌫ then 1, U  ⇠, 2 `
`

 ⌫.

 ⇠.

The unfolding lemma. Another important lemma is the unfolding lemma, which reveals that: if
two recursive types are subtypes, then their unfoldings are also subtypes. The unfolding lemma is
important for proving preservation in a system with iso-recursive subtyping. A key di�culty in`the formalization of  is proving the unfolding lemma which, due to the presence of bounded
quanti�cation, requires a di�erent proof technique compared to the proofs by Zhou et al. [2022].
We discuss the proof of the unfolding lemma in §4.1.
Lemma 3.4 (Unfolding Lemma). If
3.3` [U 7! `U . ] [U 7! `U . ⌫] ⌫.

Type Soundness

Figure 2 shows the typing rules and reduction rules. Most rules are standard except for the typing
rule for unfold and fold. For these two expressions we use structural rules instead (rule �������
������� and rule ������������), as we explained in §2.3.
Structural unfolding lemma. Since the typing rules that we adopt for fold/unfold expressions are
the structural rules, which generalize the conventional rules, we need a more general form for theunfolding lemma. The generalization of the lemma is necessary for the type preservation proof
with the structural folding/unfolding rules. We call the new lemma the structural unfolding lemma:
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:14

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira`4 :����������

����������

`

G:

`

` i : nat

`x:A����������

`e:A

2

������������

` e : [U 7! B] A

`e:B

` e1 : A1 ! A2

`e:A

` e1 e2 : A2

�����������

` e : 8(U  B1 ). B2` A  `U . B` unfold [A] e : [U 7! A] B

�����������

` e2 : A1` _x : A1 . e : A1 ! A2��������������

` fold [B] e : B����������

, G : A1 ` e : A2

`AB

` `U . A  B(Typing)����������

�����������

` e : {;8 : A8 8 21···= }, U A`e:B` e.;8 : A8

` ⇤(U  A). e : 8(U  A). B

����������

for each 8` A  B1

` e A : [U 7! A] B2` e8 : A8` {;8 = e8 8 21···= } : {;8 : A8 8 21···= }(Reduction)

4 1 õ! 4 2
���������

��������

e1 A õ! e2 A��������

e1 e2 õ! e10 e2

v1 e2 õ! v1 e20

e2 õ! e20�����������

���������

unfold [A] e õ! unfold [A] e0

fold [A] e õ! fold [A] e0

e õ! e0

unfold [A] (fold [B] v) õ! v
e1 õ! e2���������

e1 õ! e10(_x : A. e1 ) v2 õ! [G 7! v2 ] e1���������

���������

e õ! e0���������

���������

e õ! e0(⇤(U  A). e) B õ! [U 7! B] ee.; 9 õ! e0 .; 9������������

{;8 = v8 8 21···= }.; 9 õ! v 9e 9 õ! e09{;8 = E8 8 21···9 1, ; 9 = e 9 , ;: = 4: : 2 9+1···= } õ! {;8 = E8 8 21···9 1, ; 9 = e09 , ;: = 4: : 2 9+1···= }Fig. 2. Typing and Reduction Rules

Lemma 3.5 (Structural unfolding lemma). If`U . ⇠]  [U 7! `U . ⇡] ⌫.

` `U .

 `U . ⇠  `U . ⇡  `U . ⌫ then

` [U 7!

In this lemma, in the one-step unfolding the recursive types substituted in the bodies are, respectively, a supertype and a subtype of `U . and `U . ⌫. In contrast, in the unfolding lemma proposedby Zhou et al., the recursive types that get substituted in the bodies are the same. As §4.1 will
discuss, both forms of the unfolding lemma can be proved using a more general lemma.
Type Soundness. To see how the structural unfolding lemma is used in the proof of type preservation, let us consider an expression unfold[⇡ 0] (fold[⇠ 0] 4). Starting from a closed expression, both
⇠ 0 and ⇡ 0 must be recursive types, thus we assume that ⇠ 0 is `U . ⇠ and ⇡ 0 is `U . ⇡,Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

`

*⌫

48:15

(Upper Exposure)
XA��������

U A2

`

XA���

A is not type variable`A * B`U * B`A * A(Lower Exposure)+⌫

XA�����

XA����

A is not type variable or >`A + A` > + `U . >`0 4 :(Algorithmic Typing)��������

`a e1 : A

` A * A1 ! A2

`a e1 e2 : A2

���������

`a e : B`a e2 : B

` B * 8(U  B1 ). B2` A  B1`a e A : [U 7! A] B2

������������

`a e : A` B * `U . C` B  A1`AB

`a unfold [B] e : [U 7! B] C����������

`a e : A` C + `U . B` A  [U 7! C] B`a fold [C] e : C`C

Fig. 3. Algorithmic Typing.

` 4 : [U 7! ⇠ 0]
` `U .  ⇠ 0������������
` fold[⇠ 0] 4 : ⇠ 0` ⇠0  ⇡0����������
` fold[⇠ 0] 4 : ⇡ 0` ⇡ 0  `U . ⌫��������������
` unfold[⇡ 0] (fold[⇠ 0] 4) : [U 7! ⇡ 0] ⌫The type of unfold[⇡ 0] (fold[⇠ 0] 4) becomes [U 7! `U . ⇡] ⌫, and it should be a subtype of[U 7! `U . ⇠] , which is the type of reduction result 4.
The other parts of the type soundness proof are standard, thus we have:
Theorem 3.6 (Preservation). If ` 4 :Theorem 3.7 (Progress). If ` 4 :3.4

and 4 õ! 4 0 then ` 4 0 : .

then 4 is a value or exists 4 0, 4 õ! 4 0.

Algorithmic typing

The rules that we have presented in Figure 2 are declarative. The conclusion of the subsumption
rule overlaps with all other rules, making it non-trivial to derive an implementation from the rules.
Figure 3 shows the algorithmic rules for typing. We only present new rules and rules that di�er
from Figure 2. Compared with the declarative typing rules, the subsumption rule (����������)is removed. Besides, application (����������), type application (�����������), structural folding(������������) and structural unfolding (��������������) rules are replaced by rules ��������,Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:16

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira���������, ���������� and ������������, respectively. In the algorithmic typing rules we takethe standard approach of distributing subtyping checks in appropriate places in the other rules,
thus eliminating the need for the subsumption rule.
`
One interesting point is the two exposure relations * and + in  . In  , there is only the upper
exposure function ( ` * ⌫), which is used to �nd the least non-variable upper bound for avariable in the context [Pierce 2002]. Thus the upper exposure function plays an important rolefor �nding the minimal type with the algorithmic typing rules. To make our rules more general,
we additionally de�ne the lower exposure function ( ` + ⌫) to �nd the greatest non-variable`
subtype ⌫ for . For  , lower exposure only helps to �nd the correct shape for the recursive typebody to be folded in rule ���������� by mapping > to `U . >. The lower exposure function will be
more useful when we have lower bounded variables in the system, as we will see in §5.
The algorithmic rules are equivalent (sound and complete) with respect to the declarative rules:
Theorem 3.8 (Soundness of the algorithmic rules). If`0 4 :

Theorem 3.9 (Completeness of the algorithmic rules). If`0 4 : ⌫ and ` ⌫  .

then

`4 :

`4 : .

then there exists a ⌫ such that

Theorem 3.9 implies that our algorithm can always �nd a minimal type, which is an important`
property for  .
4

METATHEORY OF`In this section we discuss the most interesting and di�cult aspects of the metatheory of  inmore detail. We cover three key properties: the unfolding lemma, decidability of subtyping and the`conservativity of  over the original  . The interaction between iso-recursive types and bounded
quanti�cation requires signi�cant changes in the proofs of the unfolding lemma and decidability.
`
In addition, conservativity cannot be proved using a declarative formulation of  , and we need to
employ the algorithmic formulation instead.
4.1`

Unfolding Lemma

The unfolding lemma (Lemma 3.4) is a core lemma for the metatheory of a calculus with isorecursive subtyping. Though the statement of the unfolding lemma is quite simple and intuitive tounderstand, the lemma cannot be proved directly. We will �rstly review the previous approach toprove the unfolding lemma, which does not account for bounded quanti�cation, and then show
how to transfer this approach to a system with bounded quanti�cation.
The previous approach for proving the unfolding lemma. Because the premise of the unfolding
lemma is a subtyping relation between two recursive types `U .  `U . ⌫, a direct induction onsuch subtyping relation is problematic. Thus, we need to prove a generalized lemma �rst. In Zhou
et al.’s work that lemma has the following form:
Lemma 4.1 (The generalized unfolding lemma in Zhou et al. [2022]). If 1, U, 2, `
 ⌫ and
`
`U
.
⇠

`U
.
⇡
then
1
(1) 1, U, 2 ` [U 7! ⇠ U ]  [U 7! ⇡ U ] ⌫ implies 1, 2 ` [U 7! `U . ⇠]  [U 7! `U . ⇡] ⌫;(2) 1, U, 2 ` [U 7! ⇡ U ]  [U 7! ⇠ U ] ⌫ implies 1, 2 ` [U 7! `U . ⇡]  [U 7! `U . ⇠] ⌫.

Due to the tricky interaction between rule S���� and rule S������, in the generalized unfolding
lemma we need two mutual dependent lemmas: one is used for covariant cases (1) and the other one
is used for contravariant cases (2). The proof for this lemma proceeds by induction on 1, U, 2, ` ⌫. In the inductive proof we need to switch between covariance and contravariance. In particular, in
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:17

the rule S������ case for functions, we need an induction hypothesis that arises from conclusion(2) to prove the contravariant premise ` ⌫ 1  1 relating the input types of the function.
`
For the generalized unfolding lemma in  , Lemma 4.1 is unfortunately not general enough.
In a setting with bounded quanti�cation, 2 may contain bounds with the type variable U, andthose variables are not being substituted in Lemma 4.1. Let us consider the e�ect of adding rule S���������. In the conclusion of Lemma 4.1, the variable U is substituted by another type and tracked
in the context 2 . In the premises of rule S���������, we need to �nd the upper bound of variable U
in the contexts 1 and 2 . With those two observations, in our new attempt, the context also needs
to do substitutions. Thus, a natural attempt to solve this problem is to reformulate the lemma into
the following form (for the covariant case (1)):
Proposition 4.2 (A �rst attempt at the generalized unfolding lemma). If 1, U  >, 2 `  ⌫and 1 ` `U . ⇠  `U . ⇡ then 1, U  >, 2 [U 7!?U ] ` [U 7! ⇠ U ] [U 7! ⇡ U ] ⌫ implies
 [U 7! `U . ⇡] ⌫.
1, 2 [U 7! `U . ?] ` [U 7! `U . ⇠]Here, the syntax [U 7! (] denotes that all the occurrences of U in context will be replaced
by a speci�ed type (. However, we do not know yet what type should be �lled in the hole ? in
Proposition 4.2, so we leave the hole there for now. Although we omit conclusion (2) in Proposition
4.2, similar reasoning applies to that conclusion.
Let us now consider the e�ect of adding the rule S��������: Assume that := 8(V  * 1 ). )1
and ⌫ := 8(V  * 2 ). )2 . The goal would look like:
1, 2 [U 7! `U . ?] ` [U 7! `U . ⇠] 8(V  * 1 ). )1  [U 7! `U . ⇡] 8(V  * 2 ). )2

After simpli�cation and applying rule S��������, one of the goals becomes:

1, 2 [U 7! `U . ?], V  [U 7! `U . ⇡] * 2 ` [U 7! `U . ⇠] )1  [U 7! `U . ⇡] )2

From the above, we would expect that the hole ? is �lled with ⇡ because all the substitutions in thecontext must be the same in order to apply induction hypothesis. Thus, a second attempt at thegeneralized unfolding lemma looks like:
Proposition 4.3 (The second attempt at the generalized unfolding lemma (1)). If 1, U  >, 2 `  ⌫and 1 ` `U . ⇠  `U . ⇡ then 1, U  >, 2 [U 7! ⇡ U ] ` [U 7! ⇠ U ]  [U 7! ⇡ U ] ⌫ implies
 [U 7! `U . ⇡] ⌫.
1, 2 [U 7! `U . ⇡] ` [U 7! `U . ⇠]Proposition 4.3 deals with rule S��������� and S�������� successfully. However, the function
case, which is correctly proven in Lemma 4.1, will break. Consider := 1 ! 2 and ⌫ := ⌫ 1 ! ⌫ 2 ,and apply rule S������. We need to prove two subgoals:(1) 1, 2 [U 7! `U . ⇡] ` [U 7! `U . ⇠] 2  [U 7! `U . ⇡] ⌫ 2 ;(2) 1, 2 [U 7! `U . ⇡] ` [U 7! `U . ⇡] ⌫ 1  [U 7! `U . ⇠] 1 .
Note that we do not have any induction hypothesis for proving subgoal (2) because occurrences of
U in 2 have been substituted by `U . ⇡, but we expect the U’s to have been replaced by `U . ⇠ forapplying the induction hypothesis. Even if we add the second conclusion back to the Proposition
4.3, we still have problems. For conclusion (2), the type used for the substitution in the context
should be same as the type used for the substitution in the right-hand side of the subtyping. If we�ll the hole ? with ⇠ in Proposition 4.2, the subgoal (1) in case S������ will get stuck for a similarreason. Therefore, the type in the hole ? cannot be the type ⇠ or ⇡.
In summary, in the previous approach by Zhou et al., without bounded quanti�cation, only theinteraction of covariance/contravariance between types has to be considered. In contrast, withbounded quanti�cation, the interaction of covariance/contravariance among contexts and types
also needs to be considered. Our generalization should be able to deal with all the complications
arising from rule S����, rule S���������, rule S������ and rule S��������.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:18

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

The generalized unfolding lemma for  . Surprisingly, the generalization is relatively straightforward. For solving the issue that we mention above, instead of picking type ⇠ or type ⇡, we pick anintermediate type ( between ⇠ and ⇡. We need the following auxiliary lemma:`

Lemma 4.4. If , U  > ` [U 7!

U]

The generalized unfolding lemma for [U 7! ⌫U ] ⌫ then , U  > `

`
 is:

 ⌫.

Lemma 4.5 (The generalized unfolding lemma for  ). If (1) 1, U  >, 2 `  ⌫, (2) 1 ` `U . ⇠ `U . ( and (3) 1 ` `U . (  `U . ⇡ then(1) 1, U  >, 2 [U 7! ( U ] ` [U 7! ⇠ U ]  [U 7! ⇡ U ] ⌫ implies 1, 2 [U 7! `U . (] ` [U 7!
`U . ⇠]  [U 7! `U . ⇡] ⌫;(2) 1, U  >, 2 [U 7! ( U ] ` [U 7! ⇡ U ]  [U 7! ⇠ U ] ⌫ implies 1, 2 [U 7! `U . (] ` [U 7!
`U . ⇡]  [U 7! `U . ⇠] ⌫.
`By applying Lemma 4.5 with 1 = , 2 = ·, ( = , ⇠ = and ⇡ = ⌫, we prove the unfolding
lemma (Lemma 3.4). The premises can be obtained by inversion on ` `U .  `U . ⌫, and thenapplying Lemma 4.4. Next we give an overview of the key points in the proof of Lemma 4.5 for thefour tricky cases. Assume that we do induction on premise (1).
• Rule S����: This case mostly follows the previous approach. The interesting point is that wecannot obtain `U . ⇠  `U . ⇡ directly from the conditions raised by the goals, but have one extra
step via transitivity (Theorem 3.3).
• Rule S���������: For this case we need to consider two subcases. If = U then from the context
U  > we can easily know that ⌫ is > too. Otherwise, we apply the induction hypothesis directly.
• Rule S������: This case is surprisingly easy: we can follow the previous approach for dealing
with the contravariant case for subtyping input types of functions, and apply the induction
hypothesis derived from conclusion (2) directly. Note that the key point of avoiding the issue we
discussed before is that, by picking an intermediate type (, we decouple the substitution in thecontext and in the subtyping relation for the function case. That is, the substitution with type
`U . ( is invariant in both subgoals, independent of the substitution in the subtyping relation.
• Rule S��������: This case is the most interesting one. Assume = 8(V  * 1 ). )1 and ⌫ = 8(V * 2 ). )2 . Let us consider how to prove the goal (1). Doing inversion on condition arising from thegoal, we obtain that [U 7! ⇠ U ] * 1 and [U 7! ⇡ U ] * 2 are equivalent. Meanwhile, we know * 1
and * 2 that are equivalent. There are two possibilities: either ⇠ and ⇡ are equivalent or U is notin type * 1 nor * 2 . For the latter case, we can rewrite the substituted types in the contexts foraligning the contexts, then solve the issue we discussed above. The former case is quite subtle:
since ( lies in the middle of ⇠ and ⇡, the three types are all equivalent. In other words, we canchange the substituted types arbitrarily and get the equivalent types and contexts. The criticalpoint is that, although the substitution in the context is indeed a�ected by the substitution in the
supertype, since the bounds are equivalent, the type ( will converge into the types ⇠ and ⇡.
As a �nal note, we cannot apply this technique to full  . In full  , in the context, the type ⇠and ⇡ will swap due to the contravariance. How to prove the unfolding lemma for full  is notclear now, and we leave this as the future work.
4.2

Decidability

Decidability is one of the important properties of  . We �rst start by reviewing the approaches
to prove decidability in kernel  , and nominal unfoldings, and then describe our approach toprove decidability. These two previous approaches to prove decidability employ di�erent measures,`
which creates a challenge for proving the decidability of  .
`Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:19

Decidability of kernel  . It is well-known that bounded quanti�cation for full  is undecidable[Pierce 1994]. However, for kernel  , identical bounds make the system decidable. A common
practice is to de�ne a weight function to compute the size of a type [Pierce 2002]:
F486⌘C (>)
F486⌘C 1,U  , 2 (U)F486⌘C (8(U  ). ⌫)F486⌘C ( ! ⌫)

=
=
=
=

1
1 + F486⌘C 1 ( )1 + F486⌘C ,U  (⌫)
1 + F486⌘C ( ) + F486⌘C (⌫)

For universal types, we store its bound into a context , and when we meet the universal variable, we
retrieve its bound from the context and compute the size recursively. Since the size of a conclusion
is always greater than any premise, this measure can be used to show that the subtyping algorithm
in kernel  terminates for all inputs.
Decidability of nominal unfoldings. The nominal unfolding rule in simple calculi with subtyping
is also decidable [Zhou et al. 2022]. Compared with kernel  , the decidability proof of nominal
unfoldings is trickier. Based on the substitution of the type body, after every unfolding, the sizeof types will increase. Thus a straightforward induction on the size of types does not work. Zhou
et al. choose a size measure based on an over-approximation of the height of the fully unfolded
tree. Concretely, they de�ne a height function:⌘486⌘C (>)⌘486⌘C (U)⌘486⌘C ( ! ⌫)⌘486⌘C (`U . )

=
=
=
=

0

(U) if U 2 else 0
1 + max(⌘486⌘C ( ), ⌘486⌘C (⌫))
1 + let 8 = ⌘486⌘C ,U7!0 ( ) in ⌘486⌘C ,U7!8+1 ( )The size measure of a type is de�ned as ⌘486⌘C ( ) where the context is empty. In contrast to
kernel  , the context here is used to store the size of the corresponding recursive variables. Zhou
et al. proved that such height measure will precisely decrease by one for every nominal unfolding.
Decidability of  . Now consider how to combine these two approaches together. We wish toextend the measure of nominal unfoldings with the measure of kernel  non-invasively. The
easiest thing to do is to switch the maximum function to addition for the function case in themeasure of nominal unfoldings, which simply widens the over-approximation. Then we consider
the major di�erences between the two approaches. There are three main challenges:• The measures for variables are inconsistent in the two approaches: In the height function,
the type variable case is a base case, while in the weight function we will continue the computation`
for a variable by getting its bound from the contexts. In  , a recursive variable is regarded as auniversal variable, so the new formulation should re�ect those two distinct situations.
• The purposes of contexts are inconsistent in two approaches: The context of the heightfunction is used to store the pre-computed size of the recursive type body so that measures ofrecursive variables are counted in their nominal unfolded form. The context of the weight function
is a straightforward bookkeeping of universal bounds. In later computation, these bounds will be
retrieved and their measure will be computed to serve as the measure of a universal variable.
This is to ensure that the premises in rule S��������� have a smaller measure of types than the
conclusion does. We need to treat both designs carefully if we want a uni�ed context.
• The measure information is lost in the bounded quanti�cation case: Recall that we employ the rule S�������� instead of the standard rule S���������� for  . Since we impose
equivalent bounds for kernel  , for the subtyping relation ` 8(U  1 ). ⌫ 1  8(U  2 ). ⌫ 2 ,the measure would consist of the measures of type 1 , 2 , ⌫ 1 and ⌫ 2 . However, the measure forthe premise , U  2 ` ⌫ 1  ⌫ 2 will lose the measure of type 1 because we do not store it.
`

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:20

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

We �rst show the measure used for the decidability of  , and then discuss how it addresses
the concerns above. The measure is relatively simple and based on the approach from Zhou et al.
[2022]. Similarly, we de�ne a context := · | , U 7! 8 which is used to store the measures of (bothuniversal and recursive) variables during the measure computation, where 8 represents a natural
number. Then, a measure function B8I4 ( ), de�ned on types, is:`

B8I4 (nat)
B8I4 (>)
B8I4 ( ! ⌫)B8I4 ( U )

=
=
=
=

B8I4 (U)=

B8I4 (8(U  ). ⌫)B8I4 (`U . )

=
=

1
1
1 + B8I4 ( ) + B8I4 (⌫)
1 + B8I4
( )
(
(U)
U2
1+
0
U8
let 8 := B8I4 ( ) in 1 + 8 + B8I4 ,U7!8 (⌫)
let 8 := B8I4 ,U7!1 ( ) in 1 + B8I4 ,U7!8 ( )The formulation of the size function is very similar to the height function. We have an extra rule foruniversal types, and slightly adjust the variable and recursive cases. The measure of universal types
is the sum of the measure of the bound and the measure of the body. For variables, one is added
when they are retrieved. Accordingly, we do not need to add one when storing the size of recursive
variables into the context. For atomic constructs, we follow the weight function and measure themas 1.
We solve the �rst challenge in a straightforward way: there is no need to distinguish between
recursive and universal variables. The fact that all recursive variables in the context are bounded
by a top type whose measure is simply one �ts our needs naturally.
As for the second concern, despite the di�erent purposes of contexts, the key ideas of measuringtypes in kernel  and nominal unfoldings are the same: they both relate the measure of a variable
to its true meaning, either its unfolded form or its bound size. A slight modi�cation is madebased on the de�nition of weight. In the weight function, for a universal variable, its bound is �rst
retrieved and then the measure is computed. To align with the “pre-computation” mechanism of
measuring nominal unfoldings (8 := B8I4 ,U7!1 ( )), we also pre-compute the measure of the bound(8 := B8I4 ( )) in the size function, so that we retrieve the measure instead of the type bound fromthe context. In a well-formed type, variables are guaranteed to be unique, so we can use a single
context to store the measures for both recursive variables and universal variables.
A subtler issue lies on variables in the initial subtyping context. When measuring nominal
unfoldings, the context in a subtyping relation is simply a list of variables, without any boundinformation, so variables that occur freely can be counted as 0. In contrast, now the subtyping
context stores the bound information, and the measures of bounds play a role in deciding thesubtyping relation. To address this issue, we need to make sure that the bound information is
pre-computed in the measure function. We transform a subtyping context into an environment
containing measures , which tracks universal variables. In our decidability proof statement(Lemma 4.6), is computed from the subtyping context by an evaluation function 4E0; : õ! ,de�ned as:
4E0; (·)= ·0
4E0; ( , G : )= 4E0; ( 0)0
4E0; ( , U  ) = let 0 = 4E0; ( 0) in 0, U 7! B8I4 0 ( )With both 4E0; and B8I4 we can then state the decidability theorem:
Lemma 4.6. If B8I44E0; ( ) ( ) + B8I44E0; ( ) (⌫)  : thenTheorem 4.7 (Decidability).

` ⌫ is decidable.

` ⌫ is either true or not.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:21

As for the third concern, note that in  , the subtyping relation is antisymmetric [Baldan et al.
1999]. Adding recursive types does not change the property of antisymmetry. However, the additionof records makes the subtyping relation not antisymmetric: two record types may be syntacticallydi�erent. The lack of antisymmetry poses a challenge for our decidability proof, in particular for
rule S��������. However, the �elds of two equivalent records must be a permutation of each other.
Therefore, the measures of two equivalent record types are the same. As a result, the measure oftwo equivalent bounds 1 and 2 is equal, as Lemma 4.8 describes. The measure information oftype 1 can therefore be reconstructed from type 2 , addressing the �nal concern with decidability.
Lemma 4.8. If
4.3`

 ⌫ and`⌫ 

then B8I44E0; ( ) ( ) = B8I44E0; ( ) (⌫).

Conservativity

One important feature of  is that it is conservative over kernel  . Conservativity means that`equivalent  judgments in  should behave in the same way as in  . For instance, if a subtyping`
statement is valid in  , then it should also be valid in  . Dually, if a subtyping statement over`
 -types is invalid in  , then it should also be invalid in  . In some calculi, including extensions of with equi-recursive types [Ghelli 1993], conservativity is lost after the addition of new features.
For avoiding ambiguity, let ` , ` , ` ⌫, ` 4 and ` 4 : represent the wellformedness of environment, well-formedness of types, subtyping, well-formedness of expressions
and the typing relation, respectively, in kernel  . Note that all these judgments are essentiallysubsets of the judgments introduced in §3, except that the rules involving records and recursive
types are removed, and that the rule S�������� is replaced with the rule S����������.
`Conservativity of subtyping. Our conservativity result for subtyping is relatively easy to establish:
Lemma 4.9 (Conservativity for subtyping). If `if `  ⌫.

,

`

, and

` ⌫ then` ⌫ if and only

Here the well-formedness conditions ensure that , and ⌫ must be respectively a valid environment, and valid  types. That is they cannot contain recursive types (or record types).
Therefore, the lemma states that for environments and types without recursive types, the two`
subtyping relations (for  and  ) are equivalent, accepting the same statements. The only hurdle
is that to establish the correspondence between rule S�������� and the rule S���������� inkernel  , we need the antisymmetry property for kernel  [Baldan et al. 1999].
Conservativity of typing. It is straightforward to obtain part of the conservativity result from`a typing relation in  to a typing relation in  . As for the reverse direction, the situation ismore complicated. If we want to derive ` 4 : from ` 4 : , when doing induction, for the
subsumption case (rule ����������), we need to guess an intermediate type. However, we do notknow if it involves recursive types or not. Consider the following example:` _G . G : > ! >` > ! >  (`U . >) ! >` _G . G : (`U . >) ! >` (`U . >) ! >  >����������
` _G . G : >Although ` _G . G : > do not involve recursive types, the typing subderivations can contain recursive
types. As a result, the induction hypothesis cannot be applied.
`This problem can be addressed by employing the algorithmic formulation of  , shown in §3.4.
With algorithmic typing, we can have more precise information about the types of an expression,
since algorithmic typing always gives the minimum type. Therefore, it can be proved that for����������

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:22

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

expressions that do not use fold/unfold constructors, their minimum types do not contain recursive
types as well. Conservativity for algorithmic typing is proved as follows:
Lemma 4.10. If `,`and ` 4 then`0 4 :

implies` 4: .

Now, given a typing relation ` 4 : in  , we �rst use the minimum typing property (Theorem
3.9) to obtain its minimum type ⌫ such that `0 4 : ⌫ and ` ⌫  . Applying Lemma 4.10 and`Lemma 4.9, we complete the conservativity proof for the declarative version of  .
Theorem 4.11 (Conservativity). If `5`and ` 4 then

`

,

` 4:

if and only if`4 : .

A CALCULUS WITH LOWER AND UPPER BOUNDED QUANTIFICATIONIn this section we introduce an extension of  , called  , with lower bounded quanti�cation
and a bottom type. While upper bounded quanti�cation has received a lot of attention in previous
research, lower bounded quanti�cation for an  -like language is much less explored, though it
appears in a few works [Amin and Rompf 2017; Oliveira et al. 2020]. We follow the same approachas Oliveira et al. [2020], where their  extension allows type variables to have either a lower
bound or an upper bound, but not both bounds at once. As discussed in §2.2, this extension enables
further applications, such as a form of extensible encodings of datatypes. We have proved all the``same results for  that were proved for  , including type soundness, decidability, transitivity
and conservativity over  .
`

5.1

The

`


`

Calculus

The syntax of types, expressions, values and contexts for the extended  calculus is shown below.
The main novelties are that bottom types and lower bounded quanti�cation are introduced. The
syntactic additions are highlighted in gray .
Types, ⌫, . . . F nat | > | ? | 1 ! 2 | U | `U . | U). ⌫ | {;8 : 8 8 21···= }| 8(U  ). ⌫ | 8(U`Expressions 4

F

ValuesF

E

Contexts

F

G | i | 4 1 4 2 | _G : . 4 | 4 | ⇤(U  ). 4 | ⇤(U). 4
821···=| unfold [ ] 4 | fold [ ] 4 | {;8 = 48
} | 4.;
i | _G : . 4 | fold [ ] E | ⇤(U  ). 4 | ⇤(U). 4
821···=| {;8 = E8}
· | ,U  | ,U
| ,G :

Subtyping, typing and reduction. Similarly to §3.1, the well-formedness for the additional bottom`
types and universal types with lower bounds are standard. Figure 4 shows the additional rules of ``with respect to  for subtyping, typing and reduction. Compared with  , we add rule S����, S����������� and S����������, which are the dual forms of rule S����, S��������� and S��������,respectively. The rule ������������� and ������������� are the dual forms of rule ����������� and����������� for typing, respectively. The rule ����������� rule is the dual form of rule ���������
for reduction.
The new subtyping relation is re�exive and transitive:
Theorem 5.1 (Re�exivity for` ). If ``Theorem 5.2 (Transitivity for  ). If

and
`

`

then

 ⌫ and` .

` ⌫  ⇠ then

`

 ⇠.

Structural folding and lower bounded quanti�cation. The structural folding rule ������������
`on recursive types has already been shown for  . Note that this rule is not strictly necessary for` , because a recursive type can only be a subtype of another recursive type or the > type. Thus
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

`

48:23

(Subtyping)

⌫

S����

`

S�����������

`A

B2

U

`?A

`AB

`AU

S����������

` A1  A2

` 8(U

`4 :

�������������

` e : 8(UB1 ). B2

` A2  A1, U

A1 ). B  8(UA2 ` B  C

A2 ). C�������������

` B1  A, U` e A : [U 7! A] B2(Typing)A`e:BA). e : 8(U

` ⇤(U

A). B
(Reduction)

4 1 õ! 4 2
�����������

(⇤(U

A). e) B õ! [U 7! B] e``

Fig. 4. Additional subtyping, typing and reduction rules for  with respect to  .

the e�ect of structural folding in  , can be subsumed by other subtyping/typing rules. Perhaps
for this reason, Abadi et al. [1996] have only considered a structural unfolding rule. However, in` , a recursive type can also be a subtype of a type variable. In this case, the structural folding
rule can give the desired typings to the Add8 constructors of the Exp1 and Exp2 datatypes that wehave presented in §2.2, while the standard folding rule cannot. The rule ������������ has the same``
form in  as in  . Therefore, we believe that the structural folding rule that we have proposed,
together with the structural unfolding lemma in the metatheory, is general.
`

Type soundness. Our type soundness proof for
Theorem 5.3 (Preservation for
Theorem 5.4 (Progress for
5.2

Metatheory of

`


`


). If ` 4 :). If ` 4 :`

is standard, thus we have:and 4 õ! 4 0 then ` 4 0 : .

then 4 is a value or exists 4 0, 4 õ! 4 0.

`

The addition of lower bounded quanti�cation and the bottom type creates some di�culties in the`metatheory of  . The proof strategies for the unfolding lemma, decidability and conservativity,`
as we showed in the §4 for  , require some adjustments. In the following, we describe how to
overcome the di�culties. We refer readers to the appendix for more details.
Unfolding Lemma. A type system that simultaneously allows introducing lower and upperbounded type variables will break the proof for the unfolding lemma shown in §4.1. The interactionof lower bounds and upper bounds invalidates the following inversion lemma for rule S���������,which has been used to prove the unfolding lemma:
Lemma 5.5. If U 

2 ,` U  ⌫, and U < ⌫ then

`

 ⌫.

This lemma holds when the bounds in the context can only have one direction. However, when
we have both kinds of bounds in the context, a counter-example can be found as follows:G  >, ~G `G ~=)\G  >, ~G `>~

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:24

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

For avoiding using this inversion lemma in the proof of unfolding lemma, we need to re�ne thegeneralized unfolding lemma. In Lemma 4.5, there is more than one subtyping statement on thepremises related to type and ⌫, and we do induction on the premise (1). In the re�ned generalized
unfolding lemma, we integrate those subtyping statements into one statement, thus the premise (1)can be induced implicitly. Meanwhile, the context is also re�ned to be more general. The concrete`
generalized unfolding lemma for  is shown in the appendix. With these changes we prove:
Lemma 5.6 (Unfolding lemma for`U . ⌫] ⌫.

). If

`


 `U . ⌫ then

` `U .

` [U 7! `U . ] [U 7!

Decidability. The interaction between bottom types and rule S�������� breaks the measure`based decidability proof in §4.2. The bottom type in  brings a new form of equivalent types:
when U  ? 2 , one can derive that ` U  ? and ` ?  U, as observed by Pierce [1997].
Simply extending the measure function with B8I4 (?) = 1 will not work. For type variables, themeasure function will recursively look up its bound in the context, and add one to the measure ofits bound, making a variable equivalent to ? to have a larger measure than ?. Therefore, replacing
two equivalent types into the abstracted type body may not produce the same measures. We canconstruct derivations of rule S�������� that have a larger measure in the premise than that of theconclusion, which makes the decidability proof fail with the current measure.
We solve this issue by replacing all the type variables who are a subtype of bottom by bottom.
Every time that we compute the size for a variable bounded by an upper bound, we �rstly recursively
check whether it is a synonym for bottom, and return the size of bottom if it is. This can be
implemented by an extension to the measure context . Dually, when we compute the size for avariable bounded by a lower bound, we recursively check if it is the supertype of top. With thischange the measures work, and we can prove decidability.
Theorem 5.7 (Decidability for

`


).

`


is decidable.

Conservativity. The proof of conservativity for  follows the same pattern as the proof for  .
To prove conservativity of typing, we need the help of the algorithmic typing rules to obtain theminimum type of an  term. However, the introduction of bottom types requires us to add several
new algorithmic typing rules, since in the declarative system, one can always use the subsumption
rule to transform a term with type ? to any function type or universal type, and apply it to anyargument, as also observed by Pierce [1997]. We also develop a similar treatment for recursive
types. Moreover, the meanings of the two exposure functions also need to be re�ned. For example,
the upper exposure function (*) is now used to �nd the least non-upper-bounded-variable upperbound in the context, so it will return the variable itself if the variable is lower bounded. For lower
exposure, we also need a dual form of the rule XA��������, which �nds the non-variable lower
bound for a variable:``

XA������������

U
The complete set of``A + B`U + Balgorithmic typing rules can be found in the appendix.

Theorem 5.8 (Conservativity for`4 : .
6

A2`
). If `,`and ` 4 then

` 4 :if and only if

RELATED WORK

Bounded Quanti�cation and Recursive Types. Bounded quanti�cation was �rstly introduced by
Cardelli and Wegner [1985] in the language Fun, where their kernel Fun calculus corresponds
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:25

to the kernel version of  . The full variant of  was introduced by Curien and Ghelli [1992]
and Cardelli et al. [1994], where the subtyping for bounds are contravariant. Although full  ispowerful, subtyping is proved to be undecidable [Pierce 1994]. As discussed in §1 there are several
attempts to add recursive types to  , such as the work by Ghelli [1993], Colazzo and Ghelli [2005]
and Je�rey [2001]. Unfortunately, as Table 1 shows, such combinations are not painless, and eventhe successful combinations require the signi�cant changes for the subtyping rules.
Ghelli illustrates how the combination of equi-recursive subtyping and full  changes theexpressiveness power of the subtyping relation with a simple example:⌫⌘ 8U . (8(U 0  U).
⌘ 8(V  ⌫). V

U)

0

'

⌘ 8(V  ⌫). 8(V 0  V). V⌘ 8(V  ⌫). `- . 8(V 0  - ).

-

where
stands for ! > and 8U . is the abbreviation of 8(U  >). . In full  ,  0 does
not hold. However, such system allows  ' and '  0 to be derived, which by transitivity, allows
us to conclude that  0. In Colazzo and Ghelli’s work, there is no independent universal type,
and the shape of recursive types is either `U .8(G  ). ⌫ or `U . ! ⌫. The recursive variables
and universal variables are distinct, resulting in changes in environments and subtyping rules. For
example, the subtyping environment is de�ned as ⇧ := · | ⇧, (G, ~)  ( , ⌫) | ⇧, (U = , V = ⌫),and the rule S��������� rule of  is changed to:(G, ~)  ( 0, ⌫ 0) 2 ⇧8U 0, ⌫ < U 0⌫ <> ⌫ <~ ⇧ ` 0  ⌫⇧`G ⌫
The algorithm proposed by Je�rey is also complex, and requires major changes. Both recursive
variables and the subtyping algorithm are labelled polarly, and the implementation of U-conversion
is not discussed. In contrast, our subtyping rules do not change the contexts, the types are not
restricted, and most importantly, we do not have to change the rules in the original  . This has
the bene�t that we can largely reuse the existing metatheory of the original  , and it also enables
our conservativity result. While it is plausible that Je�rey’s or Colazzo and Ghelli’s work for the
kernel  extensions with recursive types are conservative, this has not been proved. Furthermore,such proof is likely to be non-trivial because of the major changes introduced by equi-recursive
subtyping.
There are many other extensions to  . Bounded existentials are also studied by Cardelli andWegner [1985]. Existential types can be encoded by universal types, thus we can obtain a formof bounded existentials for free in  [Cardelli and Wegner 1985]. Another important extension
is f-bounded quanti�cation, �rstly proposed by Canning et al. [1989], then studied by Baldan
et al. [1999] in terms of the basic theory. In f-bounded quanti�cation, the bounded variables areallowed to appear in the bound. For example, a bound of the form 8(U  [U]). ⌫, where is a
type-level function applied to U, is allowed in f-bounded quanti�cation. We can encode polymorphic
binary methods [Bruce et al. 1995] and methods that have recursive types in their signatures withf-bounded quanti�cation. For the example that we have showed in §2.2, the bound in the translatefunction is not Point but would have a form [U] = {G : Int, ~ : Int, move : Int ! Int ! U }.
Therefore, with f-bounded quanti�cation the translate function could have the type:8(U  {G : Int, ~ : Int, move : Int ! Int ! U }). U ! U

Then the U can instantiate to Point or subtypes of Point, because Point  [Point]. Note that for
subtyping statements such as U  {G : Int, ~ : Int, move : Int ! Int ! U } to hold, they must
be interpreted using equi-recursive subtyping, since the f-bounds are normally records, and an
iso-recursive type cannot be the subtype of a record. This approach is appealing because it caneven deal with binary methods, where recursive types appear in negative positions. For example,
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:26

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveirawith f-bounded quanti�cation we can model bounds such as U  {G : Int, eq : U ! Bool}, and still
have the expected subtyping relations.
Whereas we show that with the structural unfolding rule we can model positive cases of f-bounded`
quanti�cation (such as translate) in  , we can only model a restricted form of negative f-bounded`
quanti�cation. For instance in  we can have the bound U  ` P. {G : Int, eq : P ! Bool} and we
can instantiate U with % (where % = ` P. {G : Int, eq : P ! Bool}). However, we would not be able
to instantiate U with some types that have extra �elds, such as ` P’. {G : Int, ~ : Int, eq : P’ ! Bool}for example. In contrast, f-bounded quanti�cation allows such forms of instantiation. Nevertheless,`given the overlap between some of the applications of iso-recursive types in  and f-bounded
quanti�cation, we believe that it is worthwhile to investigate whether f-bounded quanti�cation
can be avoided to deal with general binary methods.
Dependent Object Types. The interest in languages with bounded quanti�cation and recursive
types has been reignited recently in the research community with the introduction of the dependent
object types (DOT) [Rompf and Amin 2016] calculus. DOT is the foundation of Scala 3 [EPFL 2021],
and also employs a generalized form of bounded quanti�cation and recursive types. The generalized
form of bounded quanti�cation subsumes both upper and lower bounded quanti�cation, which are`present in  . DOT supports both upper and lower bounds at the same time for path selection.
In addition, DOT also supports path-dependent types [Amin et al. 2014] and intersection types[Barbanera et al. 1995; Coppo et al. 1981; Pottinger 1980]. DOT can encode full  [Rompf andAmin 2016] and has been shown to be undecidable [Hu and Lhoták 2020; Mackay et al. 2020]. Oneof the limitations for DOT is that transitivity elimination is not possible [Rompf and Amin 2016],
and even the decidable fragments of DOT lack transitivity [Hu and Lhoták 2020; Mackay et al.
2020]. The research on DOT has been intimately related to  . For instance, Amin and Rompf[2017] explain many of the features of DOT by incrementally extending  . In addition, there havebeen various attempts to prove the undecidability of DOT by a reduction to the undecidability
problem in  . Although, as Hu and Lhoták [2020] observed, DOT is not conservative over  .
Thus an undecidability result for DOT cannot be proved by reduction to the undecidability of full`
 . While  does not have all the features of DOT, our results can potentially help in research inthat area, where the decidable fragments of DOT lack important properties such as transitivity. In`
addition  preserves the conservativity over  , while DOT does not.
Object Encodings. Recursive records can encode objects [Bruce et al. 1999; Canning et al. 1989;
Cook et al. 1989]. Alternatively, existential types can also be used to encode objects [Pierce andTurner 1994], or they can be employed together with recursive types [Bruce 1994]. Pierce andTurner’s object encoding is notable in that it requires only  , and does not employ recursive
types. The ORBE encoding, presented by Abadi et al. [1996] consists of recursive types, boundedexistential quanti�cation, records, and the structural unfolding rule. In their work, an interface is
encoded as:$'⌫⇢ ( ) , `U . 9(V  U). V ⇥ (V ! (V))

As Bruce et al. observe, the ORBE encoding requires full  for the bounded quanti�cation subtyping
rule. When we try to compare two bounds, the type variable will be substituted with the existential
types, which may result in bounds that are not equivalent. The overview paper by Bruce et al. [1999]
makes a detailed comparison among di�erent object encodings. Except for the ORBE encoding,` could serve as a target for the existing object encodings. However, no complete formalizationof  with recursive types with desirable properties (such as type soundness and conservativity)
existed at the time. Our work helps to further validate such encodings by providing a complete
formalization of  with recursive types, together with various desirable properties.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:27

Algebraic Datatypes and Subtyping. Algebraic datatypes are a fundamental feature in modern
functional programming languages, such as Haskell [Haskell Development Team 1990] and Ocaml[INRIA 1987]. However, such languages do not support subtyping between datatypes. Hosoya
et al. [1998] discussed the interaction between mutually recursive datatypes and subtyping. They
presented two variants of  extending  with user-de�ned datatype declarations. The �rst variant
has user-de�ned subtyping declarations between datatypes, and can be viewed as having a formof nominal subtyping. The second variant allows structural subtyping among the datatypes. One
advantage of employing user-de�ned datatypes is that it is simple to deal with formally, and that itallows mutually recursive datatype de�nitions easily. However, they do not support conventional`
recursive types of the form `U . as we do in  . Moreover, they do not consider lower bounded
quanti�cation which, as argued in §2.2, seems to be quite useful in a system targeting algebraic
datatypes. There has been some work integrating ML datatypes and OO classes [Bourdoncle andMerz 1997; Millstein et al. 2004]. In the implementation of hierarchical extensible datatypes, methods
are simulated via functions with dynamic dispatch. Those works are focused on the design ofintermediate languages that have complex constructs such as classes or datatypes. In contrast, wedevelop foundational calculi, where more complex constructs can be encoded. Finally, Poll [1998]
investigated the categorical semantics of datatypes with subtyping and a limited form of inheritanceon datatypes, improving our understanding on the relation between categorical datatypes andobject types.
Oliveira [2009] showed encodings of algebraic datatypes with subtyping assuming a variant of extended with records, recursive types and higher kinds. He showed that adding subtyping
to datatypes allows solving the Expression Problem [Wadler 1998]. However, as we mentionedin §2.2, he did not formalize the  extension, although he showed a translation of the encoding
into Scala. Moreover, his encoding is more complex than ours because he employs upper bounded
quanti�cation with higher kinds. In §2.2, we showed that �rst-order lower bounded quanti�cation`in  , together with the structural folding rule enables such encodings. Like for encodings ofobjects, our work is helpful to further validate such encodings formally.
7

CONCLUSION

Recursive types and bounded quanti�cation are important in many programming languages.
However, although those features are well-studied independently, their interaction has posed a`long term challenge. Our  calculus illustrates how to integrate iso-recursive types and kernel  .
We obtain a transitive and decidable subtyping relation, while the full calculus is shown to be``conservative over  and is proven to be type-sound.  and  could serve as a theoretic
foundation for object encodings and encodings of algebraic datatypes with subtyping. With therenewed interest on recursive types and bounded quanti�cation due to the DOT calculus, we
believe that our work is also helpful to �nd calculi with most features in DOT, while retaining
desirable properties, such as decidability and transitivity of subtyping, or even conservativity over`
 . Investigating extensions of  with some of the features of DOT is a clear avenue for future
work. In addition, studying the combination of iso-recursive subtyping and full  , could be usefulfor modelling the ORBE encoding [Abadi et al. 1996].
ACKNOWLEDGMENTS
We thank the anonymous reviewers for their helpful comments. This work has been sponsored byHong Kong Research Grant Council projects number 17209519, 17209520 and 17209821.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:28

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

REFERENCES
Martín Abadi, Luca Cardelli, and Ramesh Viswanathan. 1996. An interpretation of objects and object types. In Proceedingsof the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 396–409.
Roberto M. Amadio and Luca Cardelli. 1993. Subtyping recursive types. ACM Transactions on Programming Languages andSystems (TOPLAS) 15, 4 (1993), 575–631.
Nada Amin and Tiark Rompf. 2017. Type soundness proofs with de�nitional interpreters. In Proceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages. 666–679.
Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of path-dependent types. Acm Sigplan Notices 49, 10(2014), 233–249.
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 Ma�ei. 2014. Union, intersection and re�nement types and reasoning abouttype disjointness for secure protocol implementations. Journal of Computer Security 22, 2 (2014), 301–353.
Paolo Baldan, Giorgio Ghelli, and Alessandra Ra�aeta. 1999. Basic theory of F-bounded quanti�cation. Information andComputation 153, 2 (1999), 173–237.
Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. Intersection and Union Types: Syntax and
Semantics. Information and Computation 119, 2 (June 1995), 202–230.
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Ma�eis. 2011. Re�nement types
for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS) 33, 2 (2011), 1–45.
Corrado Böhm and Alessandro Berarducci. 1985. Automatic synthesis of typed Lambda-programs on term algebras.
Theoretical Computer Science 39, 2-3 (1985).
François Bourdoncle and Stephan Merz. 1997. Type checking higher-order polymorphic multi-methods. In Proceedings ofthe 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 302–315.
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.
Kim Bruce, Luca Cardelli, Giuseppe Castagna, Hopkins Objects Group, Gary T Leavens, and Benjamin C. Pierce. 1995. On
binary methods. Theory and Practice of Object Systems 1, 3 (1995), 221–242.
Kim B Bruce. 1994. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of
Functional Programming 4, 2 (1994), 127–206.
Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. 1999. Comparing Object Encodings. Information and Computation 155,
1.
Peter Canning, William Cook, Walter Hill, Walter Oltho�, and John C. Mitchell. 1989. F-Bounded Polymorphism for ObjectOriented Programming. In Proceedings of the Fourth International Conference on Functional Programming Languages andComputer Architecture (Imperial College, London, United Kingdom) (FPCA 1989). 8 pages.
Luca Cardelli. 1985. Amber. In LITP Spring School on Theoretical Computer Science. Springer, 21–47.
Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1994. An extension of system F with subtyping.
Information and computation 109, 1-2 (1994), 4–56.
Luca Cardelli and Peter Wegner. 1985. On understanding types, data abstraction, and polymorphism. ACM Computing
Surveys (CSUR) 17, 4 (1985), 471–523.
Giuseppe Castagna and Benjamin C. Pierce. 1994. Decidable Bounded Quanti�cation. In Proceedings of the 21st ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, Oregon, USA) (POPL ’94). Association
for Computing Machinery, New York, NY, USA, 151–162.
Alonzo Church. 1932. A set of postulates for the foundation of logic. 33, 2 (1932), 346–366.
Dario Colazzo and Giorgio Ghelli. 2005. Subtyping recursion and parametric polymorphism in kernel fun. Information andComputation 198, 2 (2005), 71–147.
William R. Cook, Walter Hill, and Peter S. Canning. 1989. Inheritance is Not Subtyping. In Proceedings of the 17th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’90). Association for Computing Machinery.
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional characters of solvable terms. Mathematical
Logic Quarterly 27, 2-6 (1981), 45–58.
Pierre-Louis Curien and Giorgio Ghelli. 1992. Coherence of subsumption, minimum typing and type-checking in F.
Mathematical structures in computer science 2, 1 (1992), 55–91.
EPFL. 2021. Scala 3. https://www.scala-lang.org/
Vladimir Gapeyev, Michael Levin, and Benjamin C. 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).
Giorgio Ghelli. 1993. Recursive types are not conservative over F. In International Conference on Typed Lambda calculi andApplications. Springer, 146–162.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:29

Jean-Yves Girard. 1972. Interprétation fonctionnelle et elimination des coupures de l’arithmétique d’ordre supérieur. Thèsed’état. Université de Paris 7.
Haskell Development Team. 1990. Haskell. https://www.haskell.org/
Haruo Hosoya, Benjamin C. Pierce, and David N. Turner. 1998. Datatypes and subtyping. Unpublished manuscript (1998).
Jason ZS Hu and Ondřej Lhoták. 2020. Undecidability of D<: and its decidable fragments. Proceedings of the ACM on
Programming Languages 4, POPL (2020), 1–30.
INRIA. 1987. OCaml. https://ocaml.org/
Alan Je�rey. 2001. A symbolic labelled transition system for coinductive subtyping of F` types. In 2001 IEEE Conference on
Logic and Computer Science (LICS 2001). 323.
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.
Julian Mackay, Alex Potanin, Jonathan Aldrich, and Lindsay Groves. 2020. Decidable subtyping for path dependent types.
Proc. ACM Program. Lang. 4, POPL (2020), 66:1–66:27.
Todd Millstein, Colin Bleckner, and Craig Chambers. 2004. Modular typechecking for hierarchically extensible datatypes
and functions. ACM Transactions on Programming Languages and Systems (TOPLAS) 26, 5 (2004), 836–889.
James Hiram Jr Morris. 1969. Lambda-calculus models of programming languages. Ph.D. Dissertation. Massachusetts Instituteof Technology.
Bruno C. d. S. Oliveira. 2009. Modular visitor components. In European Conference on Object-Oriented Programming. Springer,
269–293.
Bruno C. d. S. Oliveira, Shaobo Cui, and Baber Rehman. 2020. The Duality of Subtyping. In 34th European Conference on
Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference) (LIPIcs), Robert
Hirschfeld and Tobias Pape (Eds.).
Michel Parigot. 1992. Recursive programming with proofs. Theoretical Computer Science 94, 2 (1992), 335–356.
Benjamin C. Pierce. 1994. Bounded quanti�cation is undecidable. Information and Computation 112, 1 (1994), 131–165.
Benjamin C Pierce. 1997. Bounded quanti�cation with bottom. Technical Report. Citeseer.
Benjamin C. Pierce. 2002. Types and programming languages. MIT press.
Benjamin C Pierce and David N Turner. 1994. Simple type-theoretic foundations for object-oriented programming. Journalof functional programming 4, 2 (1994), 207–247.
Erik Poll. 1998. Subtyping and Inheritance for Categorical Datatypes: Preliminary Report (Type Theory and its Applications
to Computer Systems). Kyoto University Research Information Repository 1023 (1998), 112–125.
Garrel Pottinger. 1980. A type assignment for the strongly normalizable _-terms. To HB Curry: essays on combinatory logic,
lambda calculus and formalism (1980), 561–577.
John C. Reynolds. 1974. Towards a theory of type structure. In Colloque sur la Programmation. Springer, 408–425.
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.
Davide Sangiorgi and Robin Milner. 1992. The Problem of “Weak Bisimulation up to”. In CONCUR, Vol. 630. 32–46.
Dana Scott. 1962. A system of functional abstraction. (1962). Lectures delivered at University of California, Berkeley,
California, USA, 1962/63.
Philip Wadler. 1998. The Expression Problem. (1998). discussion on the Java Genericity mailing list.
Yaoda Zhou, Bruno C. d. S. Oliveira, and Jinxu Zhao. 2020. Revisiting Iso-Recursive Subtyping. Proc. ACM Program. Lang. 4,
OOPSLA (2020).
Yaoda Zhou, Jinxu Zhao, and Bruno C. d. S. Oliveira. 2022. Revisiting Iso-Recursive Subtyping. ACM Transactions on
Programming Languages and Systems 44, 4, Article 24 (2022).

A

METATHEORY OF`In §5.2 we brie�y discussed how to overcome the issues when proving the important properties of` . In this section we will provide more details. For full details, we suggest readers to consult ourmechanized proof.
A.1

Unfolding Lemma

The generalized unfolding lemma in both Zhou et al. [2022] and §4.1 are relied on inversion
properties for every subtyping rule, like Lemma 4.1 and Lemma 4.5. It is because in the generalized
unfolding lemma, we have 2 subtyping statements related to type and ⌫. However, when a typesystem involves subtyping rules where the inversion properties do not hold, such as intersection
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:30

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira

types or bounded quanti�cation with both upper bounds and lower bounds (as  ), the current
generalized unfolding lemma cannot be applied.
By observing the form of the generalized unfolding lemma (Lemma 4.5), we can see that, when
we apply the nominal unfolding rules for iso-recursive types, the conditions (1) and (2) raised by
the goals implicitly subsume the premise (1). That is because 1-time unfoldings can be derivablefrom general nominal unfoldings. With such an important observation, we merge 2 subtyping
statements related to type and ⌫ into 1. To accommodate this change, the context is also needed`
to re�ne. Formally, the generalized unfolding lemma for  is:`

Lemma A.1 (Generalized unfolding lemma for

`


). If

(1) 1, U  >, 2 ` and 1, U  >, 2 ` ⌫;(2) ⌧ ` [U 7! ⇠ U ]  [U 7! ⇡ U ] ⌫;(3) ⌧ di�ers from 1, U  >, 2 [U 7! ( U ] only in the components labelled by U, where ( U canbe replaced by ) U that satis�es 2 ` `U . (  `U . ) and 2 ` `U . )  `U . (,
then

(1)

1 ` `U . ⇠  `U . ( and 1 ` `U . (  `U . ⇡ implies 1,[U 7! `U . ⇡] ⌫;(2) 1 ` `U . ⇡  `U . ( and 1 ` `U . (  `U . ⇠ implies 1,[U 7! `U . ⇡] ⌫.

2 [U 7! `U . (] ` [U 7! `U . ⇠]



2 [U 7! `U . (] ` [U 7! `U . ⇠]

P����. Do induction on premise (2) and then premise (1), respectively.
A.2⇤

Decidability

In §5.2, we said that the introduction of bottom types breaks the measure approach for decidability
shown in §4.2. A counter-example is that:U  ?, V  U ` U  V
U  ?, V  U ` V  U
U  ?, V  U, W  V `U  ?, V  U ` 8(W  U).  8(W  V). ⌫⌫

The measure for premise (3) is:

B8I4U7!1, V7!2, W 7!3 ( ) + B8I4U7!1, V7!2, W 7!3 (⌫)
while the measure for the goal is:
B8I4U7!1, V7!2 (8(W  U). ) + B8I4U7!1, V7!2 (8(W  V). ⌫)õ! B8I4U7!1, V7!2, W 7!2 ( ) + B8I4U7!1, V7!2, W 7!3 (⌫)
which is less than the measure of premise (3).
This issue can be solved by replacing all the subtypes of bottom types with bottom. That way,
the subtyping relation U  ?, V  U ` 8(W  U).  8(W  V). ⌫ becomesU  ?, V  ? ` 8(W  ?).

 8(W  ?). ⌫and the measure works again.
This idea can be implemented by modifying the measure function to identify upper/lower
bounded variables that are equivalent to bottom/top types. Firstly, the context is rede�ned as:= · | , U 7! 8 | , U 7! ? | , U 7! >, which is used to store the measure of variables orindicate them as upper bounded by ? or lower bounded by >. Then, a measure function B8I4 ( )Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

Recursive Subtyping for All

48:31

is rede�ned as:
B8I4 (nat)
B8I4 (>)
B8I4 (?)
B8I4 ( ! ⌫)B8I4 ( U )

=
=
=
=
=

B8I4 (U)=

B8I4 (8(U  ). ⌫)=B8I4 (8(U=B8I4 (`U . )8B⌫>C (?)
8B⌫>C ,U7!? (U)
8B⌫>C ,V7!_ (U)otherwise 8B⌫>C ( )

). ⌫)

=

1
1
1
1 + B8I4 ( ) + B8I4 (⌫)
1 + B8I4( )(8
U 7! 8 2
1+0otherwise(
1 + B8I4 ,U7!? (⌫)
1+
B8I4 ( ) + B8I4 ,U7!B8I4 ( ) (⌫)(
1 + B8I4 ,U7!> (⌫)
1+
B8I4 ( ) + B8I4 ,U7!B8I4 ( ) (⌫)
let 8 := B8I4 ,U7!1 ( ) in 1 + B8I4 ,U7!8 ( )= true= true= 8B⌫>C (U) if U < V= false8B)>? (>)
8B)>? ,U7!> (U)8B)>? ,V7!_ (U)otherwise 8B)>? ( )8B⌫>C ( )otherwise8B)>? ( )otherwise= true= true= 8B)>? (U) if U < V= falseThe 8B)>? and 8B⌫>C functions basically use the information in the measure context to check
whether the bound type is equivalent to > or ?. If so, when the variable bounded by is looked
up in the context, it will have a measure of 1. In this way, we retain the important property thatequivalent types have the same measure.
A.3

Conservativity

We also proved conservativity of  to kernel  . The conservativity of subtyping is easy to prove.
`
To prove conservativity of typing, we de�ne an algorithmic typing system for  . Compared`to the algorithmic typing rules for  , the two exposure functions are rede�ned, and some extra
rules that deal with corner cases introduced by bottom and top types are added. The changes arepresented in Figure 5. We prove the soundness and completeness of the algorithmic typing system,
and Theorem 5.8 follows.
`

Theorem A.2 (Soundness of the algorithmic rules for
Theorem A.3 (Completeness of the algorithmic rules forthat `0 4 : ⌫ and ` ⌫  .

`


). If
`


). If

`0 4 :`4 :then`4 : .

then there exists a ⌫ such

Received 2022-07-07; accepted 2022-11-07

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.

48:32`

Litao Zhou, Yaoda Zhou, and Bruno C. d. S. Oliveira(Upper Exposure)*⌫

XA��������

U A2

`

`A * BU`U * BXA���

A is not type variable

A2`A * A`U * U(Lower Exposure)+⌫

XA������������U

XA������

A2`A + B`U + B

XA��������

XA���������

A is not type variable

U A2`A + A`U + U`0 4 :(Algorithmic Typing)�����������

`a e1 : A`a e2 : A2

`B * ?

`AB`a e1 e2 : ?

���������������

`a e : A`A * ?

`a unfold [B] e : ?

������������

`a e : B`A`C + >`C`a e A : ?

�������������

`a e : A`B * ?

`a fold [C] e : >`Fig. 5. The new exposure function and additional algorithmic typing rules for  .

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 48. Publication date: January 2023.