Recursive Subtyping for All

Metadata

Title: Recursive Subtyping for All
Venue: JFP
Area: Iso-recursive subtyping
Source URL: https://i.cs.hku.hk/~bruno/papers/jfp25.pdf
Downloaded PDF: Recursive-Subtyping-for-All.pdf
Extracted assets: _assets/Recursive-Subtyping-for-All/
Pages: 55
Embedded image count reported by PyMuPDF: 0

Why this note exists

This note is part of the HKU PL Group literature knowledge base for work on iso-recursive subtyping, intersection types, union types, disjointness, merge operators, and compositional programming. It is designed for later Coding Agent / Proof Agent use during proof search, design brainstorming, and comparison against prior systems.

Extraction quality note

This is the fast pass generated with pymupdf4llm, not the heavier marker-pdf pass. The original PDF is linked above and kept in _pdfs/. Figures/images detected by PyMuPDF are saved under _assets/. Some mathematical notation may still require checking against the PDF, especially inference rules with complex layouts.

Technical landmarks detected automatically

These are line references into the converted Markdown below. They are meant as a quick navigation layer for rules, lemmas, theorems, proofs, algorithms, examples, and counterexamples.

line 5: Recursive Subtyping for All
line 7: LITAO ZHOU1 YAODA ZHOU1 QIANYONG WAN BRUNO C. D. S. OLIVEIRA
line 11: Abstract
line 17: 1 Introduction
line 25: Recursive Subtyping for All
line 49: |Kernel/Full𝐹≤
Equi-/Iso-Recursive|full
kernel
full
kernel
full
kernel
full
equi
equi
equi
equi
iso
iso
iso|
line 66: Recursive Subtyping for All
line 70: formally (Ligatti et al., 2017; Backes et al., 2014; Zhou et al., 2020, 2022): it is difficult to prove results such as transitivity, or define sound and complete algorithmic formulations.
line 78: - 𝐹[𝜇] [extending] [𝐹][≤] [with][iso-recursive][types.][We][have][two][variants][of] [𝐹][𝜇][kernel] ≤ [:] ≤[:]
line 80: - 𝐹[𝜇][the][extension][of][kernel] [𝐹][≤][with][iso-recursive][subtyping,][and][full] [𝐹][𝜇][the] ≤[as] ≤[as]
line 82: - extension of full 𝐹 ≤ with iso-recursive subtyping. We prove several properties for 𝐹[𝜇][including:][type][soundness;][transitivity][of][subtyping;][decidability][of][subtyping] ≤[,]
line 84: - of kernel 𝐹[𝜇] ≤[; undecidability of subtyping of full] [ 𝐹] ≤ [𝜇][; and the unfolding lemma, a key]
line 86: - property to ensure type soundness.
line 100: - An extension of 𝐹[𝜇] ≤ [with intersection types, both upper and lower bounded quan-]
line 104: - Coq formalization: We have formalized all the calculi and proofs in this paper in Coq, and made the formalization available online at https://github.com/juda/ Recursive-Subtyping-for-All/tree/main/JFP .
line 108: 2 Overview
line 116: Recursive Subtyping for All
line 118: 2.1 Bounded Quantification and Recursive Subtyping
line 123:
line 130: kernelall.
line 133:
line 151:
line 154: Despite being less convenient, iso-recursive types are known to have the same expressive power as equi-recursive types (Abadi and Fiore, 1996; Zhou et al., 2024). We will focus next on iso-recursive types.
line 159:
line 168: Recursive Subtyping for All
line 172: For example, consider the subtyping statement 𝜇𝛼.𝛼 → nat ≤ 𝜇𝛼.𝛼 →⊤. If we unfold the recursive types twice, we obtain:
line 175:
line 178: This statement requires both nat ≤⊤ (which is true) and ⊤≤ nat (which is false), thus correctly rejecting the subtyping statement. Unfolding once would not expose the invalid ⊤≤ nat comparison.
line 180: The nominal unfolding rules simulate this double-unfolding process by replacing recursive types with labeled types ( 𝐴[𝛼] ):
line 183:
line 189:
line 196: 2.2 Applications of Bounded Quantification and Recursive Types
line 212: 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 define some auxiliary functions:
line 224:
line 228: With subtyping, we can develop subtypes of Point, such as:
line 238: The type of this translate function is ∀(P ≤ Point) . P →Point, which is obtained from the following typing derivation (some parts omitted):
line 242: typing-unfold
line 248: Recursive Subtyping for All
line 254: ∀(P ≤ Point) . P → P
line 289:
line 295:
line 301:
line 307:
line 326: Recursive Subtyping for All
line 330: Method calls are encoded by unfoldings of iso-recursive types and unpacking of bounded existentials. For example, accessing the x field of a Point object can be implemented as:
line 332: function getXORBE(p: Point ORBE ) =
line 334: (unpack (unfold [Point ORBE ] p) as [ 𝛼 , o] in o.x[sel] (o.self) )
line 350: If we unfold the recursive type, this encoding is a polymorphic higher order function that takes a record with three fields (num, add and sub) as input. Each field corresponds to a
line 366:
line 378: Subtyping between datatypes. Now consider a larger datatype Exp2, which extends the Exp1 datatype with a new constructor Neg, for denoting negative numbers.
line 392: Recursive Subtyping for All
line 408:
line 416:
line 426: avoids the duplication at the cost of static typing guarantees. In 𝐹 ≤≥ [𝜇][∧][we do not need such] compromises: we can avoid code duplication and preserve the static typing guarantees.
line 428: 2.3 Key Ideas and Results
line 434: The more challenging aspect in the metatheory of 𝐹 ≤ [𝜇][lies in the] [ unfolding lemma][:]
line 437:
line 452: Recursive Subtyping for All
line 454: Structural folding and unfolding rules. In our work, instead of standard rules for fold/unfold expressions, we use structural rules :
line 457:
line 465:
line 475:
line 478: Records as intersection types. It is well known that multi-field records can be encoded using intersection types and single field records (Reynolds, 1988; Dunfield, 2012). In 𝐹 ≤≥ [𝜇][∧]
line 489:
line 497:
line 504: Recursive Subtyping for All
line 510: Fig. 1: Syntax of 𝐹 ≤ [𝜇][.]
line 512: 3 Bounded Quantification with Iso-Recursive Types
line 516: 3.1 Kernel 𝐹 ≤ with Iso-recursive Subtyping
line 518: Firstly, we introduce how to combine kernel bounded quantification, multi-field records and iso-recursive subtyping in kernel 𝐹 ≤ [𝜇][.]
line 524: Subtyping for kernel 𝐹 ≤ [𝜇] [.][The][bottom][of][Figure][2][shows][the][subtyping][judgement.][Our] subtyping rules are mostly standard. The rules essentially include the rules of the algorithmic
line 537:
line 544: Fig. 2: Well-formedness and subtyping rules for kernel 𝐹 ≤ [𝜇][.]
line 548: Lemma 3.1 (Regularity of subtyping) . If Γ ⊢ 𝐴 ≤ 𝐵 , then the following well-formedness conditions hold: (1) ⊢ Γ, (2) Γ ⊢ 𝐴 , and (3) Γ ⊢ 𝐵 .
line 552: Recursive Subtyping for All
line 558: ∀( 𝛼 ≤ 𝑥 : nat , 𝑦 : nat) .𝛼 → 𝛼 ≤∀( 𝛼 ≤ 𝑦 : nat , 𝑥 : nat) .𝛼 → 𝛼
line 566: Lemma 3.2 (Narrowing) . If Γ1 ⊢ 𝐶 ≤ 𝐶[′] and Γ1 , 𝛼 ≤ 𝐶[′] , Γ2 ⊢ 𝐴 ≤ 𝐵 then Γ1 , 𝛼 ≤ 𝐶, Γ2 ⊢ 𝐴 ≤ 𝐵 .
line 568: Theorem 3.3 (Reflexivity) . If ⊢ Γ and Γ ⊢ 𝐴 then Γ ⊢ 𝐴 ≤ 𝐴 .
line 570: Theorem 3.4 (Transitivity) . If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ 𝐵 ≤ 𝐶 then Γ ⊢ 𝐴 ≤ 𝐶 .
line 580: Lemma 3.5 (Unfolding Lemma) . If Γ ⊢ 𝜇𝛼. 𝐴 ≤ 𝜇𝛼. 𝐵 then Γ ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐵 ] 𝐵 .

Full converted paper text

JFP , 55 pages, 2022. © Cambridge University Press 2022 doi:10.1017/xxxxx

Recursive Subtyping for All

LITAO ZHOU1 YAODA ZHOU1 QIANYONG WAN BRUNO C. D. S. OLIVEIRA

The University of Hong Kong (e-mail: {ltzhou,ydzhou,qywan,bruno}@cs.hku.hk)

Abstract

Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability , transitivity of subtyping, conservativity and a sound and complete algorithmic formulation has been a long-time challenge.

This paper shows how to extend 𝐹 ≤ with iso-recursive types in a new calculus called 𝐹 ≤ [𝜇][.] [𝐹][≤] is a well-known polymorphic calculus with bounded quantification. In 𝐹 ≤ [𝜇][we][add][iso-recursive] types, and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. In addition we use so-called structural folding/unfolding rules for typing iso-recursive expressions, inspired by the structural unfolding rule proposed by Abadi, Cardelli, and Viswanathan (1996). 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; the conservativity of 𝐹 ≤ [𝜇][over] [𝐹][≤][;][and][a][sound][and] complete algorithmic formulation of 𝐹 ≤ [𝜇][. We study two variants of] [ 𝐹] ≤ [𝜇][. The first one uses an extension] of the kernel 𝐹 ≤ (a well-known decidable variant of 𝐹 ≤ ). This extension accepts equivalent rather than equal bounds and is shown to preserve decidable subtyping. The second variant employs the full 𝐹 ≤ rule for bounded quantification and has undecidable subtyping. Moreover, we also study an extension of the kernel version of 𝐹[𝜇][called] [𝐹][𝜇][∧][with][a][form][of][intersection][types][and] [lower] ≤[,] ≤≥[,] bounded quantification . All the properties from the kernel version of 𝐹 ≤ [𝜇][are preserved in] [𝐹] ≤≥ [𝜇][∧][. All] the results in this paper have been formalized in the Coq theorem prover.

1 Introduction

Recursive types and bounded quantification are two prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Bounded quantification was introduced by Cardelli and Wegner (1985) in the Fun language, and has been widely studied (Curien and Ghelli, 1992; Cardelli et al., 1994; Pierce, 1994). Bounded quantification 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 (OOP) languages to encode binary methods (Bruce et al., 1995). For adding recursive types to a language with subtyping, it is desirable to have recursive subtyping between recursive types. The first rules for recursive

1 BOTH AUTHORS CONTRIBUTED EQUALLY TO THIS WORK.

--- end of page.page_number=1 ---

Recursive Subtyping for All

subtyping, due to Cardelli (1985), are the well-known Amber rules. Recursive subtyping has been studied in two different forms: equi-recursive subtyping (Amadio and Cardelli, 1993; Brandt and Henglein, 1998; Gapeyev et al., 2003), and iso-recursive subtyping (Ligatti et al., 2017; Bengtson et al., 2011; Zhou et al., 2020, 2022). In equi-recursive subtyping, recursive types and their unfoldings are considered to be equal. In contrast, in iso-recursive subtyping they are only isomorphic, 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 type-theoretic foundations for OOP. Both recursive subtyping, as well as bounded quantification played a major part on this effort. The two features were perceived to be important to model objects in some forms of object encodings. At that time the key ideas around 𝐹 ≤ (Curien and Ghelli, 1992; Cardelli and Wegner, 1985; Cardelli et al., 1994), which is a polymorphic calculus with bounded quantification (but no recursive types), were reasonably well understood due to the early work on the Fun language by Cardelli and Wegner (1985). Therefore 𝐹 ≤-like calculi were being used in foundational work on OOP. Some landmark papers on the foundations of OOP, which established important results such as the distinction between inheritance and subtyping (Cook et al., 1989), F-bounded quantification (Canning et al., 1989), or encodings of objects (Cook et al., 1989; Abadi et al., 1996; Bruce et al., 1999), 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 first formalization of 𝐹 ≤ (Curien and Ghelli, 1992), Ghelli (1993) questioned this state-of-affairs, which implicitly assumed that the extension of 𝐹 ≤ with recursive types was straightforward. He conducted the first 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 addition of equi-recursive types allows well-formed, but invalid subtyping statements in 𝐹 ≤ to be valid in an extension with recursive types. Ghelli (1993) 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 reopened questions about the decidability or undecidability of the system.

Even if we choose the weaker form of bounded quantification present in the Fun language and kernel 𝐹 ≤, the natural extension of Amadio and Cardelli (1993)’s algorithm to kernel 𝐹 ≤ is incomplete (Colazzo and Ghelli, 2005). In kernel 𝐹 ≤, only universal quantifiers with equal bounds are allowed to be in a subtyping relation. This more restrictive formulation of bounded quantification is known to be decidable. However, complications still arise after adding equi-recursive types to kernel 𝐹 ≤. Instead of Amadio and Cardelli (1993)’s meet 2 times rules, Colazzo and Ghelli (2005) 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 not prove conservativity. Based on an earlier draft from Colazzo and Ghelli (2005), Jeffrey (2001) extended the system and proved it correct and

--- end of page.page_number=2 ---

Journal of Functional Programming

Table 1: Comparison among different works.

	Ghelli (1993) Colazzo and Ghelli(2005) Jefrey (2001) Abadi et al. (1996) This Work
Kernel/Full_𝐹_≤ Equi-/Iso-Recursive	full kernel full kernel full kernel full equi equi equi equi iso iso iso
Transitivity Decidability Conservativity Type System Algorithmic Typing Type Soundness Modularity Mechanized Proofs	× ✓ ✓ ✓ built-in ✓ ✓ ✓ ✓ ∖ ✓ ✓ × × × ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ × × × × ✓ ✓ × × × × × ✓ ✓

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

complete. By transferring the polar bisimulations (Sangiorgi and Milner, 1992) technique from concurrency theory, Jeffrey (2001)’s system is more general than Colazzo and Ghelli’s, but it is only partially decidable. It is decidable for kernel 𝐹 ≤ with equi-recursive types, but for full 𝐹 ≤ with equi-recursive types, only when the algorithm terminates it returns the correct answer, but it may not terminate. Furthermore, although being more powerful, Jeffrey (2001)’s full system is not conservative over full 𝐹 ≤ 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 the property was proved or not. Modularity here means whether the original rules and definitions of 𝐹 ≤ are the same or they need to be modified.

The proofs in all the 4 systems with equi-recursive types are complex because of the strong recursion, as can be seen from the literature. Adding equi-recursive subtyping requires major changes in existing definitions, rules and proofs compared to 𝐹 ≤, making most of the existing metatheory on 𝐹 ≤ not reusable. No prior work has proved the conservativity of kernel 𝐹 ≤ with equi-recursive 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.

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, reflexivity 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 of technical results is that the iso-recursive Amber rules are hard to work with

--- end of page.page_number=3 ---

Recursive Subtyping for All

formally (Ligatti et al., 2017; Backes et al., 2014; Zhou et al., 2020, 2022): it is difficult to prove results such as transitivity, or define sound and complete algorithmic formulations.

This paper shows how to extend 𝐹 ≤ with iso-recursive types in a calculus called 𝐹 ≤ [𝜇][. 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 the same expressive power as the well-known iso-recursive Amber rules (Cardelli, 1985). Moreover, the nominal unfolding rules address the difficulties of working formally with the (iso-recursive) Amber rules. With the nominal unfolding rules, proving transitivity and other properties is easy, also enabling 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 definitions and proofs. In other words they allow reusing most existing metatheory and definitions that existed before the addition of isorecursive types. Our work shows that the nominal unfolding rules proposed by Zhou et al. (2022) can be integrated modularly into 𝐹 ≤ subtyping rules, while retaining desirable properties. In particular, we prove, for the first time, the conservativity of an extension of 𝐹 ≤ with recursive types over the original 𝐹 ≤.

In 𝐹[𝜇] ≤[we use the so-called] [ structural][ folding/unfolding rules for typing expressions with] recursive types, inspired by the structural unfolding rule 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 in modeling encodings of objects, as well as encodings of algebraic datatypes with subtyping. We study two variants of 𝐹 ≤ [𝜇][.][The][first][one][has][a][generalization][of][the][kernel] [𝐹][≤][rule] for bounded quantification that accepts equivalent rather than equal bounds. The second variant uses the rule of full 𝐹 ≤ for bounded quantification. We will refer to the first variant as kernel 𝐹[𝜇] ≤[, and to the second variant as full] [ 𝐹] ≤ [𝜇][. We present several results, including:] [ type] soundness ; transitivity and (un)decidability of subtyping; the conservativity of 𝐹 ≤ [𝜇][over] [ 𝐹][≤][;] and a sound and complete algorithmic formulation of 𝐹 ≤ [𝜇][. The kernel] [ 𝐹] ≤ [𝜇][variant is proved to] have decidable subtyping, whereas the full 𝐹 ≤ [𝜇][variant has undecidable subtyping. We also] present an extension of 𝐹 ≤ [𝜇][, called] [𝐹] ≤≥ [𝜇][∧][, which has a bottom type, intersection types, and] lower bounded quantification in addition to the conventional (upper) bounded quantification of 𝐹 ≤. As we show, lower bounded quantification is useful to model the subtyping of algebraic datatypes. Intersection types are used to encode record types, similarly to how the Dependent Object Calculus (DOT) (Rompf and Amin, 2016) encodes object types. All the results in this paper have been formalized in the Coq theorem prover.

In summary the contributions of this paper are:

𝐹[𝜇] [extending] [𝐹][≤] [with][iso-recursive][types.][We][have][two][variants][of] [𝐹][𝜇][kernel] ≤ [:] ≤[:]
𝐹[𝜇][the][extension][of][kernel] [𝐹][≤][with][iso-recursive][subtyping,][and][full] [𝐹][𝜇][the] ≤[as] ≤[as]
extension of full 𝐹 ≤ with iso-recursive subtyping. We prove several properties for 𝐹[𝜇][including:][type][soundness;][transitivity][of][subtyping;][decidability][of][subtyping] ≤[,]
of kernel 𝐹[𝜇] ≤[; undecidability of subtyping of full] [ 𝐹] ≤ [𝜇][; and the unfolding lemma, a key]
property to ensure type soundness.

--- end of page.page_number=4 ---

Journal of Functional Programming

The conservativity of 𝐹 ≤ [𝜇] [over] [𝐹][≤] [.][Conservativity][is][an][expected][but][non-trivial] property that has eluded past work on the combination of bounded quantification and recursive types. We show that 𝐹 ≤ [𝜇][is conservative over] [ 𝐹][≤][.]
Type soundness for the structural folding/unfolding rules. We present the first 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 kernel 𝐹 ≤ [𝜇] [.][We][show][that][kernel] [𝐹] ≤ [𝜇][is][decidable.][The][measure] needed for decidability is non-trivial because there are significant differences in the measures for kernel 𝐹 ≤ and nominal unfoldings. We show how to develop a new measure that can account for both features at once. In addition, due to our generalization of the kernel rule to allow equivalent bounds, a key property for decidability is that equivalent types have equal sizes.
An extension of 𝐹[𝜇] ≤ [with intersection types, both upper and lower bounded quan-]
tification: We present an extended calculus, called 𝐹 ≤≥ [𝜇][∧][, with a form of intersection] types, both top and bottom types, and both upper and lower bounded quantification, 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, and made the formalization available online at https://github.com/juda/ Recursive-Subtyping-for-All/tree/main/JFP .

Differences to conference version. This article is a substantial enhancement of the conference paper (Zhou et al., 2023). It introduces three major improvements over the original conference paper. The first improvement is the extension of our results to the full 𝐹 ≤ [𝜇][calcu-] lus, along with proofs demonstrating its type soundness and its conservativity over 𝐹 ≤. The initial conference version only addressed the addition of iso-recursive types into kernel 𝐹 ≤ and left the extension to the full variant as an unresolved issue. The second improvement is a further generalization of the unfolding lemma that is capable of dealing with full 𝐹 ≤, intersection types and all the other extensions in this paper. The unfolding lemma is a central lemma in the metatheory of iso-recursive subtyping, and it is also where the main challenge in the metatheory lies. In the conference version, the generalized unfolding lemma was not able to deal with full 𝐹 ≤. Our new generalization addresses this issue, and it is shown to be general and applicable to a variety of extensions. The final improvement involves the combination of several important features within the system 𝐹 ≤≥ [𝜇][∧][, and a much more detailed] overview of 𝐹[𝜇][∧] ≤≥[. Unlike the conference version, which did not include intersection types,] the updated 𝐹 ≤≥ [𝜇][∧][can][model][objects][using][structural][folding/unfolding][rules,][intersection] types and single-field record types. This alternative way to model objects is inspired by, and aligns closely with, the encoding of objects in the DOT calculus.

2 Overview

This section provides an overview of our work. We first briefly review basic concepts and some applications. Then we show our key ideas and results.

--- end of page.page_number=5 ---

Recursive Subtyping for All

2.1 Bounded Quantification and Recursive Subtyping

Bounded Quantification. Bounded quantification allows types to be abstracted by type variables with a subtyping constraint (or bound). The standard calculus with bounded quantification, 𝐹 ≤ (Cardelli and Wegner, 1985; Curien and Ghelli, 1992; Cardelli et al., 1994), has two common variants when it comes to subtyping universal types. The full 𝐹 ≤ variant (Curien and Ghelli, 1992; Cardelli et al., 1994) compares bounded quantifiers with the following rule:

The most significant characteristic of full 𝐹 ≤ is that it allows two bounded quantifiers to be contravariant on their bound types 𝐴 1 and 𝐴 2 when being compared. However, the rich expressive power of full 𝐹 ≤ results in an undecidable subtyping relation (Pierce, 1994), which is undesirable. In addition, as Ghelli (1993) demonstrates, the rule S-fullall may even prevent conservative extensions of 𝐹 ≤ in the presence of additional features.

There are several ways to restrict bounded quantification 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 quantifiers can only be subtypes when their bound types are identical (Cardelli and Wegner, 1985), which is stated in the rule S-

kernelall.

In our paper, we will show how iso-recursive subtyping can be integrated with both kernel and full variants of 𝐹 ≤. However, for the kernel variant, differently from kernel 𝐹 ≤, we will generalize the rule S-kernelall to a rule S-equivall that accepts equivalent bounds instead. The main motivation for using rule S-equivall 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 to consider types such as { 𝑥 : nat , 𝑦 : nat} and { 𝑦 : nat , 𝑥 : nat}, to be equivalent (despite being syntactically different). 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-equivall is more general than the kernel rule with identical bounds, but retains decidability, as we shall see in §4.3.

Recursive Types. Recursive types 𝜇𝛼. 𝐴 , can be traced back to Morris (1968). There are two basic approaches to recursive types: equi-recursive types and iso-recursive types . The essential difference between them is how they consider the relationship between a recursive type 𝜇𝛼. 𝐴 and its unfolding [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] 𝐴 . In equi-recursive types, a recursive type is equal to its unfolding. That is 𝜇𝛼. 𝐴 = [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] 𝐴 . In other words, recursive types and their unfoldings are interchangeable in all contexts. Equi-recursive types also allow for more general equalities than unfoldings. For example, the types 𝜇𝛼. int → 𝛼 and

--- end of page.page_number=6 ---

Journal of Functional Programming

𝜇𝛼. int → int → 𝛼 are considered equivalent in the equi-recursive setting, since they have the same infinite unfolding (Amadio and Cardelli, 1993).

In iso-recursive types, a recursive type and its one-step unfolding are not equal but only isomorphic. To convert between 𝜇𝛼. 𝐴 and [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] 𝐴 we need explicit unfold and fold operators. A fold expression constructs a recursive type, while an unfold expression opens a recursive type, as rule typing-fold and rule typing-unfold illustrate:

Despite being less convenient, iso-recursive types are known to have the same expressive power as equi-recursive types (Abadi and Fiore, 1996; Zhou et al., 2024). We will focus next on iso-recursive types.

Recursive Subtyping. Subtyping between recursive types has been studied for many years (Cardelli, 1985; Amadio and Cardelli, 1993; Ligatti et al., 2017). The most widely used subtyping rules for recursive types are the Amber rules, first introduced in 1985 by Cardelli (1985) in a manuscript describing the Amber language (Cardelli, 1985). The iso-recursive Amber rules deal with recursive subtyping with three rules: rule S-amber, rule S-assmp and rule S-refl.

The Amber rules are simple, but their metatheory is troublesome. For example, transitivity is hard to prove (Bengtson et al., 2011; Zhou et al., 2020, 2022). Furthermore, due to the reliance on the reflexivity rule (rule S-refl), the Amber rules are problematic for subtyping relations that are not antisymmetric (Ligatti et al., 2017). Recently, Zhou et al. (2020, 2022) proposed a new specification for iso-recursive subtyping and some equivalent algorithmic variants (Zhou and Oliveira, 2025). For this paper we use one of those algorithmic variants, called the nominal unfolding rules (Zhou et al., 2022). The main reason to choose the nominal unfolding rules is that they are easy to work with formally: indeed, Zhou et al. (2022) have a full Coq development, including proofs of decidability, that we will reuse and extend.

Nominal Unfolding Rules. The nominal unfolding rules provide a formal mechanism for handling iso-recursive subtyping. These rules are designed to address the challenges posed by contravariant occurrences of recursive type variables. For recursive types it is expected that if two recursive types 𝜇𝛼. 𝐴 and 𝜇𝛼. 𝐵 are subtypes, then their unfolding [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] 𝐴 and [ 𝛼 ↦→ 𝜇𝛼. 𝐵 ] 𝐵 should also be subtypes. This property can be tricky to achieve with contravariant occurrences of recursive variables. The Amber rules deal with this issue by remembering pairs of recursive variables as subtyping assumptions, as can be seen in rule S-amber. In contrast, the nominal unfolding rules unfold the recursive body twice to ensure the correctness of the subtyping relation.

--- end of page.page_number=7 ---

Recursive Subtyping for All

For example, consider the subtyping statement 𝜇𝛼.𝛼 → nat ≤ 𝜇𝛼.𝛼 →⊤. If we unfold the recursive types twice, we obtain:

This statement requires both nat ≤⊤ (which is true) and ⊤≤ nat (which is false), thus correctly rejecting the subtyping statement. Unfolding once would not expose the invalid ⊤≤ nat comparison.

The nominal unfolding rules simulate this double-unfolding process by replacing recursive types with labeled types ( 𝐴[𝛼] ):

In rule S-nominal, every time two recursive types are compared, a fresh label 𝛼 is used to label to the unfolded parts. Labeled types can only be compared to other labeled types with the same label, which ensures that they arise from the same recursive type, as shown in rule S-label. The bound type variable 𝛼 in the recursive body becomes free variable after unfolding1. For instance, to compare 𝜇𝛼.𝛼 → nat and 𝜇𝛼.𝛼 →⊤, the subtyping statement becomes:

The one-time unfolding is captured by the labels, since if we ignore the body of the labeled types, 𝛼 → nat and 𝛼 →⊤ are compared. On the other hand, when ignoring the labels, the double unfolding statement is obtained, which exposes the invalid ⊤≤ nat comparison. The key design in the nominal unfolding rules is to use label as a syntactic device to ensure that recursive types are compared correctly. Without labels providing distinct identities to recursive types, unsound subtyping statements such as 𝜇𝛼. nat → 𝛼 ≤ 𝜇𝛼. nat → nat →⊤, which unfolds to nat → nat → 𝛼 ≤ nat → nat →⊤, may be accepted.

The nominal unfolding rules are formally proven to be type sound and have the same expressive power as the iso-recursive Amber rules (Zhou et al., 2022). They are also easier to work with formally, enabling the development of sound and complete algorithmic formulations of subtyping. Additionally, these rules are modular, allowing the extension of existing calculi with iso-recursive types without significant changes to existing definitions and proofs.

2.2 Applications of Bounded Quantification and Recursive Types

We now turn to applications of bounded quantification and recursive types. In particular the classic application for both features is encodings of objects (Bruce et al., 1999). In addition, we also show that the two features are useful to model encodings of algebraic datatypes with subtyping.

1 In our Coq formalization we use a locally nameless representation (Aydemir et al., 2008), which distinguishes free and bound variables naturally. With a locally nameless representation we can reuse the free variable name 𝛼 for the fresh label 𝛼 . In the paper we use the named representation for better readability, so type variables 𝛼 and label variables 𝛼 are distinguished by color. In a black-and-white printout, these label variables can be identified by noting that they only occur as superscripts in labeled types 𝐴[𝛼] .

--- end of page.page_number=8 ---

Journal of Functional Programming

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 records2. For example, we can define 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 define some auxiliary functions:

function getX(p : Point) = (unfold [Point] p ). x function getY(p : Point) = (unfold [Point] p ). y function moveTo(p : Point, x : Int , y : Int ) = (unfold [Point] p ). move x y

then a constructor mkPoint can be defined 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 language with iso-recursive subtyping, the fold’s and unfold’s do not need to be explicitly written and are automatically inserted by the compiler. For instance, this is what Abadi et al. (1996)’s translation of a 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, suppose we wish to translate the coordinates by one unit for a point, but we do not want to write such a translation function for each subclass of Point. As a first attempt, 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 ∀(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 typing-sub P ≤ Point , p : P ⊢ p : Point x : Int , y : Int , P ≤ Point , p : P ⊢(unfold [Point] p) : � move : Int → Int → Point � … ⊢ translate : ∀(P ≤ Point) . P → Point

typing-unfold

2 We will use a simplified form of the encoding that does not deal with self-references, which allows programmers to refer to the object itself in method implementations using the self parameter. But self-references could be dealt with in standard ways (Canning et al., 1989).

--- end of page.page_number=9 ---

Recursive Subtyping for All

However, this type is unsatisfying because it loses precision: it returns a Point instead of a P. The type that we want instead is:

∀(P ≤ Point) . P → P

Unfortunately, we cannot obtain this more general type with only bounded quantification and the usual unfolding rule typing-unfold. In the rule typing-unfold, the unfold annotation must be a recursive 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 quantification (Canning et al., 1989; Baldan et al., 1999), address this issue. In F-bounded quantification, the bounded variables are allowed to appear in the bound, and universal types take the form ∀( 𝛼 ≤ 𝐹 [ 𝛼 ]) . 𝐵 , where 𝐹 is a type-level function applied to the bound variable 𝛼 . For the example above, the bound in the translate function is no longer the closed recursive type Point but would have the form 𝐹 [ 𝛼 ] = { 𝑥 : Int , 𝑦 : Int , move : Int → Int → 𝛼 }. Therefore, with F-bounded quantification the translate function could have the type:

∀( 𝛼 ≤{ 𝑥 : Int , 𝑦 : Int , move : Int → Int → 𝛼 }) .𝛼 → 𝛼

Then the 𝛼 can be instantiated to Point or subtypes of Point, since Point ≤ 𝐹 [Point]. Note that to satisfy the F-bounded constraints 𝛼 ≤ 𝐹 [ 𝛼 ], the subtyping statements must be interpreted in an equi-recursive setting. 𝐹 ≤ [𝜇][uses][a][less][intrusive][approach][to][achieve] the same effect for typing the translate function, without requiring recursive bounds or equi-recursive types. This is achieved by using the structural unfolding rule (Abadi et al., 1996), which we will discuss in §2.3.

Encoding positive F-bounded quantification. Fortunately, with the structural rules, we can use a type variable as an annotation for unfold. This enables us to encode forms of F-bounded quantification 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)

In §2.3, we will discuss the typing of this program via the structural unfolding rule in detail. After this change the type of translate is ∀(P ≤ Point) . P → P. Then we can apply translate to Point or any of its subtypes, without losing static precision. Thus, if we call translate [EqPoint] (mkEqPoint 0 0), then we obtain an EqPoint object at (1 , 1). Here mkEqPoint is a constructor for objects 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)

}

--- end of page.page_number=10 ---

Journal of Functional Programming

Encoding objects with bounded existentials. Recursive types are not the only way to encode objects. Another common encoding is to use bounded existentials (Cardelli and Wegner, 1985). Existential types can be used to encode objects (Pierce and Turner, 1994), or they can be employed together with recursive types (Bruce, 1994). Since the intentional behavior of existential types can be encoded by universal types, we can obtain a form of bounded existentials for free in 𝐹 ≤ (Cardelli and Wegner, 1985):

Abadi et al. (1996) presented an encoding of objects using a combination of recursive types and bounded existential quantification, called the ORBE encoding. In their work, an interface 𝐼 ( 𝛼 ) is defined as a record of type-level functions, each having a self variable 𝛼 argument ({ 𝑙𝑖 : 𝐼𝑖 ( 𝛼 ) [𝑖][∈][1] […𝑛] }). For example, the interface for the Point object is:

The general ORBE encoding for an interface 𝐼 ( 𝛼 ) is:

The bounded existential quantification (∃( 𝛽 ≤ 𝛼 )) is used to indicate that the true type of an object can be a subtype of the object type 𝛼 . Intuitively, it allows the object implementation to contain more fields, such as private variables, than the interface specifies. The field self is the object itself with all its methods including private ones so that the listed methods can access the object’s private fields. Through fields 𝑙𝑖[sel][,][users][of][the][object][can][access] the object’s public methods. The fields 𝑙𝑖[upd] are optional in the encoding. They allow users to update method 𝑙𝑖 by taking a new function of self and returning a new object with the updated method, which is a feature not supported in many other object encodings. For example, the Point object from above can be encoded with the ORBE encoding as follows:

We can implement the Point object with the ORBE encoding as follows:

function mkPointORBE(x1: Int, y1: Int) = fold [Point ORBE ] (

pack [Point ORBE , {

self = mkPointORBE(x1, y1),

x[sel] = 𝜆 (self’: Point ORBE ). x1,

y[sel] = 𝜆 (self’: Point ORBE ). y1, move[sel] = 𝜆 (self’: Point ORBE ) x2 y2. mkPointORBE(x1 + x2, y1 + y2),

… } ] as ∃( 𝛽 ≤ Point ORBE ) . { … })

--- end of page.page_number=11 ---

Recursive Subtyping for All

Method calls are encoded by unfoldings of iso-recursive types and unpacking of bounded existentials. For example, accessing the x field of a Point object can be implemented as:

function getXORBE(p: Point ORBE ) =

(unpack (unfold [Point ORBE ] p) as [ 𝛼 , o] in o.x[sel] (o.self) )

We omit the encodings for the method update fields in the mkPointORBE function for brevity, but they can also be written using 𝐹 ≤ [𝜇][.][More][details][about][the][encoding][can][be] found in the original work (Abadi et al., 1996). As we can see, the ORBE encoding requires both recursive types and bounded existentials. By rewriting all bounded existentials into universal quantification using (2.1), we are able to write all the programs and types in the ORBE encoding presented above in our 𝐹 ≤ [𝜇][calculus.][Therefore,] [𝐹] ≤ [𝜇][can][serve][as][a][target] language for the ORBE encoding.

When it comes to subtyping, as Bruce et al. (1999) observe, the ORBE encoding requires full 𝐹 ≤ for the bounded quantification subtyping rule. Consider the encoding for the object ColorPoint, which has more fields than Point. ColorPoint ORBE should extend the record in Point ORBE with color[sel] and color[upd] fields. When we try to compare the two encodings, we see that the bounds in ( 𝛽 ≤ pnt) for the two types are not the same – the recursive variable pnt in ColorPoint ORBE stands for more fields than in Point ORBE . As a result, contravariant subtyping is needed for comparing the bound in the existential type, which in turn requires full 𝐹 ≤ instead of kernel 𝐹 ≤. Therefore, we also study the full 𝐹 ≤ [𝜇][calculus in this paper, in] order to support subtyping between objects in the ORBE encoding.

Encodings of Algebraic Datatypes with Subtyping. It is well-known that, in the polymorphic lambda calculus (System F) (Reynolds, 1974), we can use Church (1932) encodings to encode algebraic datatypes (B¨ohm and Berarducci, 1985). However, Church encodings make it hard to encode some operations, or worse they prevent encoding certain operations with the correct time complexity. 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 that captures intentional behavior of datatypes in the untyped lambda calculus and avoids the issues of Church encodings, is due to Scott (1962). Unfortunately, Scott encodings cannot be encoded in plain System F. The addition of recursive types to a polymorphic lambda calculus allows a typed Scott encoding (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 with recursive 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][define][a][datatype][Exp] 1[for] mathematical expressions, with constant, addition, and subtraction constructors:

data Exp1 = Num Int | Add Exp1 Exp1 | Sub Exp1 Exp1

The encoding in 𝐹 ≤ [𝜇][of this datatype can be defined as follows:]

Exp1 ≜ 𝜇 E . ∀A . {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 a record with three fields (num, add and sub) as input. Each field corresponds to a

--- end of page.page_number=12 ---

Journal of Functional Programming

constructor in the datatype definition. 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 then provide a record that maps each case to an implementation function that takes the constructor components as input and returns a result of type A. For example, given an expression e with type Exp1, 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 field implements a function that returns the integer n of the Num constructor directly, while the functions in add and sub fields perform the evaluation process recursively. To construct concrete instances of 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 typing-fold, 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 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 . ∀A . {num : Int → A , add : E → E → A , sub : E → E → A , neg : E → A} → A

The datatype Exp2 differs from Exp1 only in the new constructor: the other constructors are just the same. To reduce code duplication, it is desired that the constructor functions such as Add1 can be polymorphic and used for both datatypes. 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 𝐹 ≤ [𝜇][encoding for the][ Add][ constructor to have] the following type, so that both encodings of Exp1 and Exp2 can use this constructor function:

Add∀ : ∀(E ≥ Exp1) . E → E → E

There are two problems here. Firstly, similarly to the issue that we have faced in the translate function, we would like to use a type variable in the fold’s of the constructors. This way

--- end of page.page_number=13 ---

Recursive Subtyping for All

we can make the constructors polymorphic. Secondly, as evidenced by the desired type for Add, we need lower bounded quantification , but in 𝐹 ≤ [𝜇][(and] [𝐹][≤][)][we][only][have][upper] bounded quantification.

Polymorphic constructors with lower bounded quantification. For applications such as encodings of algebraic datatypes, the dual form of bounded quantification (lower bounded quantification) seems to be more useful. Thus we have an extended system, called 𝐹 ≤≥ [𝜇][∧][, that] also supports lower bounded quantification. Polymorphic datatype constructors become typeable with the structural folding rule. For example, we can encode the polymorphic Add constructor as:

function Add∀ [E ≥ Exp1] (e1 : E, e2 : E) = fold [E] (Λ A. 𝜆 e. (e.add e1 e2)) Other polymorphic constructors such as Num∀ and Sub∀ 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 define a pretty printer function for Exp2

function print ( 𝑒 : Exp2) = (unfold [Exp2] 𝑒 ) [string] {

num = 𝜆 n. ( int t o s tring 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 defined in the above function.

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 case analysis on Exp2 and use only the constructors in Exp1 to produce the result, i.e. it should have a type Exp2 → Exp1. The following code, with polymorphic constructors, has the desired typing:

function desugar ( 𝑒 : Exp2) = (unfold [Exp2] 𝑒 ) [Exp1] { num = 𝜆 n. Num∀ [Exp1] n, add = 𝜆 e1 e2. Add∀ [Exp1] (desugar e1) (desugar e2), sub = 𝜆 e1 e2. Sub∀ [Exp1] (desugar e1) (desugar e2), neg = 𝜆 e. Sub∀ [Exp1] (Num∀ [Exp1] 0) (desugar e)

}

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 define both Exp1 and Exp2 and also 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 different, and many operations, such as pretty printing, need to be essentially duplicated. In 𝐹 ≤≥ [𝜇][∧][, in] addition to polymorphic constructors, we would just need to define the pretty printer for Exp2, and that function would also work for Exp1. Alternatively, in a typical functional language one could define 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

--- end of page.page_number=14 ---

Journal of Functional Programming

avoids the duplication at the cost of static typing guarantees. In 𝐹 ≤≥ [𝜇][∧][we do not need such] compromises: 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 quantification and recursive types are fully satisfactory in all dimensions. In particular, equi-recursive types are problematic, since they can change the expressive power of the subtyping relation in unexpected ways. More importantly, adding equi-recursive subtyping to 𝐹 ≤ requires novel algorithms, and the extension is non-modular, requiring several changes to existing definitions 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 effect on the original 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][:]

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 is insufficient, due to bounded quantification. Therefore, an even 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 different measures. A natural combination is problematic, thus we need a new approach.

After overcoming those challenges, we show that kernel 𝐹 ≤ [𝜇][is][transitive,][decidable,] conservative and modular. Furthermore, there is a simple, sound and complete algorithmic type system to enable implementations and to provide important help in the proofs of results such as conservativity of typing.

Full 𝐹 ≤ with iso-recursive types. We have also integrated full 𝐹 ≤ with iso-recursive subtyping. The most significant challenge compared to the kernel variant is proving the unfolding lemma. As we will discuss in §4.3, the method used to prove the generalized unfolding lemma for the kernel variant does not apply to the full variant due to the contravariance of the bounds. Therefore, a yet more sophisticated adaptation of the generalized unfolding lemma is required. Additionally, we establish several other properties for full 𝐹 ≤ [𝜇][,] such as type soundness, conservativity, and undecidability.

--- end of page.page_number=15 ---

Recursive Subtyping for All

Structural folding and unfolding rules. In our work, instead of standard rules for fold/unfold expressions, we use structural rules :

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. This is forbidden in the traditional rules. In the rule typing-sunfold, it is worthwhile to mention that when we have 𝐴 ≤ 𝜇𝛼. 𝐵 where 𝛼 appears negatively in 𝐵 , then there are very limited choices to what 𝐴 can be. Essentially it can be 𝜇𝛼. 𝐵 itself and little else. In other words, negative recursive types have very restricted subtyping, which is why the structural unfolding rule can be type safe. Note also that, since the structural unfolding rules provide almost no flexibility for negative recursive subtyping, they are insufficient to fully express F-bounded quantification 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 unfold and fold expressions, together with the formalization of the type soundness for both rules. With the structural unfolding rule we can, for instance, obtain the desired typing for the translate function.

Readers can compare this derivation to the one in §2.2, where the conventional unfolding rule and the subsumption rule are used instead. The use of rule typing-sunfold enables us to give a more precise type for the translate function.

Lower bounded quantification and 𝐹 ≤≥ [𝜇][∧] [.][We have also formalized an extension of] [ 𝐹] ≤ [𝜇][with] both upper and lowerboundedquantification,called 𝐹 ≤≥ [𝜇][∧][. Allthesameresults thatareproved] for 𝐹[𝜇] ≤[are also proved for] [ 𝐹] ≤≥ [𝜇][∧][, including transitivity, decidability and type soundness. The] structural folding rules become more useful in 𝐹 ≤≥ [𝜇][∧][.][With][lower][bounded][quantification] and the structural folding rules we can get the correct typing for the polymorphic Add constructor:

· · ·

Records as intersection types. It is well known that multi-field records can be encoded using intersection types and single field records (Reynolds, 1988; Dunfield, 2012). In 𝐹 ≤≥ [𝜇][∧]

--- end of page.page_number=16 ---

Journal of Functional Programming

we follow this alternative approach to type record expressions. The record type {x : nat , y : nat} in 𝐹 ≤ [𝜇][is now simply syntactic sugar in] [ 𝐹] ≤≥ [𝜇][∧][for the intersection type][ {][x][ :][ nat][}][&][{][y][ :][ nat][}][.] To avoid records with duplicate labels being intersected, we restrict the labels in the intersection types to be disjoint. For instance, { 𝑥 : nat} & { 𝑥 : nat → nat} is not a valid type in 𝐹[𝜇][∧] ≤≥[. We will further discuss such design choice in][ §][5][. The combination of unrestricted] intersection types and iso-recursive subtyping was studied in Zhou et al. (2022). Our work models a restricted form of intersection types. In 𝐹 ≤≥ [𝜇][∧][,][only][types][that][are][formed][by] intersecting single-field record types are considered, and the disjointness relation discussed in Zhou et al. (2022) is in turn simplified to a compatibility relation for checking wellformedness of intersection types. The intersection type operator & is commutative and associative in terms of type equivalence, so that record permutations are obtained for free. The typing rules for record expressions and projections in 𝐹 ≤≥ [𝜇][∧][are shown below:]

With intersection types, record expressions are now typed using rule typing-srcd. As a result, we no longer need a dedicated rule for subtyping multi-field record types, which has a complicated definition since it needs to decide the subset inclusion of record fields and check the subtyping relation for common fields. Instead, we can now rely on the subtyping relation for intersection types and a direct subtyping rule for subtyping types in singlefield records. Moreover, record projections can be defined in terms of subtyping now, as rule typing-sproj shows. When projecting a field from a record expression 𝑒 , we can simply check if the record type of 𝑒 is a subtype of the expected record type.

The treatment of records in 𝐹[𝜇][∧] ≤≥[aligns closely with the way Dependent Object Calculus] (DOT) (Rompf and Amin, 2016) deals with object types. Rule typing-dot-object shows the typing rule for object expressions in DOT. In DOT object expressions are a record with a self reference variable 𝑥 bounded to the object itself, containing a list of labeled declarations 𝑑 1 … 𝑑𝑛 . When type checking objects, each declaration is checked on its own, and the intersection of all the declaration types forms the type of the object.

𝐹[𝜇][∧][DOT][share][the][same][idea][of][using][intersection][types][to][type][record][expressions] ≤≥[and] or objects and both require the labels to be disjoint. Due to the use of path-dependent types (Amin et al., 2014) in DOT, the treatment of recursive types is different. In 𝐹 ≤≥ [𝜇][∧][we] do not have a self reference variable in record expressions or types, and 𝐹 ≤≥ [𝜇][∧][lacks of some] DOT features. On the other hand 𝐹[𝜇][∧] ≤≥[has key properties, such as decidability, transitivity] of subtyping, and being a conservative extension of 𝐹 ≤, which are partly missing in DOT. Despite these differences, we hope that 𝐹 ≤≥ [𝜇][∧][can provide insights into the design of DOT-] like calculi with bounded quantification and recursive types and complement the existing work in terms of the design space.

--- end of page.page_number=17 ---

Recursive Subtyping for All

Types 𝐴, 𝐵, … � nat | ⊤| 𝐴 1 → 𝐴 2 | 𝛼 | 𝜇𝛼. 𝐴 | 𝐴[𝛼] | ∀( 𝛼 ≤ 𝐴 ) . 𝐵 | { 𝑙𝑖 : 𝐴𝑖[𝑖][∈][1][···] [𝑛] } Expressions 𝑒 � 𝑥 | i | 𝑒 1 𝑒 2 | 𝜆𝑥 : 𝐴. 𝑒 | 𝑒𝐴 | Λ( 𝛼 ≤ 𝐴 ) . 𝑒 | unfold [ 𝐴 ] 𝑒 | fold [ 𝐴 ] 𝑒 | { 𝑙𝑖 = 𝑒𝑖[𝑖][∈][1][···] [𝑛] } | 𝑒.𝑙 Values 𝑣 � i | 𝜆𝑥 : 𝐴. 𝑒 | fold [ 𝐴 ] 𝑣 | Λ( 𝛼 ≤ 𝐴 ) . 𝑒 | { 𝑙𝑖 = 𝑣𝑖[𝑖][∈][1][···] [𝑛] } Contexts Γ � · | Γ , 𝛼 ≤ 𝐴 | Γ , 𝑥 : 𝐴

Fig. 1: Syntax of 𝐹 ≤ [𝜇][.]

3 Bounded Quantification with Iso-Recursive Types

This section introduces a new calculus, called 𝐹 ≤ [𝜇][,][integrating][bounded][quantification,] record types and recursive types. We show two variants of 𝐹 ≤ [𝜇][.][One][is][kernel] [𝐹] ≤ [𝜇][,][by] adopting the kernel rule for subtyping bounded quantification from kernel 𝐹 ≤ (Cardelli and Wegner, 1985). The other one is full 𝐹 ≤ [𝜇][, which instead adopts the full rule for subtyping] bounded quantification from full 𝐹 ≤ (Curien and Ghelli, 1992; Cardelli et al., 1994).

3.1 Kernel 𝐹 ≤ with Iso-recursive Subtyping

Firstly, we introduce how to combine kernel bounded quantification, multi-field records and iso-recursive subtyping in kernel 𝐹 ≤ [𝜇][.]

Syntax and Well-Formedness. The syntax of types and contexts for 𝐹 ≤ [𝜇][is][shown][in] Figure 1. Meta-variables 𝐴, 𝐵, 𝐶, 𝐷 range over types. Types consist of natural numbers (nat), the top type (⊤), function types ( 𝐴 → 𝐵 ), type variables ( 𝛼 ), recursive types ( 𝜇𝛼. 𝐴 ), labeled types ( 𝐴[𝛼] ), universal types (∀( 𝛼 ≤ 𝐴 ) . 𝐵 ), and record types ({ 𝑙𝑖 : 𝐴𝑖[𝑖][∈][1][···] [𝑛] }). Labeled types are types that are annotated with a label. They enable distinguishing between otherwise structurally compatible types (equal types or subtypes). That is if the two types being compared have different labels or one of the types is unlabeled, then the two types will not be related, even when, ignoring the labels, they would be structurally compatible. Expressions, denoted by the meta-variable 𝑒 , include term variables ( 𝑥 ), natural numbers (i), applications ( 𝑒 1 𝑒 2), abstractions ( 𝜆𝑥 : 𝐴. 𝑒 ), type applications ( 𝑒𝐴 ), type abstractions (Λ( 𝛼 ≤ 𝐴 ) . 𝑒 ), fold expressions (fold [ 𝐴 ] 𝑒 ), unfold expressions (unfold [ 𝐴 ] 𝑒 ), records ({ 𝑙𝑖 = 𝑒𝑖[𝑖][∈][1][···] [𝑛] }), and record selection ( 𝑒.𝑙 ). Among them, natural numbers, abstractions and type 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 not necessary to distinguish recursive variables and universal variables.

The definition of a well-formed environment ⊢ Γ is standard, ensuring that all variables in the environment 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 at the top of Figure 2.

Subtyping for kernel 𝐹 ≤ [𝜇] [.][The][bottom][of][Figure][2][shows][the][subtyping][judgement.][Our] subtyping rules are mostly standard. The rules essentially include the rules of the algorithmic

--- end of page.page_number=18 ---

Journal of Functional Programming

Γ ⊢ 𝐴

(Well-formed Type)

----- Start of picture text -----
wft-var wft-all
wft-nat wft-Top
𝛼 ≤ A ∈ Γ Γ ⊢ A Γ , 𝛼 ≤ A ⊢ B
Γ ⊢ nat Γ ⊢⊤ Γ ⊢ 𝛼 Γ ⊢∀( 𝛼 ≤ A ) . B
wft-arrow wft-rec wft-label wft-rcd
Γ ⊢ A 1 Γ ⊢ A 2 Γ , 𝛼 ≤⊤⊢ A Γ ⊢ A Γ ⊢ A𝑖 for each 𝑖
Γ ⊢ A 1 → A 2 Γ ⊢ 𝜇𝛼. A Γ ⊢ A [𝛼] Γ ⊢{ 𝑙𝑖 : A𝑖 [𝑖] [∈][1][···] [𝑛] }
Γ ⊢ 𝐴 ≤ 𝐵 (Subtyping)
S-nat S-top S-var S-arrow
⊢ Γ ⊢ Γ Γ ⊢ A ⊢ Γ Γ ⊢ 𝛼 Γ ⊢ B 1 ≤ A 1 Γ ⊢ A 2 ≤ B 2
Γ ⊢ nat ≤ nat Γ ⊢ A ≤⊤ Γ ⊢ 𝛼 ≤ 𝛼 Γ ⊢ A 1 → A 2 ≤ B 1 → B 2
S-rec S-vartrans
Γ , 𝛼 ≤⊤⊢[ 𝛼 ↦→ A [𝛼] ] A ≤[ 𝛼 ↦→ B [𝛼] ] B 𝛼 ≤ B ∈ Γ Γ ⊢ B ≤ A
Γ ⊢ 𝜇𝛼. A ≤ 𝜇𝛼. B Γ ⊢ 𝛼 ≤ A
S-equivall S-label
Γ ⊢ A 1 ≤ A 2 Γ ⊢ A 2 ≤ A 1 Γ , 𝛼 ≤ A 2 ⊢ B ≤ C Γ ⊢ A ≤ B
Γ ⊢∀( 𝛼 ≤ A 1) . B ≤∀( 𝛼 ≤ A 2) . C Γ ⊢ A [𝛼] ≤ B [𝛼]
S-rcd
⊢ Γ Γ ⊢{ 𝑘 𝑗 : A 𝑗 [𝑗] [∈][1][···] [𝑚] } { 𝑙𝑖 [𝑖] [∈][1][···] [𝑛] } ⊆{ 𝑘 𝑗 [𝑗] [∈][1][···] [𝑚] } 𝑘 𝑗 = 𝑙𝑖 implies Γ ⊢ A 𝑗 ≤ B𝑖
Γ ⊢{ 𝑘 𝑗 : A 𝑗 [𝑗] [∈][1][···] [𝑚] } ≤{ 𝑙𝑖 : B𝑖 [𝑖] [∈][1][···] [𝑛] }
----- End of picture text -----

Fig. 2: Well-formedness and subtyping rules for kernel 𝐹 ≤ [𝜇][.]

version of kernel 𝐹 ≤ (Cardelli and Wegner, 1985; Cardelli et al., 1994), but the rule for bounded quantification is generalized. The rules S-var and S-vartrans are standard 𝐹 ≤ rules. Since we do not distinguish universal and recursive variables, those rules apply also to recursive type variables. The rule for function types (rule S-arrow) is contravariant on the input types and covariant on the output types. We have placed well-formedness checks on all the base cases of the subtyping rules, which ensures that the context and types in a subtyping relation are well-formed, as shown in Lemma 3.1. Note that for this regularity property to hold, in rule S-rcd we requires the left record type to be well-formed but not the right one, since the well-formedness of the right type can be derived from the subtyping relation on record fields, while there might be extra fields in the left record type that are not compared in the subtyping relation.

Lemma 3.1 (Regularity of subtyping) . If Γ ⊢ 𝐴 ≤ 𝐵 , then the following well-formedness conditions hold: (1) ⊢ Γ, (2) Γ ⊢ 𝐴 , and (3) Γ ⊢ 𝐵 .

--- end of page.page_number=19 ---

Recursive Subtyping for All

Subtyping bounded quantification. The rule for bounded quantification 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. Rule S-equivall is more general than rule S-kernelall since the latter requires the bounds to be equal. The reason to have the more general rule using equivalent bounds is that, for records, we wish to accept subtyping statements such as:

∀( 𝛼 ≤{ 𝑥 : nat , 𝑦 : nat}) .𝛼 → 𝛼 ≤∀( 𝛼 ≤{ 𝑦 : nat , 𝑥 : nat}) .𝛼 → 𝛼

where the bounds can be syntactically different, but equivalent, types. In the presence of records or other features, such as intersection and union types (Pottinger, 1980; Coppo et al., 1981; Barbanera et al., 1995), we can have such equivalent but not syntactically equal types. Therefore, we should generalize the rule for bounded quantification to deal with those cases. This generalization to equivalent bounds retains decidable subtyping just as kernel 𝐹 ≤ as we shall see in §4.3.

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-nominal to the rule S-rec 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, reflexivity 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 of bounded quantification due to the generalization to equivalent bounds. For those new cases, the proofs are all straightforward from the induction hypothesis.

Lemma 3.2 (Narrowing) . If Γ1 ⊢ 𝐶 ≤ 𝐶[′] and Γ1 , 𝛼 ≤ 𝐶[′] , Γ2 ⊢ 𝐴 ≤ 𝐵 then Γ1 , 𝛼 ≤ 𝐶, Γ2 ⊢ 𝐴 ≤ 𝐵 .

Theorem 3.3 (Reflexivity) . If ⊢ Γ and Γ ⊢ 𝐴 then Γ ⊢ 𝐴 ≤ 𝐴 .

Theorem 3.4 (Transitivity) . If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ 𝐵 ≤ 𝐶 then Γ ⊢ 𝐴 ≤ 𝐶 .

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 type preservation in a calculus with iso-recursive subtyping. A key difficulty in the formalization of 𝐹 ≤ [𝜇][is][proving][the][unfolding][lemma] which, due to the presence of bounded quantification, requires a different proof technique compared to the proofs by Zhou et al. (2022). We discuss the proof of the unfolding lemma in §4.1.

--- end of page.page_number=20 ---

Journal of Functional Programming

Lemma 3.5 (Unfolding Lemma) . If Γ ⊢ 𝜇𝛼. 𝐴 ≤ 𝜇𝛼. 𝐵 then Γ ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐵 ] 𝐵 .

3.2 Full 𝐹 ≤ with Iso-recursive Subtyping

In full 𝐹[𝜇][which][incorporates][full] [𝐹][≤][and][iso-recursive][types,][the][sole][distinction][from] ≤[,] the kernel variant of 𝐹[𝜇][in][permitting][contravariant][bounds,][so][we][only][present][the] ≤[lies] differences between the two variants.

Syntax and subtyping. The syntax of the full 𝐹 ≤ [𝜇][is][identical][to][that][of][the][kernel] [𝐹] ≤ [𝜇] (§3.1). As for the subtyping rules, rule S-equivall is replaced by rule S-fullall in full 𝐹[𝜇] ≤[.]

The only distinction between these two rules lies in the variance of the bounds: rule S- fullall permits contravariance, allowing 𝐴 2 to be a subtype of 𝐴 1, whereas rule S- equivall demands 𝐴 2 to be equivalent to 𝐴 1. The change to the subtyping rules in full 𝐹 ≤ [𝜇] does not impact many subtyping lemmas, such as reflexivity (Theorem 3.3) and transitivity (Theorem 3.4), which remain provable by reusing proof techniques from full 𝐹 ≤. However, as we shall see in §4.1, the unfolding lemma (Lemma 3.5) needs a different proof technique due to the presence of contravariant bounds in full 𝐹 ≤ [𝜇][.][In][§][4.1][we][will][present][a][new] generalized unfolding lemma that can be proved in both kernel and full 𝐹 ≤ [𝜇][. With this new] lemma, we can prove the unfolding lemma (Lemma 3.5) for full 𝐹 ≤ [𝜇][.]

3.3 Typing, Reduction and Type Soundness

The two variants of the subtyping rules have no impact on proving type soundness. Therefore, the typing and reduction rules remain consistent across both variants. Figure 3 shows the typing rules and reduction rules. Most rules are standard except for the typing rules for unfold and fold. For these two expressions we use structural rules instead (rule typing-sunfold and rule typing-sfold), as 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 the unfolding 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 :

Lemma 3.6 (Structural unfolding lemma) . If Γ ⊢ 𝜇𝛼. 𝐴 ≤ 𝜇𝛼.𝐶 ≤ 𝜇𝛼. 𝐷 ≤ 𝜇𝛼. 𝐵 then Γ ⊢ [ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 .

In this lemma, in the one-step unfolding the recursive types substituted in the bodies are, respectively, a supertype and a subtype of 𝜇𝛼. 𝐴 and 𝜇𝛼. 𝐵 . In contrast, in the unfolding

--- end of page.page_number=21 ---

Recursive Subtyping for All

Fig. 3: Typing and Reduction Rules.

--- end of page.page_number=22 ---

Journal of Functional Programming

Fig. 4: Structural unfolding derivation.

lemma proposed by Zhou et al. (2022), the recursive types that get substituted in the bodies are the same. As §4.1 and §5.3 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 the typing derivation of an expression unfold [ 𝐷[′] ] (fold [ 𝐶[′] ] 𝑒 ) in Figure 4. Starting from a closed expression, both 𝐶[′] and 𝐷[′] must be recursive types, thus we assume that 𝐶[′] is 𝜇𝛼.𝐶 and 𝐷[′] is 𝜇𝛼. 𝐷 . The type of unfold [ 𝐷[′] ] (fold [ 𝐶[′] ] 𝑒 ) becomes [ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 , and it should be a subtype of [ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 , which is the type of reduction result 𝑒 .

The other parts of the type soundness proof are standard, thus we have:

Theorem 3.7 (Preservation) . If ⊢ 𝑒 : 𝐴 and 𝑒↩ → 𝑒[′] then ⊢ 𝑒[′] : 𝐴 .

Theorem 3.8 (Progress) . If ⊢ 𝑒 : 𝐴 then 𝑒 is a value or 𝑒↩ → 𝑒[′] for some 𝑒[′] .

3.4 Algorithmic Typing

The rules that we have presented in Figure 3 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 5 shows the algorithmic rules for typing. Compared with the declarative typing rules, the subsumption rule (typing-sub) is removed. Also, the application (typing-app), type application (typing-tapp), structural folding (typing-sfold), structural unfolding (typing-sunfold) and record projection (typing-proj) rules are replaced by rules atypapp, atyp-tapp, atyp-sfold atyp-sunfold and atyp-proj, respectively. In the algorithmic typing rules we take the 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 find the least non-variable upper bound for a variable in the context (Pierce, 2002). Consider the term

(Λ( 𝛼 ≤ nat → nat) . 𝜆 ( 𝑦 : 𝛼 ) . 𝑦 5) : ∀( 𝛼 ≤ nat → nat) .𝛼 → nat .

Without the upper exposure function in the rule atyp-tapp, the 𝑦 in the function body would be typed as its minimal type 𝛼 , which cannot be unified with a function type with the argument type nat. The exposure function finds the smallest type that matches the expected type, such as the function type for the argument 𝑦 in the example above. Thus the upper exposure function plays an important role in finding the minimal type with the algorithmic typing rules. To make our rules more general, we additionally define the lower

--- end of page.page_number=23 ---

Recursive Subtyping for All

Fig. 5: Algorithmic Typing.

--- end of page.page_number=24 ---

Journal of Functional Programming

exposure function (Γ ⊢ 𝐴 ⇓ 𝐵 ) to find the greatest non-variable subtype 𝐵 for 𝐴 . For 𝐹 ≤ [𝜇][,] lower exposure only helps to find the correct shape for the recursive type body to be folded in rule atyp-sfold by mapping ⊤ to 𝜇𝛼. ⊤, so that it is valid to type check expressions accepted by the structural rule typing-sfold like

with the algorithmic typing rules. 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.9 (Soundness of the algorithmic rules) . If Γ ⊢ 𝑎 𝑒 : 𝐴 then Γ ⊢ 𝑒 : 𝐴 .

Theorem 3.10 (Completeness of the algorithmic rules) . If Γ ⊢ 𝑒 : 𝐴 then there exists a 𝐵 such that Γ ⊢ 𝑎 𝑒 : 𝐵 and Γ ⊢ 𝐵 ≤ 𝐴 .

Theorem 3.10 implies that our algorithm can always find a minimal type, which is an important property for 𝐹 ≤ [𝜇][.]

It should be noted that there is no difference in terms of algorithmic typing rules for both variants of 𝐹[𝜇][though][for][full] [𝐹][𝜇][the][algorithm][might][not][terminate,][since][subtyping][is] ≤[,] ≤[,] undecidable for full 𝐹[𝜇] ≤[.]

4 Metatheory of 𝐹 ≤ [𝜇]

In this section we discuss the most interesting and difficult aspects of the metatheory of 𝐹 ≤ [𝜇] in more detail. We cover three key properties: the unfolding lemma for 𝐹 ≤ [𝜇][, the] [ conservativity] of 𝐹[𝜇] ≤[over the original] [ 𝐹][≤][and] [ (un)decidability][ of subtyping. The interaction between iso-] recursive types and bounded quantification requires significant changes in the proofs of the unfolding lemma and decidability. In addition, we show how to prove the conservativity of 𝐹[𝜇] ≤[over] [ 𝐹][≤][using the algorithmic formulation of] [ 𝐹] ≤ [𝜇][.]

4.1 Unfolding Lemma

The unfolding lemma (Lemma 3.5) is a core lemma for the metatheory of a calculus with iso-recursive subtyping. Though the statement of the unfolding lemma is quite simple and intuitive to understand, the lemma cannot be proved directly. We will first review previous approaches for proving the unfolding lemma, which do not account for bounded quantification or only apply to kernel 𝐹 ≤ [𝜇][. Then we show how to generalize the unfolding lemma] to address all the complications arising from the interaction of iso-recursive subtyping and bounded quantification, including the case of full 𝐹 ≤ [𝜇][.]

The generalized unfolding lemma for iso-recursive subtyping. We first review the unfolding lemma for the special case of iso-recursive subtyping without bounded quantification. Because the premise of the unfolding lemma is restricted to a subtyping relation between two recursive types 𝜇𝛼. 𝐴 ≤ 𝜇𝛼. 𝐵 instead of two generic types 𝐴 and 𝐵 , a direct induction on the premise is problematic, as it fails to provide a useful induction hypothesis

--- end of page.page_number=25 ---

Recursive Subtyping for All

for reasoning with nominal unfoldings like [ 𝛼 ↦→ 𝐴[𝛼] ] 𝐴 , where the type after substitution may not be a recursive type. In Zhou et al. (2022)’s work the unfolding lemma is generalized to the following form:

Lemma 4.1 (The generalized unfolding lemma in Zhou et al. (2022)) . If Γ1 , 𝛼, Γ2 , ⊢ 𝐴 ≤ 𝐵 and Γ1 ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼. 𝐷 then

Γ1 , 𝛼, Γ2 ⊢[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 implies
- Γ1 , Γ2 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 ;
Γ1 , 𝛼, Γ2 ⊢[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐵 implies Γ1 , Γ2 ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐵 .

Due to the tricky interaction between rule S-var and rule S-arrow, in the generalized unfolding lemma we need two mutually dependent lemmas: one for covariant cases (1) and the other for contravariant cases (2). The proof for Lemma 4.1 proceeds by induction on Γ1 , 𝛼, Γ2 , ⊢ 𝐴 ≤ 𝐵 . In the inductive proof we need to switch between covariance and contravariance. In particular, in the rule S-arrow 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.

The generalized unfolding lemma for kernel 𝐹 ≤ [𝜇] [.][When bounded quantification is taken] into account, Lemma 4.1 is unfortunately not general enough. The key difference is that now the contexts are no longer just a list of type variables, but also associate a type bound with each type variable. Moreover, the bounds are dependent on the type variables in the order they appear, so that in the context Γ2, the bounds may contain the type variable 𝛼 . Since rule S-vartrans may look up a bound in the context Γ2, and compare it with the right-hand side of the subtyping relation, to apply the induction hypothesis, the bound type in the context should be equal to the substitution form [ 𝛼 ↦→? [𝛼] ] 𝑈 as in the subtyping relation. To address this issue, Zhou et al. (2023) extends the unfolding lemma to the following form:

Lemma 4.2 (The generalized unfolding lemma for kernel 𝐹 ≤ [𝜇][in Zhou et al. (][2023][))] [.][If (1)]

Γ1 , 𝛼 ≤⊤ , Γ2 ⊢ 𝐴 ≤ 𝐵 , (2) Γ1 ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼.𝑆 and (3) Γ1 ⊢ 𝜇𝛼.𝑆 ≤ 𝜇𝛼. 𝐷 then
1. Γ1 , 𝛼 ≤⊤ , Γ2 [ 𝛼 ↦→ 𝑆[𝛼] ] ⊢[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 implies Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 ;
2. Γ1 , 𝛼 ≤⊤ , Γ2 [ 𝛼 ↦→ 𝑆[𝛼] ] ⊢[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐵 implies Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐵 .

We explain a few key points in the proof of Lemma 4.2 together with some proof sketches below.

Firstly, the context Γ2 now comes with a substitution. Here, the syntax Γ[ 𝛼 ↦→ 𝑆 ] denotes that all the occurrences of 𝛼 in context Γ will be replaced by a specified type 𝑆 . With substitutions in the context Γ2, in case S-vartrans and S-equivall, the premise from inversion can have the same form as the original premise and thus the induction hypothesis can be applied. For example, in case S-vartrans, assume that 𝐴 := 𝛽 , 𝐵 := 𝐵 , and Γ2 contains a bound 𝛽 ≤ 𝑈 . We need to prove the following goal:

--- end of page.page_number=26 ---

Journal of Functional Programming

By analyzing the context we know that 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼.𝑆 ] 𝑈 ∈ Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ], so we only need to show

Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] ⊢[ 𝛼 ↦→ 𝜇𝛼.𝑆 ] 𝑈 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵.

This can be proved by instantiating the induction hypothesis with 𝐶 := 𝑆 and 𝐷 := 𝐷 . In this way, we overcome the issue with the substitutions in the context Γ2.

Secondly, note that the substituted type is neither 𝐶 nor 𝐷, but an intermediate type 𝑆 that lies between 𝐶 and 𝐷 . This is to ensure that the induction hypothesis can be applied to both the contravariant and covariant subgoals in case S-arrow. Otherwise, consider an alternative lemma where 𝑆 is fixed to be 𝐷 . In case S-arrow, assume that 𝐴 := 𝐴 1 → 𝐴 2 and 𝐵 := 𝐵 1 → 𝐵 2. We need to prove two subgoals:

Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 2 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 2
Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 1 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 1

If one follows the original proof steps in Lemma 4.1, the induction hypothesis has to be instantiated with 𝐶 := 𝐷 and 𝐷 := 𝐶 , so that the substitution matches with the two types in the subtyping relation for the contravariant subgoal (2). In that case, the substituted type in the context Γ2 becomes 𝜇𝛼.𝐶 , which cannot be used to prove the subgoal (2). Therefore, in Lemma 4.2 an intermediate type 𝑆 is introduced to decouple the substitution in the context and in the subtyping relation for the function case. In other words, the invariant substitution with type 𝜇𝛼.𝑆 to the context makes the induction hypothesis applicable to both subgoals, regardless of the substitution in the subtyping relation.

Finally, having the intermediate type 𝑆 will not affect the inductive proof for case S- equivall in kernel 𝐹 ≤ [𝜇][.][We][assume][that] [𝐴][:][=][ ∀(] [𝛽][≤] [𝐴][1][)] [. 𝐴][2][and] [𝐵][:][=][ ∀(] [𝛽][≤] [𝐵][1][)] [. 𝐵][2][.][The] goal would look like:

Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] ∀( 𝛽 ≤ 𝐴 1) . 𝐴 2 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] ∀( 𝛽 ≤ 𝐵 1) . 𝐵 2

After simplification and applying rule S-equivall, one of the goals becomes:

Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] , 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 1 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 2 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 2

To apply the induction hypothesis, we need to unify the new bound 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 1 and the existing context Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] into the same substitution form. In other words, we need to show the following two environments are equivalent:

This can be done by showing that 𝜇𝛼.𝑆 is equivalent to 𝜇𝛼. 𝐷 . To prove this, we rely on the fact that the bounds [ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 1 and [ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 1 are equivalent, and the following inversion lemma on substitution:

Lemma 4.3 (Substitution inversion) . If 𝐴 is equivalent to 𝐵 , and [ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 is equivalent to [ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 , then either 𝐶 is equivalent to 𝐷 or 𝛼 is not in 𝐴 nor 𝐵 .

For the first case we get from Lemma 4.3, by the fact that 𝑆 lies in the middle of 𝐶 and 𝐷 , we can show that all the three types 𝜇𝛼.𝐶 , 𝜇𝛼.𝑆 and 𝜇𝛼. 𝐷 are equivalent. For the second case, since 𝛼 is not in 𝐴 1 nor 𝐴 2, we can freely rewrite the substituted types to any types in the context. In either case, the rewriting in (4.1) can be achieved, so that the induction hypothesis can be applied to the subgoal. The critical point here is that, although

--- end of page.page_number=27 ---

Recursive Subtyping for All

the substitution form in the context is indeed affected by the new bound introduced by rule S-equivall, since kernel 𝐹 ≤ [𝜇][requires all pairs of the bounds in the subtyping relation] to be equivalent, the type 𝑆 will converge into the types 𝐶 and 𝐷 in the end.

The generalized unfolding lemma for kernel 𝐹 ≤≥ [𝜇] [.][In][Zhou][et][al.][(][2023][)’s][work,][an] extension to kernel 𝐹[𝜇][proposed,][called] [𝐹][𝜇][which][extends][kernel] [𝐹][𝜇][lower] ≤[is] ≤≥[,] ≤[with] bounded quantification and bottom types. It is worth noting that these new features will break the proof of Lemma 4.2 we have discussed above. The interaction of lower bounds and upper bounds invalidates the following inversion lemma for rule S-vartrans, which has been used to prove Lemma 4.2:

Lemma 4.4 . If 𝛼 ≤ 𝐴 ∈ Γ and Γ ⊢ 𝛼 ≤ 𝐵 , where 𝛼 ≠ 𝐵 , then Γ ⊢ 𝐴 ≤ 𝐵 .

In Lemma 4.2, there is more than one subtyping statement on the premises related to type 𝐴 and 𝐵 . During the proof we do induction on the premise (1), and use the inversion lemma to match the subderivation of [ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 with the induction hypothesis we get from the premise (1). Lemma 4.4 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:

To avoid using this inversion lemma in the proof of unfolding lemma, we need to refine the generalized unfolding lemma for kernel 𝐹 ≤ [𝜇][:]

Lemma 4.5 (The generalized unfolding lemma for 𝐹 ≤≥ [𝜇][in Zhou et al. (][2023][))] [.][If]

Γ1 , 𝛼 ≤⊤ , Γ2 ⊢ 𝐴 and Γ1 , 𝛼 ≤⊤ , Γ2 ⊢ 𝐵 ;
𝐺 ⊢[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 ;
𝐺 differs from Γ1 , 𝛼 ≤⊤ , Γ2 [ 𝛼 ↦→ 𝑆[𝛼] ] only in the components labeled by 𝛼 , where 𝑆[𝛼] can be replaced by 𝑇[𝛼] that satisfies Γ2 ⊢ 𝜇𝛼.𝑆 ≤ 𝜇𝛼.𝑇 and Γ2 ⊢ 𝜇𝛼.𝑇 ≤ 𝜇𝛼.𝑆 ,

then

Γ1 ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼.𝑆 and Γ1 ⊢ 𝜇𝛼.𝑆 ≤ 𝜇𝛼. 𝐷 implies Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 ;
Γ1 ⊢ 𝜇𝛼. 𝐷 ≤ 𝜇𝛼.𝑆 and Γ1 ⊢ 𝜇𝛼.𝑆 ≤ 𝜇𝛼.𝐶 implies Γ1 , Γ2 [ 𝛼 ↦→ 𝜇𝛼.𝑆 ] ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 .

In the refined generalized unfolding lemma, we integrate the two subtyping statements into one statement, by having the premise (1) in Lemma 4.2 induced implicitly. This can be justified by the fact that the one-time unfolding is implicitly derived from the nominal unfolding:

Lemma 4.6 (Inversion on nominal unfoldings) . If Γ ⊢[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 then Γ ⊢ 𝐴 ≤ 𝐵 .

To accommodate this change, the context is also refined to be more general, by allowing the substitution type in the subtyping context of premise (2) to be any type 𝑇 equivalent to 𝑆 . We omit the detailed proof for this lemma, since it was done in the appendix of Zhou et al. (2023), and is no longer used in the generalized unfolding lemma for full 𝐹 ≤ [𝜇][and] [ 𝐹] ≤≥ [𝜇][∧]

--- end of page.page_number=28 ---

Journal of Functional Programming

we will present in this paper. However, the idea of using Lemma 4.6 to avoid the issue of using Lemma 4.4 still applies, as we will show next.

The generalized unfolding lemma for full 𝐹 ≤ [𝜇] [.][It is not straightforward to generalize the] unfolding lemma to full 𝐹 ≤ [𝜇][.][As][we][have][seen][in][the][last][observation][of][Lemma][4.2][,][the] proof relies on the fact that the bounds in the subtyping relation are equivalent, so that during the proof, the intermediate type 𝜇𝛼.𝑆 can be rewritten to 𝜇𝛼.𝐶 or 𝜇𝛼. 𝐷 . However, in full 𝐹[𝜇] ≤[we use rule][ S-fullall][, which fails to maintain the equivalence of the bounds.] We need to consider a new approach to generalize the unfolding lemma for full 𝐹 ≤ [𝜇][.]

If we revisit the use of the generalized substitution type 𝑆 in the context Γ2 in Lemma 4.2, we can see that, during the proof, in most cases we just pass the same type 𝑆 around in the induction hypothesis. The exception is for the case of S-vartrans, where the type 𝑆 is instantiated to 𝐶 or 𝐷 . This suggests that the issues with the unfolding lemma in full 𝐹 ≤ [𝜇] can be solved if we can find a different approach to the S-vartrans case and remove the intermediate type 𝑆 from the generalized unfolding lemma. In that case, the requirement for the equivalent bounds can also be lifted.

To this end, we note that the introduction of the type 𝑆 in Lemma 4.2 is essentially an over-generalization, since throughout the derivation of [ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 , only the substitution 𝐶 or 𝐷 will be introduced into the context. Thus, the generalized unfolding lemma can focus only on the substitution of 𝐶 or 𝐷 . However, in full 𝐹 ≤ [𝜇][, it can happen that] we cannot find a uniform substitution type for the variable 𝛼 in the context Γ2. Due to the contravariant subtyping in rule S-arrow, the substitutions can flip between the two sides of the subtyping relation, so both 𝐶 and 𝐷 can be introduced into the context. Therefore, we define the following notion of related contexts to characterize such contexts:

Definition 4.7 (Related contexts) . Given a type variable 𝛼 , an initial context Γ0 and two types 𝜇𝛼.𝐶 , 𝜇𝛼. 𝐷 , two contexts Γ and Γ 𝜇 are related, written Γ � Γ 𝜇 , if they can be derived using the following rules:

The definition of related contexts is parameterized by a type variable 𝛼 and a subtyping relation Γ0 ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼. 𝐷 3. As we will see, the two contexts Γ and Γ 𝜇 are essentially the subtyping contexts that will be used in the generalized unfolding lemma for the premise and

3 We say that the related contexts are parameterized by the subtyping relation is just for the sake of convenience. They are actually parameterized by the components in the subtyping relation, i.e. the variable 𝛼 , the shared context Γ0, and the types 𝐶 and 𝐷 . Whether the subtyping relation Γ0 ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼. 𝐷 holds does not matter, as we shall see shortly.

--- end of page.page_number=29 ---

Recursive Subtyping for All

the conclusion respectively. They extend the context Γ0 with new bindings that are either under the substitution 𝐶 or 𝐷 . Moreover, each pair of bindings in the two contexts should be matched in terms of the substitution type 𝐶 or 𝐷 and the base type 𝐴 should be the same. For example, consider the following instance of the unfolding lemma we aim to prove:

By definition, Γ1 and Γ2 are related under the subtyping relation · ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼. 𝐷 , i.e. Γ1 � Γ2. When proving the above goal, for the contravariant case of function types, we need to show that the following holds:

To prove this by induction, Γ1 and Γ2 should be related under the subtyping relation · ⊢ 𝜇𝛼. 𝐷 ≤ 𝜇𝛼.𝐶 , that flips the order of 𝜇𝛼.𝐶 and 𝜇𝛼. 𝐷 in the parameter of the related contexts. This is possible because the related contexts are defined to be symmetric in terms of the substitution types 𝐶 and 𝐷 . This flexibility allows us to prove the generalized unfolding lemma for full 𝐹 ≤ [𝜇][without the need for the intermediate type] [ 𝑆][as in Lemma][ 4.2] to handle the contravariance.

With the notion of related contexts, we can prove inversion lemmas for looking up the bounds in the related contexts:

Lemma 4.8 (Inversion lemma for related contexts) . If Γ and Γ 𝜇 are related under the variable 𝛼 , the shared context Γ0, and the types 𝜇𝛼.𝐶 and 𝜇𝛼. 𝐷 , then for any type variable 𝛽 , if 𝛽 ≤ 𝑈 ∈ Γ and 𝛽 ≠ 𝛼 , one of the following holds:

there exists 𝑈[′] , s.t. 𝑈 = [ 𝛼 ↦→ 𝐶[𝛼] ] 𝑈[′] and 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝑈[′] ∈ Γ 𝜇 , or
there exists 𝑈[′] , s.t. 𝑈 = [ 𝛼 ↦→ 𝐷[𝛼] ] 𝑈[′] and 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝑈[′] ∈ Γ 𝜇 .

We can now state the generalized unfolding lemma for full 𝐹 ≤ [𝜇][:]

Lemma 4.9 (The generalized unfolding lemma for full 𝐹 ≤ [𝜇][)] [.][If contexts][ Γ][ and][ Γ] [𝜇][are related] under variable 𝛼 and if Γ0 ⊢ 𝜇𝛼.𝐶 ≤ 𝜇𝛼. 𝐷 , then

Γ ⊢[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 implies Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵
Γ ⊢[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐵 implies Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐵
Γ ⊢[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐶[𝛼] ] 𝐵 implies Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐵
Γ ⊢[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 implies Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵

Compared to previous versions of the unfolding lemma, in addition to conclusion (1) and (2), which talk about the covariant and contravariant substitutions, now we add two more conclusions (3) and (4) for the case where the substitutions are the same as 𝐶 or 𝐷 . As we will show in the proof sketch below, these two additional conclusions generate useful induction hypotheses for the proof of rule S-vartrans, so that we no longer need to rely on the intermediate type 𝑆 as we did in Lemma 4.2. Moreover, we follow the same approach as in Lemma 4.9 to drop the premise of 𝐴 ≤ 𝐵 and avoid the use of inversion lemmas.

--- end of page.page_number=30 ---

Journal of Functional Programming

Proof We prove the four mutually dependent goals in the lemma by induction on the premise Γ ⊢[ 𝛼 ↦→? [𝛼] ] 𝐴 ≤[ 𝛼 ↦→? [𝛼] ] 𝐵 . We unroll the mutual induction hypothesis here and assume four separate induction hypotheses available in the proof for the sake of presentation. In the rest of the proof we will refer to them as IH( 𝑛 ) for the induction hypothesis generated by the proof goal ( 𝑛 ). We show the interesting cases below:

Rule S-vartrans: We show the proof goal (1) here. Assume 𝐴 = 𝛽 , where 𝛽 ≤ 𝑈 ∈ Γ, and Γ ⊢ 𝑈 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 , by Lemma 4.8 we get two cases:
1. There exists 𝑈[′] , 𝑈 = [ 𝛼 ↦→ 𝐶[𝛼] ] 𝑈[′] and 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝑈[′] ∈ Γ 𝜇 . We need to show Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝑈[′] ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 . We can apply IH(1) directly.
2. There exists 𝑈[′] , 𝑈 = [ 𝛼 ↦→ 𝐷[𝛼] ] 𝑈[′] and 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝑈[′] ∈ Γ 𝜇 . We need to show Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝑈[′] ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 . We can apply IH(4) directly. Note that in this case, the substituted type on both sides is 𝐷 , which motivated us to state cases (3) and (4) in the lemma.

The proof for the other cases is similar to this one, by first applying Lemma 4.8 to get the corresponding cases, and then choosing the induction hypothesis that applies to complete the proof.

Rule S-arrow: Assume 𝐴 = 𝐴 1 → 𝐴 2 and 𝐵 = 𝐵 1 → 𝐵 2, for proof goal (1), we need to prove two subgoals:
1. Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 1 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 1
2. Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 2 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 2

The covariant subgoal (2) follows from IH(1) directly. In subgoal (1), due to the contravariant subtyping, the substituted types are flipped in the subtyping relation. Therefore we need to apply IH(2) to complete the proof. The proof of subgoal (2) is similar to the proof of subgoal (1), by applying IH(1) to the contravariant subgoal, and IH(2) to the covariant subgoal. For subgoals (3) and (4), the induction hypothesis can be applied directly since the substituted types are the same on both sides.

Rule S-fullall: Assume 𝐴 = ∀( 𝛽 ≤ 𝐵 1) . 𝐴 1 and 𝐵 = ∀( 𝛽 ≤ 𝐵 2) . 𝐴 2. We show the proof of goal (1) here. In this case we need to prove two subgoals:
1. Γ 𝜇 ⊢[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 2 ≤[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐵 1
2. Γ 𝜇, 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 2 ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 1 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐴 2

The proof of subgoal (1) is similar to the proof of subgoal (1) in the rule S-arrow case, by applying IH(2) to the contravariant subgoal. Next, in order to apply IH(1) to the covariant subgoal (2), we need to show that the context (Γ , 𝛽 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 2) and (Γ 𝜇, 𝛽 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 2) are related, which follows from the definition of related contexts. Therefore, we can apply IH(1) to complete the proof. The proof of other goals is similar to the proof of goal (1). Thanks to our definition of related contexts, we do not need to worry about whether the substituted type is 𝐶 or 𝐷 when we add a new binding into the context in the proof of subgoal (2). ■

To conclude, in this generalized unfolding lemma, we introduce two more conclusions for the case where the substitutions are the same as 𝐶 or 𝐷 , and we define related contexts to characterize the contexts that will be used in the proof. In this way, we prove the case of rule S-vartrans without the need for an intermediate type 𝑆 , so that rule S-fullall can be handled as well. In fact, the proof technique we use here is quite general. We also redevelop a generalized unfolding lemma for kernel 𝐹 ≤ [𝜇][using the same approach as in full] [ 𝐹] ≤ [𝜇][. As we]

--- end of page.page_number=31 ---

Recursive Subtyping for All

will see, this generalized unfolding lemma can also be used to prove 𝐹 ≤≥ [𝜇][∧][, without the need] for significant changes.

4.2 Conservativity

One important feature of 𝐹 ≤ [𝜇][is that it is conservative over] [𝐹][≤][. Conservativity means that] equivalent 𝐹 ≤ judgements 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.

To avoid ambiguity, we let ⊢ 𝐹 Γ be the well-formedness of environment, Γ ⊢ 𝐹 𝐴 be the well-formedness of types, Γ ⊢ 𝐹 𝐴 ≤ 𝐵 be the subtyping relation, ⊢ 𝐹 𝑒 be the wellformedness of expressions, and Γ ⊢ 𝐹 𝑒 : 𝐴 be the typing relation in 𝐹 ≤, where the subscript 𝐹 stands for the original 𝐹 ≤ calculus. All the definitions and rules for 𝐹 ≤ are essentially subsets of the corresponding definitions and rules for 𝐹 ≤ [𝜇][presented in][ §][3][, except that the] rules involving records and recursive types are removed, and that in kernel 𝐹 ≤, the rule S- equivall is replaced with the rule S-kernelall. Note that the properties we will show below in this section are demonstrated in both variants of 𝐹[𝜇][In][other][words,][full] [𝐹][𝜇] ≤[.] ≤[is] conservative over full 𝐹 ≤ and kernel 𝐹 ≤ [𝜇][is conservative over kernel] [ 𝐹][≤][.]

Conservativity of subtyping. Our conservativity result for subtyping is relatively easy to establish:

Lemma 4.10 (Conservativity for subtyping) . If Γ, 𝐴 , and 𝐵 are well-formed in 𝐹 ≤, namely (1) ⊢ 𝐹 Γ, (2) Γ ⊢ 𝐹 𝐴 , and (3) Γ ⊢ 𝐹 𝐵 , then Γ ⊢ 𝐹 𝐴 ≤ 𝐵 if and only if Γ ⊢ 𝐴 ≤ 𝐵 .

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 proof of this lemma is straightforward, except for the case of rule S-equivall from 𝐹[𝜇][𝐹][≤][,][as][the][rule][S-kernelall][in] [𝐹][≤][requires][the][two][types][to][be][exactly][the] ≤[to] same instead of being equivalent. This is easy to fix, given that kernel 𝐹 ≤ subtyping is antisymmetric. This property was shown by Baldan et al. (1999) for a restricted form of F- bounded quantification, and we adapt their proof to our setting. The antisymmetry property is stated as follows:

Lemma 4.11 (Antisymmetry of kernel 𝐹 ≤ subtyping) . If Γ ⊢ 𝐹 𝐴 ≤ 𝐵 and Γ ⊢ 𝐹 𝐵 ≤ 𝐴 in kernel 𝐹 ≤, then 𝐴 = 𝐵 .

Conservativity of typing. It is straightforward to obtain one direction of the conservativity result, from a typing relation in 𝐹 ≤ to a typing relation in 𝐹 ≤ [𝜇][. As for the reverse direction,] the situation is more complicated. If we want to derive Γ ⊢ 𝐹 𝑒 : 𝐴 from Γ ⊢ 𝑒 : 𝐴 , when doing induction, for the subsumption case (rule typing-sub), we need to guess an intermediate

--- end of page.page_number=32 ---

Journal of Functional Programming

type. However, we do not know if it involves recursive types or not. Consider the following example:

Although the final judgement ⊢ 𝜆𝑥. 𝑥 : ⊤ does 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 expressions that do not use fold/unfold constructors, their minimum types do not contain recursive types either. We state this property as the conservativity lemma for subtyping:

Lemma 4.12 . If Γ, 𝐴 , and 𝑒 are well-formed in 𝐹 ≤, namely (1) ⊢ 𝐹 Γ, (2) Γ ⊢ 𝐹 𝐴 , and (3) ⊢ 𝐹 𝑒 , then Γ ⊢ 𝑎 𝑒 : 𝐴 implies Γ ⊢ 𝐹 𝑒 : 𝐴 .

Now, given a typing relation Γ ⊢ 𝑒 : 𝐴 in 𝐹 ≤ [𝜇][,][we][first][use][the][minimum][typing][property] (Theorem 3.10) to obtain its minimum type 𝐵 such that Γ ⊢ 𝑎 𝑒 : 𝐵 and Γ ⊢ 𝐵 ≤ 𝐴 . Applying Lemma 4.12 and Lemma 4.10, we complete the conservativity proof for the declarative version of 𝐹[𝜇] ≤[.]

Theorem 4.13 (Conservativity) . If Γ, 𝐴 , and 𝑒 are well-formed in 𝐹 ≤, namely (1) ⊢ 𝐹 Γ, (2) Γ ⊢ 𝐹 𝐴 , and (3) ⊢ 𝐹 𝑒 , then Γ ⊢ 𝐹 𝑒 : 𝐴 if and only if Γ ⊢ 𝑒 : 𝐴 .

4.3 Decidability

This section focuses on the decidability of kernel 𝐹 ≤ [𝜇][.][We][first][start][by][reviewing][the] approaches to proving decidability in kernel 𝐹 ≤, and in nominal unfoldings, and then describe our approach to prove decidability. These two previous approaches to proving decidability employ different measures, which creates a challenge for proving the decidability of kernel 𝐹 ≤ [𝜇][.]

Decidability of kernel 𝐹 ≤ . It is well-known that bounded quantification for full 𝐹 ≤ is undecidable (Pierce, 1994). However, for kernel 𝐹 ≤, identical bounds make the system decidable. A common practice is to define a weight function to compute the size of a type (Pierce, 2002):

weight Γ (⊤) = 1 weight Γ1 ,𝛼 ≤ 𝐴, Γ2 ( 𝛼 ) = 1 + weight Γ1 ( 𝐴 ) weight Γ (∀( 𝛼 ≤ 𝐴 ) . 𝐵 ) = 1 + weight Γ ,𝛼 ≤ 𝐴 ( 𝐵 ) weight Γ ( 𝐴 → 𝐵 ) = 1 + weight Γ ( 𝐴 ) + weight Γ ( 𝐵 )

For a universal type, 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

--- end of page.page_number=33 ---

Recursive Subtyping for All

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 size of types will increase. Thus a straightforward induction on the size of types does not work. Zhou et al. (2022) choose a size measure based on an overapproximation of the height of the fully unfolded tree. Concretely, the height of a type 𝐴 in a measure context Ψ (Ψ := · | Ψ , 𝛼 ↦→ 𝑖 , where 𝑖 is a natural number) is defined as:

The size measure of a type 𝐴 is defined as height ( 𝐴 ) where the context is empty. In contrast to kernel 𝐹 ≤, the context here is used to store the size of the corresponding recursive variables. The key design in the height function is that the measure of a recursive type 𝜇𝛼. 𝐴 is computed by first setting the measure of the recursive variable to 0, and then computing the measure of the body, which achieves the effect of measuring the type body 𝐴 considering 𝛼 as a free variable. The computed measure is then incremented by one to account for the labeled type 𝐴[𝛼] , then height ( 𝐴 ) is computed again with the context updated for the recursive variable, so that intuitively the result of height ( 𝜇𝛼. 𝐴 ) measures the size of [ 𝛼 ↦→ 𝐴[𝛼] ] 𝐴 plus one. Zhou et al. (2022) prove that such height measure work well with nominal unfolding rules, as the height of a type will precisely decrease by one for every nominal unfolding.

Decidability of kernel 𝐹 ≤ [𝜇] [.][To][combine][these][two][approaches,][we][need][to][extend][the] measure of nominal unfoldings with the measure of kernel 𝐹 ≤ in a seamless manner. One easy fix to unify the two measures is to use the maximum function for both measures, as the nominal unfolding measure does. However, there are three remaining main challenges that we must address:

Inconsistent measures for variables : In the height function, type variables are treated as base cases, whereas in the weight function, the computation continues by retrieving the variable’s bound from the context. In kernel 𝐹[𝜇] ≤[, we do not distinguish between recursive]
and universal variables, so we need to find a unified way to measure variables.
Different purposes of contexts : The context in the weight function straightforwardly keeps track of universal bounds, which are later retrieved to compute the measure of a universal variable. This ensures that the premises in rule S-vartrans have smaller type measures than the conclusion. However, this trick does not work for nominal unfoldings, as shown by the case height Ψ ( 𝜇𝛼. 𝐴 ), where the context is extended with two different measures for the same variable at different points in the computation to simulate the nominal unfolding. This discrepancy complicates the unification of the two measures.
Loss of measure information with equivalent bounds : We use rule S-equivall instead of the standard rule S-kernelall for 𝐹 ≤. Given the equivalent bounds in kernel 𝐹 ≤,

--- end of page.page_number=34 ---

Journal of Functional Programming

the measure for the subtyping relation Γ ⊢∀( 𝛼 ≤ 𝐴 1) . 𝐵 1 ≤∀( 𝛼 ≤ 𝐴 2) . 𝐵 2 includes the measures of 𝐴 1, 𝐴 2, 𝐵 1, and 𝐵 2. However, the measure for the premise Γ , 𝛼 ≤ 𝐴 2 ⊢ 𝐵 1 ≤ 𝐵 2 loses the measure of 𝐴 1 because it is not stored.

We first show the measure used for the decidability of kernel 𝐹 ≤ [𝜇][, and then discuss how it] addresses the concerns above. The measure is relatively simple and based on the approach from Zhou et al. (2022). We use the same context Ψ := · | Ψ , 𝛼 ↦→ 𝑖 and now it is used to store the measures of (both universal and recursive) variables during the measure computation. Then, a measure function size Ψ ( 𝐴 ), is defined on types as follows:

The formulation of the size function is very similar to the height function. We have an extra rule for universal 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 them as 1.

We solve the first 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 fits our needs naturally.

As for the second concern, despite the different purposes of contexts, the key ideas of measuring types in kernel 𝐹 ≤ and nominal unfoldings are the same: they both relate the measure of a variable to what the variable will be substituted with in the context of the subtyping rule, either its unfolded form as a labeled type or its bound type. A slight modification is made based on the definition of weight . In the weight function, for a universal variable, its bound is first retrieved and then the measure is computed. To align with the “pre-computation” mechanism of measuring nominal unfoldings ( 𝑖 := size Ψ ,𝛼 ↦→1 ( 𝐴 )), we also pre-compute the measure of the bound ( 𝑖 := size Ψ ( 𝐴 )) in the size function, so that we retrieve the measure instead of the type bound from the 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 arises with variables in the initial subtyping context. When measuring nominal unfoldings, the context in a subtyping relation is simply a list of variables, without any bound information, so variables that occur freely can be counted as 0 in the height function. In contrast, now the subtyping context stores the bound information, and the measures of bounds play a role in deciding the subtyping relation. To address this issue, we need to make sure that the bound information is pre-computed in the measure function.

--- end of page.page_number=35 ---

Recursive Subtyping for All

We transform a subtyping context into an environment containing measures Ψ, which track universal variables. In our decidability proof statement (Lemma 4.14), Ψ is computed from the subtyping context Γ by an evaluation function 𝑒𝑣𝑎𝑙 : Γ ↩ → Ψ, defined as:

With both 𝑒𝑣𝑎𝑙 and 𝑠𝑖𝑧𝑒 we can then state the decidability theorem:

Lemma 4.14 . If sizeeval (Γ) ( 𝐴 ) + sizeeval (Γ) ( 𝐵 ) ≤ 𝑘 then there exists an algorithm that terminates and decides whether Γ ⊢ 𝐴 ≤ 𝐵 .

Theorem 4.15 (Decidability of kernel 𝐹 ≤ [𝜇][subtyping)] [.][Γ][ ⊢] [𝐴][≤] [𝐵][is decidable in kernel] [ 𝐹] ≤ [𝜇][.] Theorem 4.16 (Decidability of kernel 𝐹 ≤ [𝜇][typing)] [.][Γ][ ⊢] [𝑒][:] [ 𝐴][is decidable in kernel] [ 𝐹] ≤ [𝜇][.]

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 addition of records makes the subtyping relation not antisymmetric: two equivalent record types may be syntactically different. The lack of antisymmetry poses a challenge for our decidability proof, in particular for rule S-equivall. Nevertheless, for kernel 𝐹[𝜇] ≤[two equivalent records must have the same set of fields, and the two types for each] field must be equivalent. Therefore, the measures of two equivalent record types remain the same. As a result, the measure of two equivalent bounds 𝐴 1 and 𝐴 2 is equal, as Lemma 4.17 describes. The measure information of type 𝐴 1 can therefore be reconstructed from type 𝐴 2, addressing the final concern with decidability.

Lemma 4.17 . If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ 𝐵 ≤ 𝐴 then sizeeval (Γ) ( 𝐴 ) = sizeeval (Γ) ( 𝐵 ).

Undecidability of subtyping full 𝐹 ≤ [𝜇] [.][It is well known that the full] [ 𝐹][≤][subtyping relation] is undecidable (Pierce, 1994). Although the original formulation of full 𝐹 ≤ includes the transitivity rule, it can be reformulated into a syntax-directed version (Curien and Ghelli, 1992) that eliminates the transitivity rule, as we have adopted in 𝐹 ≤ [𝜇][. The syntax-directed] version of 𝐹 ≤ naturally forms a subtype checking algorithm. However, for full 𝐹 ≤, Ghelli (1993) demonstrated a non-terminating example for the subtyping algorithm. Furthermore, Pierce (1994) proved the undecidability of full 𝐹 ≤ by encoding a Turing machine using full 𝐹 ≤. Since we have shown in §4.2 that full 𝐹 ≤ [𝜇][is conservative over the syntax-directed] version of full 𝐹 ≤, Ghelli (1993)’s counterexample for full 𝐹 ≤ also applies to full 𝐹 ≤ [𝜇][.] Therefore, the undecidability of full 𝐹 ≤ [𝜇][is a corollary of the undecidability of full] [ 𝐹][≤][and] the conservativity of full 𝐹 ≤ [𝜇][over full] [ 𝐹][≤][.]

Theorem 4.18 (Undecidability of typing and subtyping for full 𝐹 ≤ [𝜇][)] [.][The subtyping relation] Γ ⊢ 𝐴 ≤ 𝐵 and the typing relation Γ ⊢ 𝑒 : 𝐴 are undecidable in full 𝐹 ≤ [𝜇][.]

5 A Calculus with Lower and Upper Bounded Quantification

In this section we introduce an extension of 𝐹[𝜇][called] [𝐹][𝜇][∧][with][lower][bounded][quan-] ≤[,] ≤≥[,] tification, the bottom type, and an alternative formulation of record types in terms of

--- end of page.page_number=36 ---

Journal of Functional Programming

intersections of single field record types . While upper bounded quantification has received a lot of attention in previous research, lower bounded quantification for an 𝐹 ≤-like language is much less explored, though it appears in a few works (Oliveira et al., 2020; Amin and Rompf, 2017). We follow the same approach as Oliveira et al. (2020), whose 𝐹 ≤ extension allows type variables to have either a lower bound or an upper bound, but not both bounds at once. We also introduce single-field record types and intersection types to replace record types in 𝐹 ≤ [𝜇][. Intersection types enable type level record extension and further applications] resembling the treatment of object types in the DOT calculus (Rompf and Amin, 2016). As discussed in §2.2, our extensions in 𝐹 ≤≥ [𝜇][∧][enable further applications, such as a form of] extensible encodings of datatypes. We have proved all the same results for 𝐹 ≤≥ [𝜇][∧][that were] proved for kernel 𝐹 ≤ [𝜇][, 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 quantification are introduced. We also remove record types ({ 𝑙𝑖 : 𝐴𝑖[𝑖][∈][1][···] [𝑛] }) from the syntax, and instead introduce intersection types and single-field record types. The syntactic differences are highlighted in gray .

|Types|𝐴, 𝐵, …|�|nat| ⊤|
⊥| 𝐴_1→_𝐴_2|𝛼|𝜇𝛼. 𝐴| 𝐴𝛼|nat| ⊤|
⊥| 𝐴_1→_𝐴_2|𝛼|𝜇𝛼. 𝐴| 𝐴𝛼||| |---|---|---|---|---|---|---| ||||| ∀(𝛼_≤_𝐴). 𝐵|
∀(𝛼_≥_𝐴). 𝐵|
𝐴&𝐵|||{𝑙:𝐴}|| |Expressions|𝑒|�|𝑥|i|𝑒_1 𝑒_2|𝜆𝑥:𝐴. 𝑒|𝑒𝐴|Λ(𝛼_≤_𝐴). 𝑒||||Λ(𝛼_≥_𝐴). 𝑒| |||||unfold [𝐴] 𝑒|fold [𝐴] 𝑒| {𝑙𝑖=𝑒𝑖𝑖_∈1···𝑛} |𝑒.𝑙|||| |Values|𝑣|�|i|𝜆𝑥:𝐴. 𝑒|fold [𝐴] 𝑣|Λ(𝛼_≤_𝐴). 𝑒_|||Λ(𝛼_≥_𝐴). 𝑒|| ||||| {𝑙𝑖=𝑣𝑖𝑖_∈1···𝑛}|||| |Contexts|Γ|�|· |Γ, 𝛼_≤_𝐴_|
Γ_, 𝛼_≥_𝐴_|Γ_, 𝑥_:𝐴||||

Subtyping, typing and reduction. The well-formedness for the additional bottom types, single-field record types and universal types with lower bounds are standard, as shown in Figure 6. For intersection types, we only allow single-field record types, or intersections of record types with distinct labels to be well-formed. This can be characterized by a compatibility relation 𝐴 # 𝐵 between types. We make this simplified design choice to avoid the complexity of general unrestricted intersection types, which would cause trouble in the two key properties of the type system, namely the structural unfolding lemma (Lemma 5.11) and the decidability of subtyping (Theorem 5.14), as we will discuss in §5.3.

As for the subtyping rules, compared with 𝐹 ≤ [𝜇][,][we][add][rules][S-bot][,][S-vartranslb][,] and S-equivalllb for subtyping with bottom types and lower bounded quantification. The record subtyping rule S-rcd in 𝐹 ≤ [𝜇][is now replaced by rule][ S-srcd][ for subtyping single-field] record types together with rules S-andla, S-andlb, and S-andr for subtyping intersection types. Note that in the subtyping rule for intersection types, we also add the compatibility restriction in the premise, to ensure the regularity of the subtyping relation (Lemma 5.1).

Lemma 5.1 (Regularity of subtyping in 𝐹 ≤≥ [𝜇][∧][)] [.][If][Γ][ ⊢] [𝐴][≤] [𝐵][then][the][following][well-] formedness conditions hold: (1) ⊢ Γ, (2) Γ ⊢ 𝐴 and (3) Γ ⊢ 𝐵 .

--- end of page.page_number=37 ---

Recursive Subtyping for All

Fig. 6: Additional well-formedness and subtyping rules for 𝐹 ≤≥ [𝜇][∧][with respect to] [ 𝐹] ≤ [𝜇][.]

The new subtyping relation is reflexive and transitive:

Theorem 5.2 (Reflexivity for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ ⊢][Γ][ and][ Γ][ ⊢] [𝐴][then][ Γ][ ⊢] [𝐴][≤] [𝐴][.] Theorem 5.3 (Transitivity for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ Γ][ ⊢] [𝐴][≤] [𝐵][and][ Γ][ ⊢] [𝐵][≤] [𝐶][then][ Γ][ ⊢] [𝐴][≤] [𝐶][.]

Figure 7 shows the changes of 𝐹 ≤≥ [𝜇][∧][with respect to] [ 𝐹] ≤ [𝜇][in terms of typing and reduction.] For lower bounded quantification, we add rules typing-tapplb and typing-tabslb for typing and rule step-tabslb for reduction, which are simply dual forms of rules typingtapp, typing-tabs, and step-tabs, respectively. For records, since the syntax of record expressions is unchanged, there are no further changes in the reduction rules. The typing rule for record projections is also simplified. Since record types are now represented by single-field record types, the projection of a record can be directly modeled by the subtyping relation. Rules typing-rcdnil and typing-srcd form the typing rules for record expressions.

Structural folding and lower bounded quantification. The structural folding rule typing-sfold 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]

--- end of page.page_number=38 ---

Journal of Functional Programming

Γ ⊢ 𝑒 : 𝐴

(Typing)

𝑒 1 ↩ → 𝑒 2 (Reduction)

step-tabslb

Fig. 7: Additional typing and reduction rules for 𝐹 ≤≥ [𝜇][∧][with respect to] [ 𝐹] ≤ [𝜇][.]

another recursive type or the ⊤ type. Thus the effect 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 Add∀ constructors of the Exp1 and Exp2 datatypes that we have presented in §2.2, while the standard folding rule cannot. The rule typing-sfold 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 broadly applicable to various type system extensions to 𝐹 ≤ [𝜇][.]

Type soundness. Our type soundness proof for 𝐹 ≤≥ [𝜇][∧][is standard:]

Theorem 5.4 (Preservation for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ ⊢] [𝑒][:] [ 𝐴][and] [ 𝑒↩][→] [𝑒][′][then][ ⊢] [𝑒][′][ :] [ 𝐴][.] Theorem 5.5 (Progress for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ ⊢] [𝑒][:] [ 𝐴][then] [ 𝑒][is a value or exists] [ 𝑒][′] [, 𝑒↩][→] [𝑒][′][.]

5.2 Algorithmic typing

Similarly to 𝐹 ≤ [𝜇][, we can define an algorithmic typing system for] [ 𝐹] ≤≥ [𝜇][∧][. We present the changes] in the algorithmic typing rules for 𝐹 ≤≥ [𝜇][∧][in Figure][ 8][. Rules][ atyp-tabslb][ and][ atyp-tapplb][ are] added to handle lower bounded quantification. Rules atyp-rcdnil and atyp-srcd replace the record typing rule typing-rcd in 𝐹 ≤ [𝜇][. In addition to these standard changes, there are] also a few special cases that need to be handled for 𝐹 ≤≥ [𝜇][∧][.]

Firstly, bottom types bring several extra cases to the algorithmic typing rules. 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 any argument, as also observed by Pierce (1997). To ensure that the algorithmic typing rules are complete, we need to add rules atyp-appbot and atyp-tappbot to handle these cases. We also develop a similar treatment for recursive types, as shown in rules atyp-sunfoldbot and atyp-sfoldtop.

--- end of page.page_number=39 ---

Recursive Subtyping for All

(Algorithmic Typing)

Fig. 8: The additional algorithmic typing rules for 𝐹 ≤≥ [𝜇][∧][.]

Moreover, with two kinds of bounded quantification, the meanings of the two exposure functions also need to be refined. For example, the upper exposure function (⇑) is now used to find the least upper bound in the context that is not an upper-bounded variable , so it will return the variable itself if the variable is lower bounded. We redefine the exposure functions for 𝐹[𝜇][∧] ≤≥[in Figure][ 9][. For lower exposure, we also need a dual form of the rule][ XA-promote][,] which finds the greatest lower bound in the context that is not a lower-bounded variable , as shown in rule XA-downpromote.

Record exposure. Furthermore, for typing record projections, recall that in the declarative rule typing-sproj, the lookup of the field label 𝑙 is implied by the implicit subtyping between the expression type and the single field record type for { 𝑙 : 𝐴 }. In the algorithmic system, we need to find a mechanism to find such 𝐴 . Therefore we define a new exposure relation for record types in 𝐹 ≤≥ [𝜇][∧][.][The][record][exposure][relation][Γ][ ⊢] [𝐴][⇒] [𝑙][𝐵][indicates][that] from the type 𝐴 we can lookup the field label 𝑙 and get the type 𝐵 . We show the full definition of the record exposure relation in Figure 9. Note that, in addition to single-field record types (rule XR-srcd) and intersection types (rules XR-anda, XR-andb, and XR-andr), one can also lookup ⊥ from ⊥ (rule XR-bot), as well as upper bounds from upper bounded variables (rule XR-promote). With the record exposure relation we define rule atyp-sproj for record projections to replace rule atyp-proj in 𝐹 ≤ [𝜇][.][The][record][exposure][relation][is][sound][and] complete for the subtyping relation 𝐴 ≤{ 𝑙 : 𝐵 }.

Lemma 5.6 (Record exposure properties for 𝐹 ≤≥ [𝜇][∧][)] [.]

--- end of page.page_number=40 ---

Journal of Functional Programming

Γ ⊢ 𝐴 ⇑ 𝐵 (Upper Exposure) XA-promote XA-upinv XA-up 𝛼 ≤ A ∈ Γ Γ ⊢ A ⇑ B 𝛼 ≥ A ∈ Γ A is not a type variable Γ ⊢ 𝛼 ⇑ B Γ ⊢ 𝛼 ⇑ 𝛼 Γ ⊢ A ⇑ A Γ ⊢ 𝐴 ⇓ 𝐵 (Lower Exposure) XA-downpromote XA-downinv XA-downward 𝛼 ≥ A ∈ Γ Γ ⊢ A ⇓ B 𝛼 ≤ A ∈ Γ A is not a type variable Γ ⊢ 𝛼 ⇓ B Γ ⊢ 𝛼 ⇓ 𝛼 Γ ⊢ A ⇓ A Γ ⊢ 𝐴 ⇒ 𝑙 𝐵 (Record Exposure) XR-promote XR-anda XR-andb 𝛼 ≤ A ∈ Γ Γ ⊢ A ⇒ l B Γ ⊢ A 1 ⇒ l B Γ ⊢ A 2 ⇒ l B Γ ⊢ 𝛼 ⇒ l B Γ ⊢ A 1 & A 2 ⇒ l B Γ ⊢ A 1 & A 2 ⇒ l B XR-srcd XR-bot Γ ⊢{ 𝑙 : A } ⇒ l A Γ ⊢⊥⇒ l ⊥

Fig. 9: The new exposure functions for 𝐹 ≤≥ [𝜇][∧][.]

If Γ ⊢ 𝐴 ⇒ 𝑙 𝐵 then Γ ⊢ 𝐴 ≤{ 𝑙 : 𝐵 }.
If Γ ⊢ 𝐴 ≤{ 𝑙 : 𝐵 } then there exists 𝐶 such that Γ ⊢ 𝐴 ⇒ 𝑙 𝐶 and Γ ⊢ 𝐶 ≤{ 𝑙 : 𝐵 }.

With these considerations in the algorithmic typing rules, we prove the soundness and completeness of the algorithmic typing system with respect to the declarative typing rules defined in Figure 7.

Theorem 5.7 (Soundness of the algorithmic rules for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ Γ][ ⊢] [𝑎][𝑒][:] [ 𝐴][then][ Γ][ ⊢] [𝑒][:] [ 𝐴][.] Theorem 5.8 (Completeness of the algorithmic rules for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ Γ][ ⊢] [𝑒][:] [ 𝐴][then there exists] 𝐵 such that Γ ⊢ 𝑎 𝑒 : 𝐵 and Γ ⊢ 𝐵 ≤ 𝐴 .

5.3 Metatheory of 𝐹 ≤≥ [𝜇][∧]

The addition of lower bounded quantification, bottom types, and intersection types creates some difficulties in the metatheory of 𝐹 ≤≥ [𝜇][∧][. In the following, we describe how to overcome] the difficulties, by adjusting the proof techniques we have used for 𝐹 ≤ [𝜇][.]

Unfolding Lemma. As discussed in §4.1, in a type system that simultaneously allows introducing lower and upper bounded types, the inversion lemma for rule S-vartrans (Lemma 4.4) is not valid. This is exactly the case for 𝐹 ≤≥ [𝜇][∧][.][To][resolve][this][issue,][the] unfolding lemmas should only state the subtyping relation between the nominal unfoldings [ 𝛼 ↦→ 𝐶[𝛼] ] 𝐴 ≤[ 𝛼 ↦→ 𝐷[𝛼] ] 𝐵 and remove the one-step unfolding relation 𝐴 ≤ 𝐵 from the

--- end of page.page_number=41 ---

Recursive Subtyping for All

premise. Therefore, we use the same statement of the generalized unfolding lemma as in full 𝐹[𝜇][4.9][),][under][an][extended][version][of][related][contexts][(Definition][4.7][)][that] ≤[(Lemma] takes lower bounded bindings into account. It turns out that, with only changes of the proof in cases S-equivall and S-equivalllb, the generalized unfolding lemma can be proved for 𝐹[𝜇][∧] ≤≥[as well, which results in the following unfolding lemma for] [ 𝐹] ≤≥ [𝜇][∧][.]

Lemma 5.9 (Unfolding lemma for 𝐹 ≤≥ [𝜇][∧][)] [.][If][Γ][ ⊢] [𝜇𝛼. 𝐴][≤] [𝜇𝛼. 𝐵][, then][Γ][ ⊢[] [𝛼][↦→] [𝜇𝛼. 𝐴][]] [𝐴][≤] [ 𝛼 ↦→ 𝜇𝛼. 𝐵 ] 𝐵 .

To prove type soundness, we need to show the structural unfolding lemma. If we check the typing derivation with structural folding and unfolding illustrated in Figure 4 again in 𝐹 ≤≥ [𝜇][∧][,] we can see that by inversion on the subtyping relation · ⊢ 𝜇𝛼. 𝐴 ≤ 𝐶[′] and · ⊢ 𝐷[′] ≤ 𝜇𝛼. 𝐵 , we can no longer guarantee that 𝐶[′] and 𝐷[′] are recursive types, since they can also be intersection types. To remedy this, the compatibility relation 𝐴 # 𝐵 is enforced by the well-formedness of intersection types, so that intersection types can only be formed from single-field record types, not by recursive types. We can prove the following lemma to derive a contradiction for the case of intersection types and recover the structural unfolding lemma as well as type soundness for 𝐹 ≤≥ [𝜇][∧][.]

Lemma 5.10 . For any types 𝐴 , 𝐵 1 and 𝐵 2, it cannot happen that 𝜇𝛼. 𝐴 ≤ 𝐵 1 & 𝐵 2 or 𝐵 1 & 𝐵 2 ≤ 𝜇𝛼. 𝐴 in 𝐹 ≤≥ [𝜇][∧][.]

Lemma 5.11 (Structural unfolding lemma for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ Γ][ ⊢] [𝜇𝛼. 𝐴][≤] [𝜇𝛼.𝐶][≤] [𝜇𝛼. 𝐷][≤] [𝜇𝛼. 𝐵] then Γ ⊢[ 𝛼 ↦→ 𝜇𝛼.𝐶 ] 𝐴 ≤[ 𝛼 ↦→ 𝜇𝛼. 𝐷 ] 𝐵 .

Decidability. The interaction between bottom types and rule S-equivall breaks the measure-based decidability proof in §4.3. The bottom type in 𝐹 ≤≥ [𝜇][∧][brings][a][new][form] of equivalent types: when 𝛼 ≤⊥∈ Γ, one can derive that Γ ⊢ 𝛼 ≤⊥ and Γ ⊢⊥≤ 𝛼 , as observed by Pierce (1997). Simply extending the measure function with size Ψ (⊥) = 1 will not work. For type variables, the measure function will recursively look up its bound in the context, and add one to the measure of its 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 can construct derivations of rule S-equivall that have a larger measure in the premise than that of the conclusion, which makes the decidability proof fail with the current measure. For example, consider the following subtyping derivation:

If we follow the measure function defined in §4.3, the measure for the third premise is:

while the measure for the goal is

size𝛼 ↦→1 , 𝛽 ↦→2 (∀( 𝛾 ≤ 𝛼 ) . 𝐴 ) + size𝛼 ↦→1 , 𝛽 ↦→2(∀( 𝛾 ≤ 𝛽 ) . 𝐵 )

↩ → size𝛼 ↦→1 , 𝛽 ↦→2 , 𝛾 ↦→2 ( 𝐴 ) + size𝛼 ↦→1 , 𝛽 ↦→2 , 𝛾 ↦→3 ( 𝐵 )

--- end of page.page_number=42 ---

Journal of Functional Programming

which can be less than the measure of the premise since 𝛾 is assigned a smaller measure in the goal. A similar issue arises when a variable is lower bounded by ⊤, making it equivalent to top types but with a different measure.

This issue can be resolved by replacing all the types whose supertype is ⊥ with ⊥, and all the types whose subtype is ⊤ with ⊤ before computing the measure. That way, the subtyping relation 𝛼 ≤⊥ , 𝛽 ≤ 𝛼 ⊢∀( 𝛾 ≤ 𝛼 ) . 𝐴 ≤∀( 𝛾 ≤ 𝛽 ) . 𝐵 becomes

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, as can be seen in Figure 10. The new bindings 𝛼 ↦→⊥ and 𝛼 ↦→⊤ are used to store the measure of variables or indicate them as upper bounded by ⊥ or lower bounded by ⊤. Figure 10 shows the measures needed for the decidability of 𝐹 ≤≥ [𝜇][∧][.][The][primary][measure] function is size Ψ ( 𝐴 ). The main changes are in the cases for bounded quantification where we now use isTop and isBot functions to detect whether the bounds are, respectively, equivalent to top or bottom. The isTop and isBot functions 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. The example above will now be resolved by the new measure function as follows:

↩ → size𝛼 ↦→⊥ , 𝛽 ↦→⊥ , 𝛾 ↦→⊥( 𝐴 ) + size𝛼 ↦→⊥ , 𝛽 ↦→⊥ , 𝛾 ↦→⊥ ( 𝐵 ) since isBot𝛼 ↦→⊥ , 𝛽 ↦→⊥ ( 𝛼 ) = true and isBot𝛼 ↦→⊥ , 𝛽 ↦→⊥( 𝛽 ) = true

In this way, we retain the important property that equivalent types have the same measure.

Lemma 5.12 . If Γ ⊢ 𝐴 ≤ 𝐵 and Γ ⊢ 𝐵 ≤ 𝐴 then size𝑒𝑣𝑎𝑙 (Γ) ( 𝐴 ) = size𝑒𝑣𝑎𝑙 (Γ) ( 𝐵 ) in 𝐹 ≤≥ [𝜇][∧][.]

Note that in the proof of Lemma 5.12, in the case of intersection types, we make use of the compatibility relation 𝐴 # 𝐵 to ensure that any equivalent types have the same measure. Without the compatibility restriction, the labels may be duplicated within the intersection type, which will lead to a different measure for equivalent types. By limiting compatible types to be single-field records and their intersections only, we also rule out the occurrence of ⊤ in intersection types, which will cause the same problem. With the new measure function, we can prove the decidability of subtyping and typing in 𝐹 ≤≥ [𝜇][∧][.]

Theorem 5.13 (Decidability of 𝐹 ≤≥ [𝜇][∧][subtyping)] [.][Γ][ ⊢] [𝐴][≤] [𝐵][is decidable in] [ 𝐹] ≤≥ [𝜇][∧][.] Theorem 5.14 (Decidability of 𝐹 ≤≥ [𝜇][∧][typing)] [.][Γ][ ⊢] [𝑒][:] [ 𝐴][is decidable in] [ 𝐹] ≤≥ [𝜇][∧][.]

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 the minimum type of an 𝐹 ≤ term. We have defined the algorithmic typing rules for 𝐹[𝜇][∧][proved][the][completeness][of][the][algorithmic][typing][rules][in][§][5.2][.][With][the] ≤≥[and] algorithmic typing rules, conservativity for 𝐹 ≤≥ [𝜇][∧][is straightforward.]

Theorem 5.15 (Conservativity for 𝐹 ≤≥ [𝜇][∧][)] [.][If][ Γ][,] [𝐴][and] [ 𝑒][are well-formed in] [𝐹][≤][, namely (1)] ⊢ 𝐹 Γ (2) Γ ⊢ 𝐹 𝐴 and (3) ⊢ 𝐹 𝑒 , then Γ ⊢ 𝐹 𝑒 : 𝐴 if and only if Γ ⊢ 𝑒 : 𝐴 .

--- end of page.page_number=43 ---

Recursive Subtyping for All

Ψ := · | Ψ , 𝛼 ↦→ 𝑖 | Ψ , 𝛼 ↦→⊥| Ψ , 𝛼 ↦→⊤

Fig. 10: The measures for the decidability of 𝐹 ≤≥ [𝜇][∧][.]

6 Coq Proofs

We develop and verify our formalization in Coq 8.13 (The Coq Development Team, 2021), and use Metalib to formalize variables and binders using the locally nameless representation (Aydemir et al., 2008).

The Coq formalization is available online4. The directory “kernel f sub m ain” includes all definitions and proofs for kernel 𝐹 ≤ [𝜇][described][in][Section][3][,][while][the][directory] “full f sub m ain” includes the full 𝐹[𝜇][Definition][and][proofs][for] [𝐹][𝜇][∧] ≤[variant.] ≤≥[described] in Section 5 are in the “kernel f sub e xt” directory. Each directory can be checked independently, and the dependency of the proofs follows a sequential order in each directory.

4 https://github.com/juda/Recursive-Subtyping-for-All/tree/main/JFP

--- end of page.page_number=44 ---

Journal of Functional Programming

Table 2: Paper-to-proofs correspondence guide for kernel 𝐹 ≤ [𝜇][(in kernel] f sub m ain/ directory).

Defnition	File	Name in	Coq	Notation
Types (Figure1)	Rules.v	typ
Expressions (Figure1)	Rules.v	exp
Values (Figure1)	Rules.v	value
Contexts (Figure1)	Rules.v	env
Well-formed Type (Figure2)	Rules.v	WF E A		Γ⊢_𝐴_
Subtyping (Figure2)	Rules.v	sub E A B		Γ⊢_𝐴_≤_𝐵_
Typing (Figure3)	Rules.v	typing E	e A	Γ⊢_𝑒_:𝐴
Reduction (Figure3)	Rules.v	step e1 e2		_𝑒_1_↩_→_𝑒_2
Upper Exposure (Figure5)	AlgoTyping.v	exposure E A B		Γ⊢_𝐴_⇑_𝐵_
Lower Exposure (Figure5)	AlgoTyping.v	exposure2 E B A		Γ⊢_𝐴_⇓_𝐵_
Algorithmic Typing (Figure5)	AlgoTyping.v	typing E	e A	Γ⊢_𝑎𝑒_:𝐴
Measure (§4.3)	Decidability.v	bindings	rec G E n A	_size_Ψ(𝐴)
Context Measure(§4.3)	Decidability.v	mk benv E		eval(Γ)

Table 3: Paper-to-proofs correspondence guide for full 𝐹 ≤ [𝜇][(in][full] f sub m ain/ directory). Definitions that are the same as kernel 𝐹[𝜇] ≤[are omitted.]

Defnition	File	Name in	Name in	Coq	Notation
Subtyping (§3.2)	Rules.v	sub	E A	B	Γ⊢_𝐴_≤_𝐵_
Related contexts	UnfoldingEquiv.v	sub	env	ext E X C D E1 E2	Γ�Γ_𝜇_
(Defnition4.7)

6.1 Definitions

All three systems share a similar structure for definitions: the files Rules.v contains the core definitions for the calculus, and AlgoTyping.v contains the algorithmic rules for typing. Tables 2, 3 and 4 shows the correspondence between the paper definitions and the Coq formalization. The formalization mainly follows the definitions in the paper except for some technical details. One difference to note is that throughout the paper, we use only substitution to represent unfolding of a recursive type, application of universal quantification and function abstraction. In the Coq proof, due to the use of the locally nameless representation, we also make use of the opening operation on pre-terms (Aydemir et al., 2008). We also merge several rules for exposure and typing record expressions in the paper, for readability.

6.2 Lemmas and Theorems

Tables 5, 6 and 7 show the correspondence of lemmas and theorems between the paper and the Coq formalization. We provide the file location and theorem name in Coq for each lemma and theorem in the paper, and include a brief description for each of them.

--- end of page.page_number=45 ---

Recursive Subtyping for All

Table 4: Paper-to-proofs correspondence guide for 𝐹 ≤≥ [𝜇][∧][(in kernel] f sub e xt/ directory).

Table 4: Paper-to-proofs corresp	ondence guide fo	r_𝐹_ ≤≥(in	ernel fsub ex	t/ directory).
Defnition	File	Name in	Coq	Notation
Types (§5.1)	Rules.v	typ
Expressions (§5.1)	Rules.v	exp
Values (§5.1)	Rules.v	value
Contexts (§5.1)	Rules.v	env
Compatible types (Figure6)	Rules.v	Compatible A B		𝐴#𝐵
Well-formed Type (Figure6)	Rules.v	WF E A		Γ⊢_𝐴_
Subtyping (Figure6)	Rules.v	sub E A B		Γ⊢_𝐴_≤_𝐵_
Typing (Figure7)	Rules.v	typing E	e A	Γ⊢_𝑒_:𝐴
Reduction (Figure7)	Rules.v	step e1 e2		_𝑒_1_↩_→_𝑒_2
Algorithmic Typing (Figure8)	AlgoTyping.v	typing E	e A	Γ⊢_𝑎𝑒_:𝐴
Upper Exposure (Figure9)	AlgoTyping.v	exposure	E A B	Γ⊢_𝐴_⇑_𝐵_
Lower Exposure (Figure9)	AlgoTyping.v	exposure2 E B A		Γ⊢_𝐴_⇓_𝐵_
Record Exposure (Figure9)	AlgoTyping.v	exposure	iE A l B	Γ⊢_𝐴_⇒_𝑙𝐵_
Measure(Figure10)	Decidability.v	bindings	rec G E n A	_size_Ψ(𝐴)

Throughout the paper, we have already reviewed some of the closest related work in detail. In this section, we discuss other related work.

7.1 Bounded Quantification, Recursive Types and Object Encodings

Bounded quantification was first introduced by Cardelli and Wegner (1985) in the language Fun, where their kernel Fun calculus corresponds 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 is contravariant. Although full 𝐹 ≤ is powerful, subtyping 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 Jeffrey (2001). Unfortunately, as Table 1 shows, such combinations are not painless, and even the successful combinations require significant changes for the subtyping rules. Ghelli (1993) illustrates how the combination of equi-recursive subtyping and full 𝐹 ≤ significantly alters the expressiveness of the subtyping relation. Specifically, he shows that there exist such subtyping relations 𝐴 ≰ 𝐴[′] that do not hold in full 𝐹 ≤, but are derivable when equi-recursive subtyping is added, by finding an intermediate type 𝐵 which contains equi-recursive types such that 𝐴 ≤ 𝐵 and 𝐵 ≤ 𝐴[′] . In Colazzo and Ghelli (2005)’s work, there is no independent universal type, and the shape of recursive types is either 𝜇𝛼. ∀( 𝑥 ≤ 𝐴 ) . 𝐵 or 𝜇𝛼. 𝐴 → 𝐵 . The recursive variables and universal variables are distinct, resulting in changes in environments and subtyping rules. For example, the subtyping environment is defined as Π := · | Π , ( 𝑥, 𝑦 ) ≤( 𝐴, 𝐵 ) | Π , ( 𝛼 = 𝐴, 𝛽 = 𝐵 ), and the rule S-vartrans rule of 𝐹 ≤ is changed to:

--- end of page.page_number=46 ---

Journal of Functional Programming

Table 5: Descriptions for the proof scripts for kernel 𝐹 ≤ [𝜇][(in kernel] f sub m ain/ directory).

Table 5: Descrip	tions for the proof scripts for	ernel_𝐹_ ≤(in kernel	fsub main/ directory).
Theorems	Description	Files	Name in Coq
Lemma3.1	Regularity of subtyping	Refexivity.v	sub regular
Lemma3.2	Narrowing	Transitivity.v	sub narrowing
Theorem3.3	Refexivity	Refexivity.v	Refexivity
Theorem3.4	Transitivity	Transitivity.v	sub transitivity
Lemma3.5	Unfolding lemma	Unfolding.v	unfolding lemma
Lemma3.6	Structural unfolding	Preservation.v	structural unfolding
			lemma general
Theorem3.7	Preservation	Preservation.v	preservation
Theorem3.8	Progress	Progress.v	progress
Theorem3.9	Algo-typing soundness	AlgoTyping.v	typing algo sound
Theorem3.10	Algo-typing completeness	AlgoTyping.v	minimum typing
Lemma4.2	Generalized unfolding	Unfolding.v	sub generalize
	lemma for kernel 𝐹𝜇 ≤in		intensive
	Zhou et al. (2023)
Lemma4.3	Substitution inversion	Unfolding.v	subst reverse equiv
Lemma4.10	Subtyping conservativity	Conservativity.v	sub conserv
Lemma4.11	Antisymmetry of kernel_𝐹_≤	Conservativity.v	sub antisym
	subtyping
Lemma4.12	Algo-typing conservativity	Conservativity.v	typing algo conserv
Theorem4.13	Typing conservativity	Conservativity.v	typing conserv
Theorem4.15	Decidability of subtyping	Decidability.v	decidability
Theorem4.16	Decidability of typing	DecidabilityTy.v	decidable typing
Lemma4.17	Equivalent measure	Decidability.v	equiv measure

The algorithm proposed by Jeffrey (2001) is also complex, and requires major changes. Both recursive variables and the subtyping algorithm are labeled with polarity modes, and the implementation of 𝛼 -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 benefit that we can largely reuse the existing metatheory of the original 𝐹 ≤, and it also enables our conservativity result. While it is plausible that Jeffrey (2001)’s or Colazzo and Ghelli (2005)’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 and Wegner (1985). Existential types can be encoded by universal types, thus we can obtain a form of bounded existentials for free in 𝐹 ≤ (Cardelli and Wegner, 1985). Another important extension is F-bounded quantification, firstly proposed by Canning et al. (1989), then studied by Baldan et al. (1999) in terms of the basic theory. In F-bounded quantification, the bounded variables are allowed to appear in the bound, denoted as ∀( 𝛼 ≤ 𝐹 [ 𝛼 ]) . 𝐵 . We can encode polymorphic binary methods (Bruce et al., 1995) and methods that have recursive types in their signatures with F-bounded quantification. However, as we discussed in §2.2, for

--- end of page.page_number=47 ---

Recursive Subtyping for All

Table 6: Descriptions for the proof scripts for full 𝐹 ≤ [𝜇][(in full] f sub m ain/ directory).

Table 6: Desc	riptions for the proof scripts	or full_𝐹_ ≤(in full fs	ub main/ directory).
Theorems	Description	Files	Name in Coq
Lemma3.1	Regularity of subtyping	Refexivity.v	sub regular
Lemma3.2	Narrowing	Transitivity.v	sub narrowing
Theorem3.3	Refexivity	Refexivity.v	Refexivity
Theorem3.4	Transitivity	Transitivity.v	sub transitivity
Lemma3.5	Unfolding lemma	UnfoldingEquiv.v	unfolding lemma
Lemma3.6	Structural unfolding	Preservation.v	structural unfolding
			lemma general
Theorem3.7	Preservation	Preservation.v	preservation
Theorem3.8	Progress	Progress.v	progress
Theorem3.9	Algo-typing soundness	AlgoTyping.v	typing algo sound
Theorem3.10	Minimum typing	AlgoTyping.v	minimum typing
Lemma4.8	Related context inversion	UnfoldingEquiv.v	sub env ext sem
Lemma4.9	Generalized unfolding	UnfoldingEquiv.v	sub generalize
	lemma for full_𝐹𝜇_ ≤		intensive
Lemma4.10	Subtyping conservativity	Conservativity.v	sub conserv
Lemma4.12	Algorithmic typing con-	Conservativity.v	typing algo conserv
	servativity
Theorem4.13	Typingconservativity	Conservativity.v	typing conserv

subtyping statements to satisfy the bound 𝛼 ≤ 𝐹 [ 𝛼 ], they must be interpreted using equirecursive subtyping, as F-bounds are normally records, and an iso-recursive type cannot be the subtype of a record type. F-bounded quantification is appealing because it can even deal with binary methods, where recursive types appear in negative positions. For example, with F-bounded quantification we can model bounds such as 𝛼 ≤{ 𝑥 : Int , eq : 𝛼 → 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 quantification (such as translate) in 𝐹 ≤ [𝜇][,][we][can][only][model][a] restricted form of negative F-bounded quantification. For instance in 𝐹 ≤ [𝜇][we][can][have] the bound 𝛼 ≤ 𝜇 P . { 𝑥 : Int , eq : P → Bool} and we can instantiate 𝛼 with 𝑃 (where 𝑃 = 𝜇 P . { 𝑥 : Int , eq : P → Bool}). However, we would not be able to instantiate 𝛼 with some types that have extra fields, such as 𝜇 P’ . { 𝑥 : Int , 𝑦 : Int , eq : P’ → Bool}. In contrast, F-bounded quantification allows such forms of instantiation. Nevertheless, given the overlap between some of the applications of iso-recursive types in 𝐹 ≤ [𝜇][and F-bounded quantifica-] tion, we believe that it is worthwhile to investigate whether F-bounded quantification can be avoided to deal with general binary methods.

F-bounded quantification offers an elegant method for encoding objects that possess binary methods. When not seeking to fully encode binary methods, other object encodings are also available. Recursive records can encode objects (Bruce et al., 1999; Cook et al., 1989; Canning et al., 1989). Alternatively, existential types can also be used to encode objects (Pierce and Turner, 1994), or they can be employed together with recursive types (Bruce, 1994). Pierce and Turner (1994)’s object encoding using existential types is notable in that it requires only 𝐹 ≤, and does not employ recursive types. The ORBE

--- end of page.page_number=48 ---

Journal of Functional Programming

Table 7: Descriptions for the proof scripts for 𝐹 ≤≥ [𝜇][∧][(in kernel] f sub e xt/ directory).

Table 7: Des	criptions for the	proof scripts	for_𝐹_ ≤≥(in kernel fs	ub ext/ directory).
Theorems	Description		Files	Name in Coq
Lemma5.1	Regularity of subtyping		Refexivity.v	sub regular
Theorem5.2	Refexivity		Refexivity.v	Refexivity
Theorem5.3	Transitivity		Transitivity.v	sub transitivity
Theorem5.4	Preservation		Preservation.v	preservation
Theorem5.5	Progress		Progress.v	progress
Lemma5.6	Record exposure		AlgoTyping.v	exposure i sound
				exposure i ex
Theorem5.7	Algo-typing soundness		AlgoTyping.v	typing algo sound
Theorem5.8	Algo-typing completeness		AlgoTyping.v	minimum typing
Lemma5.9	Unfolding lemma		UnfoldingEquiv.v	unfolding lemma
Lemma5.11	Structural	Unfolding	Preservation.v	structural unfolding
	lemma			lemma general
Lemma5.12	Equivalent measure		Decidability.v	equiv measure
Theorem5.13	Decidability of	subtyping	Decidability.v	decidability
Theorem5.14	Decidability of	typing	DecidabilityTy.v	decidable typing
Theorem5.15	Conservativity		Conservativity.v	typing conserv

encoding (Abadi et al., 1996), as we discussed in §2.2, consists of recursive types, bounded existential quantification, records, and the structural unfolding rule. As Bruce et al. (1999) observe, the ORBE encoding requires full 𝐹 ≤ for the bounded quantification 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 different object encodings. Our 𝐹 ≤ [𝜇] calculus could act as a target for all those existing object encodings discussed above. To our best knowledge, a complete formalization of 𝐹 ≤ with recursive types, featuring desirable properties such as type soundness and conservativity, was not available at the time. Our work contributes to the validation of these encodings by offering a complete formalization of 𝐹 ≤ with recursive types, along with several desirable properties.

7.2 Dependent Object Types

The renewed interest in languages featuring bounded quantification and recursive types has been reignited recently within the research community, following the introduction of the dependent object types (DOT) calculus (Rompf and Amin, 2016). DOT is now the foundation of Scala 3 (EPFL, 2021). 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 𝐹 ≤. DOT implements a generalized form of bounded quantification along with recursive types. This generalized form encompasses both upper and lower bounded quantification. Furthermore, DOT facilitates path selection that simultaneously supports upper and lower bounds. Additionally, DOT incorporates intersection types (Pottinger, 1980; Coppo et al., 1981; Barbanera et al., 1995) for typing objects. A distinctive characteristic of DOT is its use of path-dependent types (Amin et al., 2014). With path-dependent types,

--- end of page.page_number=49 ---

Recursive Subtyping for All

the treatment of recursive types is different from our calculus 𝐹 ≤≥ [𝜇][∧][. In DOT, recursive types] are introduced using recursive self types: { 𝑧 ⇒ 𝑇[𝑧] }. The variable 𝑧 is a term variable. Thus a recursive self type provides a limited form of dependent types, modeling a dependentlytyped fixpoint operator. In contrast, in 𝐹 ≤≥ [𝜇][∧][,][the][variable] [𝛼][of][a][recursive][type] [𝜇𝛼. 𝐴][is][a] type variable. In 𝐹 ≤≥ [𝜇][∧][, the type of objects is similar to that in DOT: we employ intersections] of the types of all the fields, and we require that the labels are disjoint. If the object uses recursive types, then we use a fold around the term.

Previous attempts to prove the undecidability of DOT reduced the problem to the undecidability problem in 𝐹 ≤, relying on a translation from 𝐹 ≤ to types in DOT (Rompf and Amin, 2016). However, as Hu and Lhot´ak (2020) later observed, the translation is not conservative. For example, in 𝐹 ≤, ⊤→⊤≤∀( 𝛼 ≤⊤) . ⊤ is not a valid subtyping statement because function types and universal types are not comparable. However, after translating them into DOT, the statement becomes ∀( 𝛼 : ⊤) . ⊤≤∀( 𝛼 : {⊤ .. ⊤}) . ⊤, in which {⊤ .. ⊤} indicates that 𝛼 is both upper and lower bounded by ⊤. This statement is valid in DOT variants that allow full or equivalent subtyping for bounded quantification, which breaks the conservativity from 𝐹 ≤ to DOT. Nevertheless, Hu and Lhot´ak (2020) showed that the undecidability of DOT can be reduced to an undecidable fragment 𝐹 ≤[−][of][full] [𝐹][≤][,][that] excludes the function types, and proved that DOT is undecidable.

There are two notable decidable variants of DOT: the strong kernel 𝐷 < : calculus from Hu and Lhot´ak (2020) and the Wyvern language by Mackay et al. (2020). These systems share features akin to 𝐹[𝜇][∧] ≤≥[, making comparisons worthwhile. As variants of DOT, both support] path-dependent types. The decidable variant by Hu and Lhot´ak (2020) selects specific features from DOT, including upper and lower bounds for path selection, and an equivalent subtyping quantifier for 𝐹 ≤, but it lacks recursive and intersection types. To handle the complexity of path types in proof of decidability, they define an algorithmic version of the subtyping rules, called stare-at subtyping, prove its equivalence to the declarative rules, and use a simple measure to show that the algorithmic rules terminate. The system developed by Mackay et al. (2020) shares several similarities with 𝐹 ≤≥ [𝜇][∧][, including the enforcement of] comparable constraints on bounds and the integration of a restricted version of intersection types for typing objects. However, it distinguishes itself by using equi-recursive types for recursion.

Reflecting on the complexity inherent in full intersection types, Mackay et al. (2020) also adopt a restricted form of these types to refine recursive objects. To ensure decidability, their methodology employs a kernel variant of 𝐹 ≤. As for the proof of decidability, Mackay et al. (2020) define type graphs, a graphical representation of types and type declarations, along with the dependency information between them. They provide a general algorithm for checking type graph subtyping, and show that in the restricted system, all types are homomorphic to type graphs that obey the material/shape separation property, which ensures that the subtyping algorithm terminates. In contrast, the decidability proof for 𝐹[𝜇][∧] ≤≥[does not rely on alternative subtyping rules or type representations, and is solely] based on measures. Both decidable systems in DOT incorporate top and bottom types and have been demonstrated to be reflexive, similarly to 𝐹 ≤≥ [𝜇][∧][. However, one of the limitations] for DOT is that transitivity elimination is not possible (Rompf and Amin, 2016), and even the two decidable fragments of DOT lack transitivity (Hu and Lhot´ak, 2020; Mackay et al., 2020). In contrast, in 𝐹 ≤≥ [𝜇][∧][transitivity can be derived from the subtyping rules.]

--- end of page.page_number=50 ---

Journal of Functional Programming

Table 8: Comparison 𝐹 ≤≥ [𝜇][∧][with DOT and its variants.]

	_𝐹𝜇_∧ ≤≥	Rompf and Amin (2016)	Hu and Lhot´ak (2020)	Mackay et al. (2020)
Path-dependent Types Bounded Quantifcation Recursive Types Intersection Types Quantifer Subtyping	× _𝛼_≤_𝐴_or 𝛼_≥_𝐴 iso limited equiv_𝐹_≤	✓ 𝐴_≤_𝛼_≤_𝐵 equi ✓ full_𝐹_≤	✓ 𝐴_≤_𝛼_≤_𝐵 × × equiv_𝐹_≤	✓ _𝛼_≤_𝐴_or 𝛼_≥_𝐴 equi limited kernel_𝐹_≤
Conservativity Refexivity Transitivity Decidability	✓ ✓ ✓ measures	× ✓ built-in ×	× ✓ × algo rules	× ✓ × typegraphs

While 𝐹[𝜇][∧][not][have][all][the][features][of][DOT,][our][results][can][potentially][help][in] ≤≥[does] research in that area, where the decidable fragments of DOT lack important properties such as transitivity. In addition 𝐹 ≤≥ [𝜇][∧][preserves][the][conservativity][over][kernel] [𝐹][≤][,][while][DOT] does not. Table 8 presents a comparative analysis of the four calculi.

7.3 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-defined datatype declarations. The first variant has user-defined subtyping declarations between datatypes, and can be viewed as having a form of nominal subtyping. The second variant allows structural subtyping among the datatypes.

One advantage of employing user-defined datatypes is that it is simple to deal with formally, and that it allows mutually recursive datatype definitions easily. However, they do not support conventional recursive types of the form 𝜇𝛼. 𝐴 as we do in 𝐹 ≤ [𝜇][. Moreover, they] do not consider lower bounded quantification which, as argued in §2.2, seems to be quite useful in a system targeting algebraic datatypes.

More recently, Rossberg (2023) proposed another calculus with a similar idea of using declared subtyping for recursive types, aiming at providing better and more efficient support for mutually recursive datatypes in type-safe low-level languages like Wasm. In their work, recursive types take the form 𝜇 ⟨ 𝛼 1 ≤ 𝐴 1 , 𝛼 2 ≤ 𝐴 2⟩ . 𝐵 , where the declared bound 𝐴 2 can refer to 𝛼 1 so that two mutually recursive types can be defined at once. This avoids the polynomial explosion of encoding mutual recursion using single recursion `a la Beki´c’s Lemma (Beki´c, 2005). However, to deal with type bounds in the 𝜇 -operator they need to employ higher-order subtyping (Pierce and Steffen, 1997).

--- end of page.page_number=51 ---

Recursive Subtyping for All

There has been some work integrating ML datatypes and OO classes (Bourdoncle and Merz, 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 of intermediate languages that have complex constructs such as classes or datatypes. In contrast, we develop 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 inheritance on datatypes, improving our understanding on the relation between categorical datatypes and object 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 for solving the Expression Problem (Wadler, 1998). However, as we mentioned in §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 quantification with higher kinds. In §2.2, we showed that first-order lower bounded quantification in 𝐹 ≤≥ [𝜇][∧][,][together][with][the][structural] folding rule enables such encodings. As for encodings of objects, our work is helpful to further validate such encodings formally.

8 Conclusion

Recursive types and bounded quantification play a significant role in various programming languages. While these features have been extensively studied individually, their combined interaction has remained a challenging problem for a long time. Our 𝐹 ≤ [𝜇][calculus demon-] strates a method for integrating iso-recursive types with two variations of 𝐹 ≤. We achieve a transitive and decidable subtyping relation for the kernel variant, and both calculi maintain conservativity over 𝐹 ≤ and are type sound. 𝐹 ≤ [𝜇][and] [𝐹] ≤≥ [𝜇][∧][could provide a theoretical basis] for object encodings and subtyping in algebraic data types. In particular, the full 𝐹 ≤ [𝜇][we] have studied in this paper provides a foundation for the ORBE object encoding (Abadi et al., 1996). Recently, there has been a renewed interest in recursive types and bounded quantification, sparked by the DOT calculus. Our research helps in identifying calculi that include most features found in DOT, while preserving properties such as subtyping’s decidability and transitivity, or even conservativity over 𝐹 ≤. Exploring extensions of 𝐹 ≤ [𝜇][to include more] features from DOT constitutes an interesting direction for future research.

Conflicts of Interest

None

References

Abadi, M., Cardelli, L. & Viswanathan, R. (1996) An interpretation of objects and object types. Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA. Association for Computing Machinery. pp. 396–409.

Abadi, M. & Fiore, M. P. (1996) Syntactic considerations on recursive types. Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. IEEE. pp. 242–252.

--- end of page.page_number=52 ---

Journal of Functional Programming

Amadio, R. M. & Cardelli, L. (1993) Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS) . 15 (4), 575–631.

Amin, N. & Rompf, T. (2017) Type soundness proofs with definitional interpreters. Proceedings of

the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. pp. 666–679.

Amin, N., Rompf, T. & Odersky, M. (2014) Foundations of path-dependent types. Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications. Portland Oregon USA. ACM. pp. 233–249.

Aydemir, B., Chargu´eraud, A., Pierce, B. C., Pollack, R. & Weirich, S. (2008) Engineering formal metatheory. ACM SIGPLAN Notices . 43 (1), 3–15.

Backes, M., Hrit¸cu, C. & Maffei, M. (2014) Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations . 22 (2), 301–353.

Baldan, P., Ghelli, G. & Raffaet`a, A. (1999) Basic Theory of F-Bounded Quantification. Information and Computation . 153 (2), 173–237.

Barbanera, F., Dezani-Ciancaglini, M. & de’Liguoro, U. (1995) Intersection and union types: Syntax and semantics. Information and Computation . 119 (2), 202–230.

Beki´c, H. (2005) Definable operations in general algebras, and the theory of automata and flowcharts. Programming Languages and Their Definition: H. Bekiˇc (1936–1982) . pp. 30–55.

Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A. D. & Maffeis, S. (2011) Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS) . 33 (2), 1–45.

B¨ohm, C. & Berarducci, A. (1985) Automatic synthesis of typed Lambda-programs on term algebras. Theoretical Computer Science . 39 (2-3).

Bourdoncle, F. & Merz, S. (1997) Type checking higher-order polymorphic multi-methods. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 302–315.

Brandt, M. & Henglein, F. (1998) Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae . 33 (4), 309–338.

Bruce, K., Cardelli, L., Castagna, G., Group, H. O., Leavens, G. T. & Pierce, B. C. (1995) On binary methods. Theory and Practice of Object Systems . 1 (3), 221–242.

Bruce, K. B. (1994) A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming . 4 (2), 127–206.

Bruce, K. B., Cardelli, L. & Pierce, B. C. (1999) Comparing Object Encodings. Information and Computation . 155 (1), 108–133.

Canning, P., Cook, W., Hill, W., Olthoff, W. & Mitchell, J. C. (1989) F-bounded polymorphism for object-oriented programming. Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture. Imperial College, London, United Kingdom.

Canning, P. S., Cook, W. R., Hill, W. L. & Olthoff, W. G. (1989) Interfaces for strongly-typed object-oriented programming. ACM SIGPLAN Notices . 24 (10), 457–467.

Cardelli, L. (1985) Amber, combinators and functional programming languages. Proc. of the 13th Summer School of the LITP, Le Val D’Ajol, Vosges (France).

Cardelli, L., Martini, S., Mitchell, J. & Scedrov, A. (1994) An Extension of System F with Subtyping. Information and Computation . 109 (1-2), 4–56.

Cardelli, L. & Wegner, P. (1985) On understanding types, data abstraction, and polymorphism. ACM Computing Surveys . 17 , 471–522.

Castagna, G. & Pierce, B. C. (1994) Decidable bounded quantification. Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA. Association for Computing Machinery. pp. 151–162.

Church, A. (1932) A set of postulates for the foundation of logic. Annals of Mathematics . 33 (2), 346–366.

Colazzo, D. & Ghelli, G. (2005) Subtyping recursion and parametric polymorphism in kernel Fun. Information and Computation . 198 (2), 71–147.

Cook, W. R., Hill, W. & Canning, P. S. (1989) Inheritance is not subtyping. Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for

--- end of page.page_number=53 ---

Recursive Subtyping for All

Computing Machinery.

Coppo, M., Dezani-Ciancaglini, M. & Venneri, B. (1981) Functional characters of solvable terms. Mathematical Logic Quarterly . 27 (2-6), 45–58.

Curien, P.-L. & Ghelli, G. (1992) Coherence of subsumption, minimum typing and type-checking in F≤ . Mathematical structures in computer science . 2 (1), 55–91.

Dunfield, J. (2012) Elaborating intersection and union types. ACM SIGPLAN Notices . 47 (9), 17–28. EPFL. (2021) Scala 3. available at https://www.scala-lang.org/.

Gapeyev, V., Levin, M. & Pierce, B. C. (2003) Recursive subtyping revealed. Journal of Functional Programming . 12 (6), 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).

Ghelli, G. (1993) Recursive types are not conservative over F≤. International Conference on Typed Lambda Calculi and Applications. Springer. pp. 146–162.

Haskell Development Team. (1990) Haskell. available at https://www.haskell.org/.

Hosoya, H., Pierce, B. C., Turner, D. N. et al. . (1998) Datatypes and subtyping. Unpublished manuscript .

Hu, J. & Lhot´ak, O. (2020) Undecidability of D < : And Its Decidable Fragments. Proceedings of the ACM on Programming Languages . 4 (POPL), 1–30.

INRIA. (1987) OCaml. available at https://ocaml.org/.

Jeffrey, A. (2001) A symbolic labelled transition system for coinductive subtyping of F 𝜇 ≤ types. 2001 IEEE Conference on Logic and Computer Science (LICS 2001).

Ligatti, J., Blackburn, J. & Nachtigal, M. (2017) On subtyping-relation completeness, with an application to iso-recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS) . 39 (1), 1–36.

Mackay, J., Potanin, A., Aldrich, J. & Groves, L. (2020) Decidable subtyping for path dependent types. Proceedings of the ACM on Programming Languages . 4 (POPL), 1–27.
Millstein, T., Bleckner, C. & Chambers, C. (2004) Modular typechecking for hierarchically extensible datatypes and functions. ACM Transactions on Programming Languages and Systems (TOPLAS) . 26 (5), 836–889.

Morris, J. H. (1968) Lambda Calculus Models of Programming Languages . Ph.D. thesis.

Oliveira, B. C. d. S. (2009) Modular visitor components. European Conference on Object-Oriented Programming. Springer. pp. 269–293.

Oliveira, B. C. d. S., Cui, S. & Rehman, B. (2020) The duality of subtyping. 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference).

Parigot, M. (1992) Recursive programming with proofs. Theoretical Computer Science . 94 (2), 335– 356.
Pierce, B. & Steffen, M. (1997) Higher-order subtyping. Theoretical Computer Science . 176 (1), 235–282.
Pierce, B. C. (1994) Bounded quantification is undecidable. Information and Computation . 112 (1), 131–165.
Pierce, B. C. (1997) Bounded quantification with bottom. CSCI Technical Report 492. Computer Science Department, Indiana University.
Pierce, B. C. (2002) Types and Programming Languages . MIT press.
Pierce, B. C. & Turner, D. N. (1994) Simple type-theoretic foundations for object-oriented programming. Journal of functional programming . 4 (2), 207–247.
Poll, E. (1998) Subtyping and inheritance for categorical datatypes: Preliminary report (type theory and its applications to computer systems). Kyoto University Research Information Repository . 1023 , 112–125.
Pottinger, G. (1980) A type assignment for the strongly normalizable 𝜆 -terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism . pp. 561–577.
Reynolds, J. C. (1974) Towards a theory of type structure. Programming Symposium: Proceedings, Colloque Sur La Programmation Paris, April 9–11, 1974. Springer. pp. 408–425.

--- end of page.page_number=54 ---

Journal of Functional Programming

Reynolds, J. C. (1988) Preliminary Design of the Programming Language Forsythe . Carnegie-Mellon University. Department of Computer Science.

Rompf, T. & Amin, N. (2016) Type soundness for dependent object types (DOT). Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. pp. 624–641.

Rossberg, A. (2023) Mutually iso-recursive subtyping. Proceedings of the ACM on Programming Languages . 7 (OOPSLA2), 347–373.

Sangiorgi, D. & Milner, R. (1992) The problem of “weak bisimulation up to”. CONCUR. pp. 32–46. Scott, D. (1962) A system of functional abstraction. Lectures delivered at University of California, Berkeley, California, USA, 1962/63.

The Coq Development Team. (2021) Coq. v8.13, available at https://coq.inria.fr.

Wadler, P. (1998) The expression problem. discussion on the Java Genericity mailing list.

Zhou, L. & Oliveira, B. C. d. S. (2025) QuickSub: Efficient Iso-Recursive Subtyping. Proceedings of the ACM on Programming Languages . 9 (POPL).

Zhou, L., Wan, Q. & Oliveira, B. C. d. S. (2024) Full Iso-Recursive Types. Proceedings of the ACM on Programming Languages . 8 (OOPSLA2), 278:192–278:221.

Zhou, L., Zhou, Y. & Oliveira, B. C. d. S. (2023) Recursive subtyping for all. Proceedings of the ACM on Programming Languages . 7 (POPL), 1396–1425.

Zhou, Y., Oliveira, B. C. d. S. & Fan, A. (2022) A calculus with recursive types, record concatenation

and subtyping. Asian Symposium on Programming Languages and Systems. Springer. pp. 175–195.

Zhou, Y., Oliveira, B. C. d. S. & Zhao, J. (2020) Revisiting iso-recursive subtyping. Proceedings of the ACM on Programming Languages . 4 (OOPSLA), 1–28.

Zhou, Y., Zhao, J. & Oliveira, B. C. d. S. (2022) Revisiting iso-recursive subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS) . 44 (4), 1–54.

--- end of page.page_number=55 ---

Tony's Wiki

Explorer

Recursive Subtyping for All

Recursive Subtyping for All

Metadata

Why this note exists

Extraction quality note

Technical landmarks detected automatically

Full converted paper text

Recursive Subtyping for All

LITAO ZHOU1 YAODA ZHOU1 QIANYONG WAN BRUNO C. D. S. OLIVEIRA

Abstract

1 Introduction

2 Overview

2.1 Bounded Quantification and Recursive Subtyping

kernelall.

2.2 Applications of Bounded Quantification and Recursive Types

}

∀(P ≤ Point) . P → P

function getXORBE(p: Point ORBE ) =

(unpack (unfold [Point ORBE ] p) as [ 𝛼 , o] in o.x[sel] (o.self) )

}

}

}

2.3 Key Ideas and Results

3 Bounded Quantification with Iso-Recursive Types

3.1 Kernel 𝐹 ≤ with Iso-recursive Subtyping

∀( 𝛼 ≤{ 𝑥 : nat , 𝑦 : nat}) .𝛼 → 𝛼 ≤∀( 𝛼 ≤{ 𝑦 : nat , 𝑥 : nat}) .𝛼 → 𝛼

3.2 Full 𝐹 ≤ with Iso-recursive Subtyping

3.3 Typing, Reduction and Type Soundness

Fig. 4: Structural unfolding derivation.

3.4 Algorithmic Typing

4 Metatheory of 𝐹 ≤ [𝜇]

4.1 Unfolding Lemma

4.2 Conservativity

4.3 Decidability

5 A Calculus with Lower and Upper Bounded Quantification

5.1 The 𝐹[𝜇][∧] ≤≥ [Calculus]

5.2 Algorithmic typing

5.3 Metatheory of 𝐹 ≤≥ [𝜇][∧]

6 Coq Proofs

6.1 Definitions

6.2 Lemmas and Theorems

7 Related Work

7.1 Bounded Quantification, Recursive Types and Object Encodings

7.2 Dependent Object Types

7.3 Algebraic Datatypes and Subtyping

8 Conclusion

Conflicts of Interest

References

Graph View

Table of Contents

Backlinks