QuickSub: Efficient Iso-Recursive Subtyping

Metadata

Title: QuickSub: Efficient Iso-Recursive Subtyping
Venue: POPL’25
Area: Iso-recursive subtyping
Source URL: https://i.cs.hku.hk/~bruno/papers/popl25_quicksub.pdf
Downloaded PDF: QuickSub-Efficient-Iso-Recursive-Subtyping.pdf
Extracted assets: _assets/QuickSub-Efficient-Iso-Recursive-Subtyping/
Pages: 32
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 1: QuickSub: Efficient Iso-Recursive Subtyping
line 11: CCS Concepts: • Theory of computation → Type theory ; • Software and its engineering → Object oriented languages .
line 13: Additional Key Words and Phrases: Recursive types, Subtyping, Algorithm
line 15: ACM Reference Format:
line 17: Litao Zhou and Bruno C. d. S. Oliveira. 2025. QuickSub: Efficient Iso-Recursive Subtyping. Proc. ACM Program. Lang. 9, POPL, Article 33 (January 2025), 32 pages. https://doi.org/10.1145/3704869
line 19: 1 Introduction
line 55: QuickSub: Efficient Iso-Recursive Subtyping
line 67: - An efficient algorithm for iso-recursive subtyping. We introduce QuickSub, a novel algorithm for iso-recursive subtyping that significantly improves efficiency over existing algorithmic formulations.
line 69: - Equivalence proof to the Amber rules. We prove that QuickSub is equivalent in expressive power to the well-known iso-recursive Amber rules.
line 73: - Extension to record types. We extend QuickSub to QuickSub[] that handles record subtyping, broadening the applicability and flexibility of the algorithm.
line 77: 2 Overview
line 79: This section provides background of existing approaches to iso-recursive subtyping, and their drawbacks in terms of efficiency. Then it introduces key ideas leading to QuickSub.
line 81: 2.1 Subtyping Iso-Recursive Types
line 96:
line 99: The subtyping rule for function types is contravariant in the argument type and covariant in the return type.
line 101: With iso-recursive subtyping, it is expected that if two recursive types are subtypes, then their unfoldings should also be subtypes, which can be expressed as follows:
line 119: At this point it is useful to introduce the concept of equivalent and strict subtyping, which will play an important role in QuickSub. By equivalent subtyping, we mean that two types are subtypes
line 125: QuickSub: Efficient Iso-Recursive Subtyping
line 134:
line 144:
line 150:
line 155: 2.2 Algorithmic Iso-Recursive Subtyping
line 157: There are several existing approaches that provide algorithms for iso-recursive subtyping. Next we give an overview of existing approaches and their issues in terms of efficiency.
line 175: For example, the derivation below shows an application of the Amber rules for subtyping the positive recursive subtyping example that we have seen before:
line 178:
line 184:
line 199: QuickSub: Efficient Iso-Recursive Subtyping
line 203: quantification [Zhou et al. 2023] with mechanized proofs in Coq. The nominal unfolding rules are:
line 206:
line 212:
line 216:
line 226:
line 243: 2.3 Key Ideas Towards an Efficient Algorithm
line 252:
line 260:
line 269: QuickSub: Efficient Iso-Recursive Subtyping
line 274:
line 277: Fig. 1. Illustration of negative recursive subtyping
line 284:
line 304:
line 307: Fig. 2. The QuickSub subtyping rules.
line 309: 3 Efficient Subtyping Algorithm
line 311: In this section, we work with a minimal set of types to explain the key idea of QuickSub. The syntax of types, as well as other constructs used in the subtyping algorithm, is:
line 315: 3.1 QuickSub Subtyping
line 327: QuickSub: Efficient Iso-Recursive Subtyping
line 336:
line 344:
line 363: Variable 𝛽 causes the subtyping statement fail, since it can appear negatively after unfolding the inner recursive type 𝜇𝛼. 𝛼 → 𝛽 twice. This can be seen from the following derivation in QuickSub:
line 391: QuickSub: Efficient Iso-Recursive Subtyping
line 401: 3.2 Correctness
line 419: Fig. 3. Weakly Positive Subtyping Rules.
line 423: To see why rule Posvar-rec needs the second condition, consider the following example:
line 426:
line 429: which will be rejected by both rules Posvar-recself and Posvar-rec, since 𝛽 ∈ FV( 𝛼 → 𝛽 ) and 𝛼 ∈+ 𝛼 → 𝛽 ≤ 𝛼 → 𝛽 is not derivable. Otherwise, unfolding the recursive type would lead to
line 432:
line 443: QuickSub: Efficient Iso-Recursive Subtyping
line 449: Theorem 3.1 (Relation to weakly positive restrictions (strict subtyping)) . If Ψ ⊢⊕ 𝐴 < 𝐵 , then
line 459: Theorem 3.2 (Relation to weakly positive restrictions (equivalence)) . If Ψ ⊢⊕ 𝐴 ≈ 𝑆 𝐵 , then
line 475: Theorem 3.3 (Relation to weakly positive restrictions (fresh variables)) . If Ψ ⊢⊕ 𝐴 ⪅ 𝐵 , then for any 𝛼 ∉ dom Ψ and any polarity ⊕[′] , 𝛼 ∈⊕[′] 𝐴 ≤ 𝐵 .
line 477: Soundness of QuickSub to weakly positive subtyping. We can now show that the QuickSub rules are sound with respect to the weakly positive subtyping rules.
line 479: Theorem 3.4 (Soundness of QuickSub to Weakly Positive Subtyping) . If Ψ ⊢⊕ 𝐴 ⪅ 𝐵 , then |Ψ| ⊢ 𝑝 𝐴 ≤ 𝐵 , where |Ψ| removes all the polarity annotations from the context Ψ.
line 483: Theorem 3.5 (QuickSub equivalence implies equality) . If Ψ ⊢⊕ 𝐴 ≈ 𝑆 𝐵 , then 𝐴 = 𝐵 .
line 485: Completeness of QuickSub to weakly positive subtyping. We wish to prove the following theorem to show that QuickSub is complete with respect to the weakly positive subtyping rules:
line 487: Theorem 3.6 (Completeness of QuickSub) . If · ⊢ 𝑝 𝐴 ≤ 𝐵 , then there exists ⪅, such that · ⊢+ 𝐴 ⪅ 𝐵 .
line 492:
line 504:
line 511: Fig. 4. Type soundness proof framework for QuickSub, indirectly
line 517: The generalized lemma is then stated as follows:
line 519: Lemma 3.8 (Generalized completeness of QuickSub) . If Γ ⊢ 𝑝 𝐴 ≤ 𝐵 , and there exists Ψ such that dom Γ = dom Ψ, and Ψ ∈⊕ 𝐴 ≤ 𝐵 , then there exists ⪅, such that Ψ ⊢+ 𝐴 ⪅ 𝐵 .
line 523: 3.3 Direct Proof of Type Soundness
line 533: QuickSub: Efficient Iso-Recursive Subtyping
line 549: Lemma 3.9 (Unfolding lemma) . If · ⊢+ 𝜇𝛼. 𝐴 ⪅ 𝜇𝛼. 𝐵 , then · ⊢+ 𝐴 [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] ⪅ 𝐵 [ 𝛼 ↦→ 𝜇𝛼. 𝐵 ]
line 562:
line 565: Fig. 5. Typing and Reduction Rules
line 568:
line 573: The unfolding lemma is proved as a corollary of the generalized lemma below:
line 575: Lemma 3.10 (Generalized unfolding lemma) . If Ψ2 ⊢⊕ 𝐶 ⪅1 𝐷 , then
line 587: QuickSub: Efficient Iso-Recursive Subtyping
line 595: Theorem 3.11 (Reflexivity) . For any closed type 𝐴 , there exists 𝑆 , such that · ⊢+ 𝐴 ≈ 𝑆 𝐴 .
line 599: Theorem 3.12 (Transitivity) . If Ψ ⊢⊕ 𝐴 ⪅1 𝐵 and Ψ ⊢⊕ 𝐵 ⪅2 𝐶 , then Ψ ⊢⊕ 𝐴 (⪅1 ◦ ⪅2) 𝐶 , where

Full converted paper text

QuickSub: Efficient Iso-Recursive Subtyping

LITAO ZHOU, University of Hong Kong, China

BRUNO C. D. S. OLIVEIRA, University of Hong Kong, China

Many programming languages need to check whether two recursive types are in a subtyping relation. Traditionally recursive types are modelled in two different ways: equi- or iso- recursive types. While efficient algorithms for subtyping equi-recursive types are well studied for simple type systems, efficient algorithms for iso-recursive subtyping remain understudied.

In this paper we present QuickSub: an efficient and simple to implement algorithm for iso-recursive subtyping. QuickSub has the same expressive power as the well-known iso-recursive Amber rules. The worst case complexity of QuickSub is 𝑂 ( 𝑛𝑚 ), where 𝑚 is the size of the type and 𝑛 is the number of recursive binders. However, in practice, the algorithm is nearly linear with the worst case being hard to reach. Consequently, in many common cases, QuickSub can be several times faster than alternative algorithms. We validate the efficiency of QuickSub with an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms. We prove the correctness of the algorithm and formalize a simple calculus with recursive subtyping and records. For this calculus we also show how type soundness can be proved using QuickSub. All the results have been formalized and proved in the Coq proof assistant.

CCS Concepts: • Theory of computation → Type theory ; • Software and its engineering → Object oriented languages .

Additional Key Words and Phrases: Recursive types, Subtyping, Algorithm

ACM Reference Format:

Litao Zhou and Bruno C. d. S. Oliveira. 2025. QuickSub: Efficient Iso-Recursive Subtyping. Proc. ACM Program. Lang. 9, POPL, Article 33 (January 2025), 32 pages. https://doi.org/10.1145/3704869

1 Introduction

There are two main approaches to model recursive types in type systems: equi-recursive types and iso-recursive types. Iso-recursive types [Crary et al. 1999] treat a recursive type and its unfolding as different types. The recursive type and its unfolding are related by inserting term level fold/unfold constructs. Equi-recursive types [Morris 1968] treat recursive types and their unfoldings as equal: 𝜇𝛼.𝐴 = [ 𝜇𝛼.𝐴 / 𝛼 ] 𝐴

since they represent the same infinite tree [Amadio and Cardelli 1993]. Equi-recursive equivalence is powerful and useful to type check many programs without requiring explicit fold and unfold annotations. This can be convenient for programming, since there is no need to change the term structure. In addition, equi-recursive subtyping is also well-studied [Amadio and Cardelli 1993].

While equi-recursive types look appealing, there are some important considerations when choosing whether to adopt them. The powerful form of equivalence or subtyping comes at a cost. As it is well-known from the literature [Brandt and Henglein 1998], equi-recursive equivalence and subtyping requires coinductive reasoning. Coinductive reasoning leads to complications in the metatheory, as well as to relatively high algorithmic complexity. Thus, there has been significant

Authors’ Contact Information: Litao Zhou, University of Hong Kong, Hong Kong, China, ltzhou@cs.hku.hk; Bruno C. d. S. Oliveira, University of Hong Kong, Hong Kong, China, bruno@cs.hku.hk.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:2

research effort on efficient algorithms for both equi-recursive subtyping [Gapeyev et al. 2002; Kozen et al. 1993] and equivalence [Cardone and Coppo 1991; Coppo 1985] for simple type systems. Gapeyev et al. presented an efficient algorithm for checking equi-recursive subtyping with at most 𝑂 ( 𝑛[2] ) recursive calls, where 𝑛 is the number of recursive binders. Kozen et al. reduced the subtyping problem to the problem of testing automata emptiness and achieved quadratic time complexity. Therefore, it can be said that efficient algorithms for equi-recursive subtyping have been foundationally well understood in the literature, despite the overall computational costs still being expensive.

Equi-recursive algorithms are also non-trivial to extend with more advanced type system features. For instance, the interaction between equi-recursive types and type constructors, which is necessary for modeling ML-style recursive modules [Crary et al. 1999], is complex: it is unknown whether type equivalence remains decidable in that setting. For another example, the combination of bounded quantification and equi-recursive subtyping introduces significant complications [Colazzo and Ghelli 2005; Ghelli 1993; Jeffrey 2001], and requires rather complex metatheory.

Iso-recursive types are less convenient but, on the other hand, they: 1) are easier to scale to more advanced features; 2) have comparatively simpler metatheory; and, 3) are perceived as having computationally less complex operations. The first two points are backed up by strong evidence in the literature. For instance, follow-up work on recursive modules has adopted iso-recursive types to obtain more practical module systems with decidable type equivalence [Dreyer 2005; Dreyer et al. 2001; Russo 2001], since the interaction of iso-recursive types and type constructors is simpler. The interaction between bounded quantification and iso-recursive typing is also simple, as illustrated by Zhou et al. [2023], leading to a natural extension of 𝐹< : [Cardelli and Wegner 1985] with iso-recursive types. In addition, 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].

The point about computational complexity (3) deserves more discussion. Since most formulations of iso-recursive types remain inductive , iso-recursive subtyping algorithms only have to deal with finite trees. Rossberg [2023] argues that is an important point to consider for performance sensitive applications as, in principle, it leads to more efficient implementations of equivalence and subtyping. Rossberg is motivated by the use of recursive types in WebAssembly (Wasm) and type-safe low-level languages in general. He argues that, in those performance sensitive settings, iso-recursive types are a significantly more attractive choice compared to equi-recursive types. His work presents an efficient formulation of declared iso-recursive types, which are adopted in practice by Wasm. This declared formulation of iso-recursive types is very efficient as it only requires subtyping to be checked at the declaration of recursive types.

Unlike equi-recursive types, efficient subtyping algorithms for iso-recursive types have received less attention in the literature. For traditional iso-recursive types the most well-known formulation of subtyping employs the Amber rules [Cardelli 1985, 1993]. In contrast to Rossberg’s more restrictive declared subtyping, the Amber rules follow a purely structural approach where a recursive type is related to any other recursive type with a compatible structure. Furthermore, the Amber rules are inductively defined, which, according to Rossberg, should be an advantage in obtaining an algorithmic formulation. However, a naive implementation of the Amber rules has exponential time complexity, which is worse than the complexity reported for the best-known algorithms for equi-recursive subtyping. The culprit for the cost of the Amber rules is the need for a built-in reflexivity rule. While several alternative formulations of subtyping with equivalent expressive power to the Amber rules exist in the literature [Zhou et al. 2022b], and can avoid built-in reflexivity, none of these formulations is efficient. Surprisingly, there is little work on efficient formulations of (non-declared) iso-recursive subtyping. A notable exception is the work by Ligatti et al. [2017],

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:3

which presents a more powerful formulation of iso-recursive subtyping, using coinductive techniques similar to those adopted in equi-recursive subtyping. Ligatti et al. designed an algorithm with efficiency in mind. However, the use of coinductive reasoning still leads to relatively high computational costs in practice.

In this paper we present QuickSub: an efficient algorithm for iso-recursive subtyping, which is also simple to implement. We prove that QuickSub has the same expressive power as the isorecursive Amber rules. The worst case complexity of QuickSub is 𝑂 ( 𝑛𝑚 ), where 𝑚 is the size of the type and 𝑛 is the number of recursive binders. However, the worst case is hard to reach. Many common cases are linear in practice. For instance, for positive recursive types – which are the only kinds of recursive types supported in languages like Coq [Coq Development Team 2024] or Agda [Norell 2007], and the most common case in functional programming – the algorithm is linear in practice. Moreover, there are still many cases with negative recursive types where the algorithm remains linear. Consequently, QuickSub can be several times faster (sometimes by orders of magnitude) than alternative algorithms, in those cases.

The efficiency of QuickSub is validated via an empirical evaluation comparing it to existing equi-recursive and iso-recursive subtyping algorithms implemented in OCaml [Leroy et al. 2021]. In addition we formalize a simple calculus with recursive subtyping and records. For this calculus we also show how type soundness, transitivity of subtyping and the unfolding lemma [Zhou et al. 2022b] can be proved using QuickSub.

We believe that our work validates the perceived intuition that (inductive) iso-recursive subtyping is, in practice, computationally simpler than formulations based on coinduction. Furthermore, it provides a practical and effective algorithm that can be employed in applications where performance is an important consideration or when equi-recursive subtyping is impractical or undecidable. In summary, the contributions of this paper are:

An efficient algorithm for iso-recursive subtyping. We introduce QuickSub, a novel algorithm for iso-recursive subtyping that significantly improves efficiency over existing algorithmic formulations.
Equivalence proof to the Amber rules. We prove that QuickSub is equivalent in expressive power to the well-known iso-recursive Amber rules.
A direct proof of type soundness of the subtyping rules. We provide a direct type soundness proof for a calculus that employs iso-recursive types and QuickSub subtyping, without relying on any equivalence results to other existing iso-recursive subtyping rules.
Extension to record types. We extend QuickSub to QuickSub[{}] that handles record subtyping, broadening the applicability and flexibility of the algorithm.
Coq formalization, OCaml implementation and empirical evaluation. We provide a mechanical formalization and proofs for all the results in Coq. We also evaluate an OCaml implementation of the algorithm and discuss its performance.

2 Overview

This section provides background of existing approaches to iso-recursive subtyping, and their drawbacks in terms of efficiency. Then it introduces key ideas leading to QuickSub.

2.1 Subtyping Iso-Recursive Types

For recursive types it is common and useful to have subtyping. The metatheory of both equirecursive subtyping [Amadio and Cardelli 1993; Brandt and Henglein 1998; Danielsson and Altenkirch 2010; Gapeyev et al. 2002] and iso-recursive subtyping [Cardelli 1985; Ligatti et al. 2017; Zhou et al. 2020, 2022b] has been studied in the literature. In this paper, we focus on iso-recursive

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:4

subtyping. Before diving into the rules for subtyping iso-recursive types, we first look at some examples to see what kind of recursive types can be in a subtyping relation. We assume standard structural subtyping rules for basic type constructs, such as:

The subtyping rule for function types is contravariant in the argument type and covariant in the return type.

With iso-recursive subtyping, it is expected that if two recursive types are subtypes, then their unfoldings should also be subtypes, which can be expressed as follows:

If 𝜇𝛼. 𝐴 ≤ 𝜇𝛼. 𝐵 then 𝐴 [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] ≤ 𝐵 [ 𝛼 ↦→ 𝜇𝛼. 𝐵 ] .

This property is called the unfolding lemma in the literature [Zhou et al. 2022b], and plays a key role in the type soundness proof in calculi with iso-recursive subtyping. We will reason about the unfolding lemma formally for QuickSub in Section 3. Readers may refer to Zhou et al. [2022b] for a more comprehensive discussion on this property. Here we use the unfolding lemma to identify valid subtyping relations between various examples.

The examples are categorized by different polarities (positive and negative) of recursive variables. Simply put, a type variable occurs positively if it appears on the left side of an even number of arrows (→) in a function type, and negatively if it appears on the left side of an odd number of arrows. For example, in the type 𝛼 →( 𝛽 → 𝛾 ), 𝛼 and 𝛽 occurs negatively, while 𝛾 occurs positively. We will see that the polarity of recursive variables plays a crucial role in determining the subtyping relation between recursive types.

Positive recursive subtyping. Consider 𝜇𝛼. ⊤→ 𝛼 ≤ 𝜇𝛼. nat → 𝛼 , where the recursive variable 𝛼 appears positively. The left type can be regarded as a function that consumes infinite values of any type, and the right type consumes infinite nat values. Therefore, the left type is more general than the right type. The unfolding lemma is helpful to validate this subtyping statement:

𝜇𝛼. ⊤→ 𝛼 ≤ 𝜇𝛼. nat → 𝛼 ⇒ ⊤→( 𝜇𝛼. ⊤→ 𝛼 ) ≤ nat →( 𝜇𝛼. nat → 𝛼 ) After unfolding, we have to check that nat < : ⊤, which is true. If we continue applying additional unfoldings, the subtyping statement would remain valid and simply require more nat < : ⊤ substatements to be validated. When the recursive variable only appears in positive positions, the subtyping relation is straightforward: it suffices to compare the recursive bodies for subtyping.

Negative recursive subtyping. Next, we consider 𝜇𝛼. 𝛼 → nat ≰ 𝜇𝛼. 𝛼 →⊤, where the type on the left can be seen as an object that takes itself and produces a nat value. In contrast, the type on the right takes itself and produces a top value. The subtyping statement above does not hold , as a term of the left type cannot be used where the right type is expected. The type on the right expects an input of an object capable of producing any values, but the type on the left only produces nat values. This inconsistency can be discovered by unfolding the recursive types twice:

(( 𝜇𝛼. 𝛼 → nat) → nat) → nat ≰ (( 𝜇𝛼. 𝛼 →⊤) →⊤) →⊤

Due to the contravariant comparison in function types, we need to check not only nat ≤⊤ but also ⊤≤ nat, which does not hold. It can be seen that negative occurrences of recursive variables prevent many subtyping statements that should hold when the recursive variables are considered as free variables, as in the positive recursive subtyping case. Indeed, they make the subtyping relation “almost” equality. Since the reflexivity property is expected for subtyping, subtyping judgments like 𝜇𝛼. 𝛼 → nat ≤ 𝜇𝛼. 𝛼 → nat should still hold.

At this point it is useful to introduce the concept of equivalent and strict subtyping, which will play an important role in QuickSub. By equivalent subtyping, we mean that two types are subtypes

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:5

of each other, i.e. 𝐴 and 𝐵 are equivalent if 𝐴 ≤ 𝐵 and 𝐵 ≤ 𝐴 . In negative recursive subtyping, recursive types that have equivalent bodies should also be equivalent and therefore in the subtyping relation. By strict subtyping, we mean that 𝐴 is a subtype of 𝐵 but 𝐵 is not a subtype of 𝐴 .

Special cases in negative recursive subtyping. Including equivalent subtyping is not the end of the story for subtyping negative recursive types. For example, consider 𝜇𝛼. ⊤→ 𝛼 ≤ 𝜇𝛼. 𝛼 → 𝛼 , which is a valid strict subtyping relation with negative recursive types. Despite the negative occurrence of 𝛼 in the right type, if we unroll the two recursive types, what we need to compare is

and the contravariant comparison 𝜇𝛼. 𝛼 → 𝛼 ≤⊤ clearly holds.

Handling negative recursive subtyping can be quite tricky. There are many invalid subtyping statements due to contravariance of function types, but we must still allow for the special cases such as reflexivity and subtyping with ⊤ types to hold. Existing approaches to iso-recursive subtyping have introduced various strategies to navigate these complexities and proposed several sets of inference rules for subtyping iso-recursive types. However, these solutions often entail a compromise on efficiency, as we will discuss in the next section.

Nested recursive subtyping. The problem of subtyping iso-recursive types becomes even more complicated when nested recursive types are involved. The polarity of variables becomes less clear in the presence of nested recursive types. Consider comparing the following two types:

The variable 𝛽 appears to be in a positive position in the recursive body of the two types. However, due to the existence of a variable 𝛼 appearing in a negative position, the two types are not related by subtyping. To see this, we unfold the 𝜇𝛼. 𝛼 → 𝛽 twice and compare the two types:

As highlighted by the gray color, the variable 𝛽 appears in a negative position in the recursive body after unfolding. Since the recursive bodies for the 𝛽 variable are strict subtypes, the two types are not subtypes. This example shows that nested recursive types can hide negative occurrences of recursive variables as “apparently” positive ones. Thus, it is difficult to test for the positivity of recursive variables, and the subtyping rules need to be carefully designed to handle such cases.

2.2 Algorithmic Iso-Recursive Subtyping

There are several existing approaches that provide algorithms for iso-recursive subtyping. Next we give an overview of existing approaches and their issues in terms of efficiency.

Amber-style iso-recursive subtyping. The Amber rules have long been known and used for subtyping iso-recursive types. They were initially introduced informally by Cardelli [1985] in the Amber programming language, and later formally studied by Amadio and Cardelli for subtyping equi-recursive types. For subtyping iso-recursive types, variants of Amadio and Cardelli’s rules have been widely used in many different calculi and programming languages [Abadi and Cardelli 1996; Abadi and Fiore 1996; Bengtson et al. 2011; Chugh 2015; Duggan 2002; Lee et al. 2015; Swamy et al. 2011]. The key rules are the rules Amber-var and Amber-rec to compare recursive types.

Amber-var 𝛼_≤_𝛽_∈Δ Δ⊢_𝑎𝑚𝑏𝛼_≤_𝛽	Amber-rec Δ_, 𝛼_≤_𝛽_⊢_𝑎𝑚𝑏A_ ≤_B_ Δ⊢_𝑎𝑚𝑏𝜇𝛼. A_ ≤_𝜇𝛽. B_	Amber-self
		Δ⊢_𝑎𝑚𝑏𝜇𝛼. A_ ≤_𝜇𝛼. A_

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:6

For example, the derivation below shows an application of the Amber rules for subtyping the positive recursive subtyping example that we have seen before:

As discussed before, due to the contravariance of function subtyping, many negative recursive types should be prevented from the subtyping relation. For example, 𝜇𝛼. 𝛼 → nat is not a subtype of 𝜇𝛽. 𝛽 →⊤. The Amber rules deal with this issue nicely with rule Amber-rec, as shown below:

However, such a design also prevents negative recursive types from being subtypes of themselves, which should be allowed due to reflexivity. Therefore, an explicit reflexivity rule Amber-self is needed to handle this case. The presence of rule Amber-self introduces a non-deterministic choice in the subtyping algorithm, since this rule overlaps with rule Amber-rec. This results in a significant performance overhead in the presence of nested recursive types. The built-in reflexivity rule also makes it difficult for the subtyping relation to be extended to non-antisymmetric subtyping relations [Ligatti et al. 2017; Zhou et al. 2022b], such as record subtyping, as discussed in Section 4.

Another technical issue with the Amber rules is that the recursive variable names need to be carefully chosen. When using the rule Amber-rec, the names for the two recursive type variables must be different. This is not conventional in practice, as programmers may write their own names for recursive types or compilers may generate variable names for anonymous recursive types in a way that does not satisfy this requirement. If one considers an internal representation of recursive types, such as de Bruijn indices [De Bruijn 1972] or named representations, then in order to use the Amber rules, one needs to traverse the recursive body every time using rule Amber-rec and rename the variables to a fresh free variable, which leads to a bottleneck in performance as well.

Cardelli [1993] considered an alternative algorithmic formulation of the Amber rules using de Bruijn indices that avoids the issue of variable renaming and non-deterministic choices of recursive subtyping rules [Cardelli 1993, Appendix G.2]. Essentially he defined a new set of rules to compute the “ties” between the recursion variables, which decides whether the recursive types are positive or not before comparing the recursive bodies. However, as we have discussed, with negative recursive subtyping, there can be more complex cases than just equivalence. Since Cardelli [1993]’s algorithmic rules differ a lot from the original form of the Amber rules and there are no formal proofs for the algorithmic rules, it is not clear whether the rules still have the same expressive power as the Amber rules. Moreover, computing the ties requires several extra traversals for the recursive types, and the equivalence is checked by running the subtyping algorithm twice, i.e. checking 𝐴 ≤ 𝐵 and 𝐵 ≤ 𝐴 for 𝐴 ≈ 𝐵 , which still incurs a performance overhead.

Subtyping by nominal unfolding. Despite the Amber rules being widely used in practice, the metatheory for the iso-recursive subtyping Amber rules has not been well studied until recently [Zhou et al. 2020, 2022b]. In Zhou et al.’s work, they proposed a new specification for iso-recursive subtyping rules by finite unfolding , and showed its equivalence to the Amber rules. They have also formulated an algorithmic subtyping relation, called nominal unfolding , to deal with iso-recursive subtyping. The nominal unfoldings rules are easy to work with formally and extend to other subtyping relations, such as records, intersection types [Zhou et al. 2022a], and bounded

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:7

quantification [Zhou et al. 2023] with mechanized proofs in Coq. The nominal unfolding rules are:

The key design for the nominal unfolding rules is that recursive type bodies need to be unfolded by labeled types 𝐴[𝛼] instead of just variables 𝛼 . Labeled types basically help with the double unfolding of the recursive type (as seen in the premise of rule SN-rec), so that the contravariant occurrences of recursive variables can be checked with an extra unfolding. The labels provide a distinct nominal identity to the unfolded form of recursive types so that they can only be compared to unfoldings of the same recursive type. For example, checking the previous positive subtyping example with the nominal unfolding rules follows the derivation below:

The nominal unfolding rules differ from the Amber rules in several ways. Firstly, recursive type variables are not required to be distinct, which makes the rules more convenient for reasoning and fits better with various representations of binders. Secondly, in terms of metatheory, the nominal unfolding rules do not have a built-in reflexivity rule, which makes the subtyping relation applicable to subtyping relations that are not antisymmetric. Zhou et al. proved that the nominal unfolding rules are type sound, and have the same expressive power as the iso-recursive Amber rules via an intermediate iso-recursive subtyping formulation, called weakly positive subtyping . This formulation is discussed in Section 3.2 to establish the expressive power of QuickSub.

Despite these results, the nominal rules are not an efficient algorithm to use in practice. As one can see in rule SN-rec, the unfolding of recursive types can cause an exponential blowup of size in terms of the depth of nested recursive variables. The weakly positive subtyping formulation also has its implementation issues, as we will discuss after introducing them in Section 3.2.

Complete iso-recursive subtyping. As we have seen, the Amber rules, as well as equivalent formulations such as the nominal unfolding rules, lack an efficient algorithmic implementation. There are alternatives to the Amber rules though, that may have a different expressive power but come with efficient algorithms. One such alternative is by Ligatti et al. [2017]. They find that the Amber rules are sound, but incomplete with respect to type-safety. In other words, there can be more subtyping statements that are not covered by the Amber rules, but are still type-safe in the setting of iso-recursive types. These mainly come from recursive type unrolling. The rules for subtyping recursive types employed by Ligatti et al. are:

The basic idea is that subtyping environments 𝑆 track all subtyping relations between recursive types that have already been observed. When deciding whether two recursive types are in a subtyping relation, the environment is consulted first to see if the relation has been observed before (rule L17-rec2). If not, the relation is added to the environment and the recursive type variables are replaced by the recursive types in the bodies (rule L17-rec1). Rule L17-rec1 resembles similar designs in equi-recursive subtyping rules [Brandt and Henglein 1998; Gapeyev et al. 2002],

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:8

and pushes the iso-recursive subtyping relation one step further to also consider recursive type unrolling. For example, the subtyping relation 𝜇𝛼. ⊤→ 𝛼 ≤ 𝜇𝛼. ⊤→( 𝜇𝛽. nat → 𝛽 ) is accepted by their rules, but not by the Amber rules. For a detailed discussion we refer to Zhou et al. [2022b]’s paper for a comparison between the Amber rules and the rules by Ligatti et al..

Rule L17-rec1 may look costly in terms of performance, as it requires unfolding the recursive types with themselves. However, in practice, it can be implemented by compressing all representations of 𝜇 -types into an “unroll table” that maps recursive type variables to their unrolled counterparts. In Ligatti et al.’s paper, one such algorithm is presented and shown to have a complexity of 𝑂 ( 𝑚𝑛 ) where 𝑚 is the number of recursive type variables and 𝑛 is the size of the types in the two types being compared, whichever is larger. Ligatti et al. informally argued that this algorithm is equivalent to the complete rules, but they did not prove this result formally.

2.3 Key Ideas Towards an Efficient Algorithm

The goal of QuickSub is to design an efficient algorithm that has the same expressive power as the Amber rules. Since Amber-style subtyping strikes a good balance between expressive power and simplicity, and has been widely adopted, we believe having an efficient and equivalent algorithm for the Amber rules is of practical significance.

In the rest of this section, we introduce the key design ideas behind the QuickSub algorithm with two goals in mind: being efficient to implement, while also being equivalent in terms of expressive power to the Amber rules. We will use the subtyping examples in previous sections to illustrate these key ideas. The actual final QuickSub algorithm will be introduced in Section 3, exploiting and refining the ideas described in this section.

Tracking polarities. The first observation from the previous examples is that, if the recursive variables all appear in positive positions, then we can just compare the recursive bodies directly. For example, for 𝜇𝛼. ⊤→ 𝛼 ≤ 𝜇𝛼. nat → 𝛼 , we could simply compare the bodies of the recursive types for subtyping. This can be described by the following rule:

where NegVar( 𝐴, 𝐵 ) is the set of negative recursive variables in 𝐴 and 𝐵 . In this way, we do not need to unfold the recursive types as in the nominal unfolding rules, and can directly compare the bodies of the recursive types. The rule can be further optimized by collecting NegVar( 𝐴, 𝐵 ) and checking the inclusion of 𝛼 on the fly, as we will show in Section 3.

Tracking strict subtypes. Rule QS-rec-1 is not sufficient to handle negative recursive types. A recursive type with negative occurrences of recursive variables, such as 𝜇𝛼. 𝛼 → nat, though not a subtype of 𝜇𝛼. 𝛼 →⊤, is still a subtype of itself due to reflexivity. The Amber rules deal with this by having an extra reflexivity rule Amber-self, which is not ideal for an efficient algorithm, since it requires backtracking. To avoid backtracking, our solution is to distinguish strict subtyping from equivalence. This idea can be described by the following rules:

Instead of using a unified symbol ≤ to indicate successful subtype checking, the checking result is now represented as a metavariable ⪅ ∈{ <, ≈} for strict subtyping and equivalence. In other words, we do not interpret the subtyping rules as a function that compares two types for subtyping and returns a boolean. Instead, we would interpret subtyping as a function that compares two types and gives us three possible results: 1) the two types are strict subtypes ( < ); 2) the two types are

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:9

Fig. 1. Illustration of negative recursive subtyping

equivalent subtypes (≈); or 3) subtyping fails. Rule QS-rec-2a accepts both equivalence and strict subtyping for positive recursive types, while rule QS-rec-2b only accepts equivalence for negative recursive types. This way, we can avoid backtracking for reflexivity, since the choice of the rules is deterministic based on whether 𝛼 is in NegVar( 𝐴, 𝐵 ).

Accordingly, the subtype result needs to be tracked throughout the rules. For example, in base cases of the inference rules we have nat ≈ nat and 𝐴 < ⊤ when 𝐴 ≠ ⊤, rather than the generic nat ≤ nat or 𝐴 ≤⊤. The subtype result also needs to be propagated when combining subtyping results. For example, the subtyping rule for function types would be:

Here ⪅1 • ⪅2 is a composition function that combines the subtyping results ⪅1 and ⪅2 to a new subtyping result. It works by checking if both subtyping results are ≈. If so, the composition is ≈; otherwise, it is < . Tracking the equality and strict subtype information precisely in the subtyping rules also avoids the need for running the subtyping algorithm twice as in Cardelli [1993]’s algorithm for Amber rules.

Tracking polarity is not enough: negative variables meet ⊤ types. The rules QS-rec-2a and QSrec-2b, however, still miss some subtyping relations that are valid in the Amber rules. Consider 𝜇𝛼. ⊤→ 𝛼 ≤ 𝜇𝛼. 𝛼 → 𝛼 , which is a valid subtyping statement. This statement is not covered by the rules we have proposed so far, as the recursive variable 𝛼 appears negatively. In a richer subtyping relation there might be more types other than ⊤ to be considered. For example, in the presence of bottom types ⊥, it is also possible to have 𝜇𝛼.𝛼 → 𝛼 < : 𝜇𝛼. ⊥→ 𝛼 . With intersection types, denoted as 𝐴 & 𝐵 for intersecting 𝐴 and 𝐵 , we may also have 𝜇𝛼. (⊤&⊤) → 𝛼 < : 𝜇𝛼.𝛼 → 𝛼 . To achieve a general solution to negative recursive subtyping, it is not effective to just identify those special cases and come up with ad-hoc rules to include them into the subtyping relation.

To have a solution that can scale up and be able to deal with other features that can make the situation even more complicated, we need to look deep into the reason why negative recursive subtyping prevents certain subtyping relations. A key observation in QuickSub is that: if the recursive variable appears at a negative position and is compared with another recursive variable , then the only supertype for its corresponding recursive type is itself and ⊤.

We illustrate this idea in Figure 1. We use superscripts to indicate the polarity of the recursive variables. For example, in comparing the recursive bodies of 𝜇𝛼. 𝛼 → nat ≰ 𝜇𝛼. 𝛼 →⊤, the recursive variable 𝛼 is compared to itself at a negative position, so 𝛼[−] will generate an equality constraint that the recursive type must be equivalent to itself. In contrast, in the second example, 𝛼[−] is compared with ⊤ instead of another recursive variable, so it is allowed for the recursive type to be in a strict subtyping relation. We call the collection of such variables that are compared with another recursive variable negatively the equality variable set , since they essentially pose a constraint on the subtyping derivation that certain recursive types must be equivalent. By refining the NegVar function in rules QS-rec-2a and QS-rec-2b to collect only the equality variable sets, the negative recursive subtyping problem can be handled effectively, as we will detail in Section 3.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:10

Fig. 2. The QuickSub subtyping rules.

3 Efficient Subtyping Algorithm

In this section, we work with a minimal set of types to explain the key idea of QuickSub. The syntax of types, as well as other constructs used in the subtyping algorithm, is:

Types 𝐴, 𝐵 � nat | ⊤| 𝐴 1 → 𝐴 2 | 𝛼 | 𝜇𝛼. 𝐴 Subtyping results ⪅ � < | ≈ 𝑆 Polarity modes ⊕ � + | − Subtyping contexts Ψ � · | Ψ , 𝛼[⊕] Equality variable sets 𝑆 � ∅| { 𝛼 1 , … , 𝛼𝑛 } Meta-variables 𝐴, 𝐵 range over types. Types include base types (nat), the top type (⊤), function types ( 𝐴 1 → 𝐴 2), type variables ( 𝛼 ), and recursive types ( 𝜇𝛼. 𝐴 ). We will explain other constructs in the syntax when they are introduced in the rules.

3.1 QuickSub Subtyping

Figure 2 presents the QuickSub algorithm as syntax-directed inference rules. The subtyping judgement Ψ ⊢⊕ 𝐴 ⪅ 𝐵 determines whether type 𝐴 is a subtype of type 𝐵 under the context Ψ, parameterized by a polarity mode ⊕∈{+ , −}. The notation that we employ is similar to conventional subtyping. However, ⪅ is not simply a piece of notation, but instead it is a parameter of the relation. Moreover, when interpreted algorithmically, this parameter is an output result. The output result ⪅ ∈{ <, ≈ 𝑆 } is a metavariable ranging over two possibilities: strict subtypes ( < ) and or equivalent types (≈ 𝑆 ). The equivalent result also carries an equality variable set 𝑆 , which tracks a set of variables used to check equality constraints during subtyping. Tracking the subtype results and the equality variable sets are key ingredients to the design of our efficient algorithm.

Subtyping base types. Base types nat and ⊤ are equal to themselves (rules QS-nat and QS-topeq), while types that are not equal to the ⊤ type are strict subtypes of ⊤ (rule QS-toplt). Since there are no common free variables in base types, in rules QS-nat and QS-topeq the equality variable set is empty, as indicated by the subscript ≈∅.

Tracking negative recursive variables. As briefly mentioned in Section 2.3, QuickSub uses the equality variable set to track those negative variables that pose an equality constraint on the

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:11

recursive types. To make QuickSub efficient, the equality variable set 𝑆 is collected dynamically in the subtyping derivation. Since the equality variable sets are only used to represent equality constraints, when the subtyping result is strict subtyping, the algorithm can fail immediately, so they are only tracked as part of the equality result, which we denote as ≈ 𝑆 . When the rules are interpreted as an algorithm, the equality variable set is also part of the output result.

Specifically, the equality variable set for two types in a subtyping relation is the set of those variables that are compared with themselves in a negative position of their recursive bodies, as spotted by the rule QS-varneg. When the variables are compared in a positive position, they are not included in the set, as indicated by rule QS-varpos. For example, in the first example of Figure 1, the variable 𝛼 appears negatively in both 𝜇𝛼. 𝛼 → nat and 𝜇𝛼. 𝛼 →⊤, so that rule QS-varneg is used and returns 𝛼[+] ⊢− 𝛼 ≈{ 𝛼 } 𝛼 , assuming the initial polarity mode is positive. In contrast, in the second example 𝜇𝛼. ⊤→ 𝛼 < 𝜇𝛼. 𝛼 → 𝛼 , of Figure 1, the variable 𝛼 is either compared with a top type or appears positively in the recursive type, so that no equality constraints are generated.

Subtyping function types. The equality variable set becomes useful in rule QS-arrow. We present the full definition of function • at the bottom of Figure 2. This definition extends the subtyping result composition function, informally introduced in Section 2.3, to include the equality variable set. The function is partial and for those cases where the composition is undefined, the subtyping checking will fail. Basically there are two cases when • returns a valid result: (1) When both subtyping statements are equality (≈), the output mode is also equality, and the equality variable set is the union of the two sets; (2) When one of the subtyping statements returns a strict subtype result ( < ), the output result must also be strict, and it is required that the equality variable set for the other subtyping statement is empty. In other words, a non-empty equality variable set indicates that the types they are related to cannot be composed with strict subtyping counterparts, as we will show in the example below. When the subtyping result is strict, the equality variable set must be empty for the composition to be valid.

Continuing with the example 𝜇𝛼. 𝛼 → nat ≰ 𝜇𝛼. 𝛼 →⊤ in Figure 1, we wish to detect at an early stage that the negative variable 𝛼 makes subtyping fail. Unlike using substitution (as in the nominal unfolding) or other techniques, QuickSub traverses the types only once without substitutions. The two subtyping premises in the rule QS-arrow are

However, the composition of the two subtyping statements ≈{ 𝛼 } • < is undefined, which makes the subtyping statement fail. This indicates that the negative variable 𝛼 requires an equality constraint on all the types it appears in, which contradicts the strict subtyping result given by the second premise. We will reason about the correctness of the • function formally in Section 3.2.

Subtyping recursive types. The rules QS-reclt, QS-receq, and QS-receqin are the most interesting rules in the algorithm. All three rules start by comparing the recursive body of the two types in the current context extended by a binding that maps the current recursive variable to the current polarity mode, as can be seen from the first premise. Based on the result of subtyping the two recursive type bodies, different rules are chosen. If the subtyping result is strict, the subtyping result in the conclusion is also strict (rule QS-reclt). If the subtyping result is equivalent and the recursive variable 𝛼 is not in the equality variable set, the subtyping result in the conclusion is also equivalent. Moreover the equality variable set is propagated through (rule QS-receq). In this case, there are no constraints on the recursive variable. The presence of the recursive variable in the set, indicates that there is an equality constraint on the variable. Thus, the recursive bodies of

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:12

the two types must be equivalent (rule QS-receqin). In this case, the update of the variable set is more complicated. The free variables in the recursive body are first included, and then the current recursive binder variable is excluded since it is no longer a free variable in the recursive type. The reason why the free variables FV( 𝐴 1) are included is related to nested recursive types. To illustrate this, recall the example for nested recursive types:

𝜇𝛽. ⊤→( 𝜇𝛼. 𝛼 → 𝛽 ) ≰ 𝜇𝛽. nat →( 𝜇𝛼. 𝛼 → 𝛽 )

Variable 𝛽 causes the subtyping statement fail, since it can appear negatively after unfolding the inner recursive type 𝜇𝛼. 𝛼 → 𝛽 twice. This can be seen from the following derivation in QuickSub:

				QS-varneg QS-varpos
𝛽+	QS-toplt ⊢−nat <		⊤	𝛽+, 𝛼+ ⊢−_𝛼_≈{𝛼} 𝛼 𝛽+, 𝛼+ ⊢+ 𝛽_≈∅_𝛽 QS-arrow 𝛽+, 𝛼+ ⊢+ _𝛼_→_𝛽_≈{𝛼} 𝛼_→_𝛽 _𝛼_∈{𝛼} QS-receqin 𝛽+ ⊢+ 𝜇𝛼. 𝛼_→_𝛽 ≈{𝛽} 𝜇𝛼. 𝛼_→_𝛽
		𝛽+ ⊢+ ⊤→(𝜇𝛼. 𝛼_→_𝛽) ≰nat→(𝜇𝛼. 𝛼_→_𝛽) QS-rec… · ⊢+ _𝜇𝛽._⊤→(𝜇𝛼. 𝛼_→_𝛽) ≰_𝜇𝛽._nat→(𝜇𝛼. 𝛼_→_𝛽)			QS-arrow✗

As we highlight in the derivation, the subtyping judgement fails due to the undefined composition < • ≈{ 𝛽 } in the rule QS-arrow rule. The failure can be further traced back to the ≈{ 𝛽 } result after applying the rule QS-receqin rule. Note that the equality variable set { 𝛽 } is computed from ({ 𝛼 } ∪ FV( 𝛼 → 𝛽 )){ 𝛼 }, where FV( 𝛼 → 𝛽 ) = { 𝛼, 𝛽 }. Without the union of FV( 𝐴 1) in rule QSreceqin, the subtyping derivation above would have succeeded since the inner recursive type 𝜇𝛼. 𝛼 → 𝛽 would return ≈∅ and the composition in rule QS-arrow would be valid.

On the other hand, 𝜇𝛼. 𝛼 → 𝛽 is equivalent to itself, so it is not feasible to reject this subtyping statement at a stage when only the 𝜇𝛼. 𝛼 → 𝛽 part is compared. The subtyping will fail only when 𝜇𝛼. 𝛼 → 𝛽 is composed with other strict subtypes, which is the case above. Nonetheless, we still expect the following equivalent subtyping statement to succeed:

QS-arrow	QS-topeq 𝛽+ ⊢−⊤∅≈⊤	QS-topeq 𝛽+ ⊢−⊤∅≈⊤
	QS-receqin
		· ⊢+ _𝜇𝛽._⊤→(𝜇𝛼. 𝛼_→_𝛽) ≈∅_𝜇𝛽._⊤→(𝜇𝛼. 𝛼_→_𝛽)

Therefore, we still allow equivalent recursive types with negative variables to be subtypes of each other, as described in rule QS-receqin. However, we refine the equality variable set so that the variables in negative positions can be precisely tracked, and leave the rejection of strict subtyping to the composition stage in rule QS-arrow. Overall, the interaction between the equality variable set and the subtyping composition function • leads to an efficient algorithm that can handle all iso-recursive subtyping cases effectively.

Analysis of the algorithm performance. For the rules in Figure 2 to be an algorithm, the context Ψ, types 𝐴, 𝐵 and polarity mode ⊕ are considered as inputs, and the subtyping result ⪅ is the output of the algorithm. Since the inference rules only describe the successful cases, the algorithm is defined as a partial function and returns a false result indicating non-subtypes when no rules are applicable. It can be verified that the rules are structurally recursive on the types, and that the size of the inputs will decrease strictly on every recursive call. As a result, the problem of exponential blowup as seen in nominal unfolding rules does not exist. Moreover, the choice of the rules is deterministic.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:13

For example, the choice of rules QS-reclt, QS-receq, and QS-receqin is decided by the result of subtyping for the recursive bodies. Because of the side conditions checking whether the current recursive binder variable is in the equality variable set, there are no performance costs due to backtracking between different inference rules as seen in the Amber rules.

Despite these optimizations, there is still a performance bottleneck in rule QS-receqin of the algorithm when it is repeatedly called on nested recursive types. As we described earlier, the equality variable set 𝑆 is updated by including the free variables of the recursive body and excluding the current recursive binder variable. Computing the free variables and the set union operation can be costly in the worst case. However, this can be optimized by collecting the free variables on the fly and using efficient data structures for set operations. As we will see in Section 5, by using imperative boolean arrays to represent the equality variable set in the QuickSub implementation, the time complexity of set union operation is linear with respect to the number of variables in the set, which in the worst case is the total number of recursive variables 𝑛 in the type. Therefore, assuming the size of the type is 𝑚 , the worst case complexity of the algorithm is 𝑂 ( 𝑚𝑛 ), which remains the same as the complexity of Ligatti et al.’s ML implementation for complete iso-recursive subtyping.

Compared to the nominal rules or the Amber rules, our QuickSub algorithm is more efficient in terms of complexity. The nominal rules have exponential complexity due to the use of substitution for unfolding. Similarly, the Amber rules, also have an exponential complexity on the depth of recursive variables due to a non-deterministic choice of rules for subtyping recursive types, and possibly extra overhead of variable renaming. Another point to note is that the 𝑂 ( 𝑚𝑛 ) complexity is worst case complexity. In practice it is not common to have a large number of negative appearing variables in a type, since these types easily tend make the subtyping judgement fail as we have shown in the examples above. As we will show in Section 5, for practical subtype checking tasks, our algorithm is already efficient to use and scales well to large recursive types, outperforming the other formulations of recursive subtyping.

3.2 Correctness

To prove the correctness of the algorithm we show that QuickSub is equivalent to the Amber rules for iso-recursive subtyping and other equivalent variants defined in previous work. Among these variants we find the weakly positive subtyping rules [Zhou et al. 2022b] most convenient to develop an equivalence proof with QuickSub. The weakly positive subtyping rules were originally proposed as an intermediate step to prove the equivalence between the nominal unfolding rules and the Amber rules. Zhou et al. [2022b] have shown that all the three sets of rules are equivalent to each other. Therefore, by proving the equivalence between QuickSub and the weakly positive subtyping rules, we can establish the equivalence between QuickSub and all of these variants.

Weakly positive subtyping rules. We present the weakly positive subtyping rules by Zhou et al. [2022b] in Figure 3. The rules have two components: weakly positive restriction 𝛼 ∈⊕ 𝐴 ≤ 𝐵 and weakly positive subtyping Γ ⊢ 𝑝 𝐴 ≤ 𝐵 .

The subtyping part is mostly structural. Rule PosRes-rec compares two recursive types by structurally checking the recursive body, but requires that the recursive variable 𝛼 satisfies the weakly positive restriction 𝛼 ∈+ 𝐴 ≤ 𝐵 . As we shall explain later, the weakly positive restriction considers more carefully the polarity of the type variable 𝛼 than standard formulations of positive subtyping [Amadio and Cardelli 1993]. For recursive types that satisfy such restriction, the subtyping can be checked simply by comparing the recursive bodies. There is also a built-in reflexivity rule PosRes-self for comparing negative equivalent recursive types, for a similar reason to that already discussed for the Amber rules.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:14

𝛼 ∈⊕ 𝐴 ≤ 𝐵 (Weakly Positive Restriction) Posvar-arrow Posvar-nat Posvar-topl Posvar-topr 𝛼 ∈⊕ [B][1][≤] [A][1] 𝛼 ∈⊕ A 2 ≤ B 2 𝛼 ∈⊕ nat ≤ nat 𝛼 ∈⊕ A ≤⊤ 𝛼 ∈⊕ ⊤≤ A 𝛼 ∈⊕ A 1 → A 2 ≤ B 1 → B 2 Posvar-vary Posvar-recself Posvar-varx 𝛼 ≠ 𝛽 𝛼 ∉ 𝑓𝑣 ( A ) 𝛼 ∈+ 𝛼 ≤ 𝛼 𝛼 ∈⊕ 𝛽 ≤ 𝛽 𝛼 ∈⊕ 𝜇𝛽. A ≤ 𝜇𝛽. A Posvar-rec 𝛼 ∈⊕ A ≤ B 𝛽 ∈+ A ≤ B 𝛼 ≠ 𝛽 𝛼 ∈⊕ 𝜇𝛽. A ≤ 𝜇𝛽. B Γ ⊢ 𝑝 𝐴 ≤+ 𝐵 (Weakly Positive Subtyping) PosRes-nat PosRes-top PosRes-var PosRes-arrow ⊢ Γ ⊢ Γ Γ ⊢ A ⊢ Γ 𝛼 ∈ Γ Γ ⊢ 𝑝 B 1 ≤ A 1 Γ ⊢ 𝑝 A 2 ≤ B 2 Γ ⊢ 𝑝 nat ≤ nat Γ ⊢ 𝑝 A ≤⊤ Γ ⊢ 𝑝 𝛼 ≤ 𝛼 Γ ⊢ 𝑝 A 1 → A 2 ≤ B 1 → B 2 PosRes-rec PosRes-self Γ , 𝛼 ⊢ 𝑝 A ≤ B 𝛼 ∈+ A ≤ B ⊢ Γ Γ ⊢ 𝜇𝛼. A Γ ⊢ 𝑝 𝜇𝛼. A ≤ 𝜇𝛼. B Γ ⊢ 𝑝 𝜇𝛼. A ≤ 𝜇𝛼. A

Fig. 3. Weakly Positive Subtyping Rules.

The weakly positive restriction describes whether a type variable 𝛼 occurs in a derivation of 𝐴 ≤ 𝐵 with a specific polarity ⊕ (either positive or negative). This relation ensures that given a variable 𝛼 in question, every instance of 𝛼 ≤ 𝛼 in the derivation of 𝐴 ≤ 𝐵 only occurs in a positive position (rule Posvar-varx), so that invalid contravariant subderivations are prevented. For recursive types, the weakly positive restriction is satisfied in two cases: either the recursive bodies are equal and 𝛼 is not free in 𝜇𝛽. 𝐴 (rule Posvar-recself), or the recursive variable 𝛽 is found in a weakly positive position inside the proof and 𝛼 satisfies the weakly positive restriction in the recursive bodies (rule Posvar-rec).

To see why rule Posvar-rec needs the second condition, consider the following example:

which will be rejected by both rules Posvar-recself and Posvar-rec, since 𝛽 ∈ FV( 𝛼 → 𝛽 ) and 𝛼 ∈+ 𝛼 → 𝛽 ≤ 𝛼 → 𝛽 is not derivable. Otherwise, unfolding the recursive type would lead to

with a negative subderivation 𝛽 ∈− 𝛽 ≤ 𝛽 , which leads to an inconsistency in the rules. Overall, the weakly positive subtyping restriction, as well as the subtyping rules ensures that iso-recursive subtyping is correctly handled. For a detailed discussion on the weakly positive subtyping rules, we refer the readers to Zhou et al.’s work.

Relating QuickSub to the weakly positive restriction. The weakly positive restriction provides a way to formally reason about the equality variable sets in QuickSub. Indeed, we can show that the QuickSub context Ψ captures the weakly positive information of all the variables in the context.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:15

Depending on whether the variable 𝛼[⊕][′] ∈ Ψ has the same polarity as the polarity ⊕ of the current subtyping judgment, we can determine whether 𝛼 appears weakly positively or negatively in the two types 𝐴 and 𝐵 , as described in the following theorems.

Theorem 3.1 (Relation to weakly positive restrictions (strict subtyping)) . If Ψ ⊢⊕ 𝐴 < 𝐵 , then

(1) 𝛼[⊕] ∈ Ψ implies 𝛼 ∈+ 𝐴 ≤ 𝐵
⊕
(2) 𝛼 ∈ Ψ implies 𝛼 ∈− 𝐴 ≤ 𝐵

This also holds for the case of ≈ 𝑆 , but only in the case where the variable 𝛼 is not in the equality variable set 𝑆 . When 𝛼 ∈ 𝑆 , indicating there is a negative equality 𝛼 ≤ 𝛼 in the derivation of 𝐴 ≈ 𝐵 (see rule QS-varneg), the weakly positive restriction no longer holds. Note that we use ∉⊕ to denote the logical negation of ∈⊕, and that ∉+ is not equivalent to ∈−.

Theorem 3.2 (Relation to weakly positive restrictions (equivalence)) . If Ψ ⊢⊕ 𝐴 ≈ 𝑆 𝐵 , then

(1) 𝛼[⊕] ∈ Ψ and 𝛼 ∉ 𝑆 implies 𝛼 ∈+ 𝐴 ≤ 𝐵
⊕
(2) 𝛼 ∈ Ψ and 𝛼 ∉ 𝑆 implies 𝛼 ∈− 𝐴 ≤ 𝐵
(3) 𝛼[⊕] ∈ Ψ and 𝛼 ∈ 𝑆 implies 𝛼 ∉+ 𝐴 ≤ 𝐵
⊕
(4) 𝛼 ∈ Ψ and 𝛼 ∈ 𝑆 implies 𝛼 ∉− 𝐴 ≤ 𝐵

For the sake of completeness we also prove a theorem for the case when 𝛼 is a fresh variable that does not appear in Ψ. In this case, it is guaranteed that 𝛼 appears weakly positively and negatively in the subtyping judgment 𝐴 ≤ 𝐵 .

Theorem 3.3 (Relation to weakly positive restrictions (fresh variables)) . If Ψ ⊢⊕ 𝐴 ⪅ 𝐵 , then for any 𝛼 ∉ dom Ψ and any polarity ⊕[′] , 𝛼 ∈⊕[′] 𝐴 ≤ 𝐵 .

Soundness of QuickSub to weakly positive subtyping. We can now show that the QuickSub rules are sound with respect to the weakly positive subtyping rules.

Theorem 3.4 (Soundness of QuickSub to Weakly Positive Subtyping) . If Ψ ⊢⊕ 𝐴 ⪅ 𝐵 , then |Ψ| ⊢ 𝑝 𝐴 ≤ 𝐵 , where |Ψ| removes all the polarity annotations from the context Ψ.

The proof is straightforward by induction on the derivation of Ψ ⊢⊕ 𝐴 ⪅ 𝐵 . Most of the cases are direct by induction hypotheses, except for the recursive type cases Ψ ⊢⊕ 𝜇𝛼. 𝐴 ⪅ 𝜇𝛼. 𝐵 . For case QS-reclt and QS-receq, by Theorem 3.1 (1) and Theorem 3.2 (1), we know that 𝛼 ∈+ 𝐴 ≤ 𝐵 , so that rule PosRes-rec can be applied. For case QS-receqin, by Theorem 3.5 the two recursive types are equal, so that we can apply the rule PosRes-self to complete the proof. The proof of Theorem 3.5 is straightforward by induction on the subtyping derivation.

Theorem 3.5 (QuickSub equivalence implies equality) . If Ψ ⊢⊕ 𝐴 ≈ 𝑆 𝐵 , then 𝐴 = 𝐵 .

Completeness of QuickSub to weakly positive subtyping. We wish to prove the following theorem to show that QuickSub is complete with respect to the weakly positive subtyping rules:

Theorem 3.6 (Completeness of QuickSub) . If · ⊢ 𝑝 𝐴 ≤ 𝐵 , then there exists ⪅, such that · ⊢+ 𝐴 ⪅ 𝐵 .

The proof of Theorem 3.6 is not straightforward by induction, as the empty context · needs to be generalized to handle recursive cases. However, the context cannot be generalized arbitrarily. For example, consider the weakly positive subtyping judgment 𝛼 ⊢ 𝑝 𝛼 → nat ≤ 𝛼 →⊤. Annotating 𝛼 with positive polarity leads to an invalid judgment in QuickSub:

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:16

----- Start of picture text -----
sound sound
Weakly Positive Nominal Unfolding
QuickSub
Subtyping Rules
complete complete
✓ Type soundness
sound & complete • Transitivity
• Unfolding lemma
• Progress
Amber Rules • Preservation
• …
This paper Zhou et al. [2022b]’s work
----- End of picture text -----

Fig. 4. Type soundness proof framework for QuickSub, indirectly

This suggests that in the generalized lemma we need to specify how the weakly positive subtyping context Γ, that only contains variables, is related to the QuickSub context Ψ in the conclusion, which also assigns polarities to variables. To this end we define a restriction well bound context to ensure that all the variables in the context Ψ are consistent with the polarity of the subtyping judgment up to the weakly positive restriction, so that the context can be safely generalized.

Definition 3.7 (Well bound context) . A context Ψ is well bound with respect to a polarity ⊕ and two types 𝐴 and 𝐵 , denoted as Ψ ∈⊕ 𝐴 ≤ 𝐵 , if for any 𝛼[⊕][′] ∈ Ψ, 𝛼 ∈⊕[′] +⊕ 𝐴 ≤ 𝐵 , where ⊕[′] + ⊕ is + if ⊕[′] and ⊕ are the same, and − otherwise.

The generalized lemma is then stated as follows:

Lemma 3.8 (Generalized completeness of QuickSub) . If Γ ⊢ 𝑝 𝐴 ≤ 𝐵 , and there exists Ψ such that dom Γ = dom Ψ, and Ψ ∈⊕ 𝐴 ≤ 𝐵 , then there exists ⪅, such that Ψ ⊢+ 𝐴 ⪅ 𝐵 .

The proof of the generalized lemma is by induction on the derivation of Γ ⊢ 𝑝 𝐴 ≤ 𝐵 . Most of the cases follow the induction hypotheses directly. In the cases for recursive types we need to show that the extended context (Ψ , 𝛼[⊕] ) is well bound, which is guaranteed by the weakly positive conditions in the weakly positive subtyping premise. The most interesting case is the PosRes-arrow case, in which we get two QuickSub results 𝐵 1 ⪅1 𝐴 1 and 𝐵 2 ⪅2 𝐴 2 from the induction hypothesis. We need to show that ⪅1 • ⪅2 does not cause trouble so that rule QS-arrow can be applied. Thanks to the well bound context restriction, those cases where ⪅1 • ⪅2 are undefined can be ruled out by contradiction. We refer the reader to the Coq formalization for the detailed proof.

3.3 Direct Proof of Type Soundness

We have shown that QuickSub is equivalent to the weakly positive subtyping rules in the previous section. Since Zhou et al. [2022b] have proven that the weakly positive subtyping rules are sound and complete to the nominal unfolding rules, and that the nominal unfolding rules are type sound, we can conclude that QuickSub is also type sound. This proof is illustrated in Figure 4, which we refer to as an indirect proof of type soundness, as the proof relies on the development of other equivalent subtyping rules. In this section we provide a direct proof of type soundness for QuickSub.

Why a direct proof? While the indirect proof shown in Figure 4 has effectively established type soundness by linking QuickSub to established rules, there are strong reasons to also study a direct proof for QuickSub. Firstly, proving type soundness via equivalence to other rules involves significant additional complexity. This can be observed by the fact that useful properties of the

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:17

Amber rules that contribute to type soundness, such as transitivity of subtyping and unfolding lemma, which we will state shortly, are proven indirectly by showing their equivalence to the nominal unfolding rules [Zhou et al. 2022b]. Whether there exists a direct proof for other equivalent rules is not clear. It is also non-trivial to prove the equivalence between various iso-recursive subtyping rules without going through an intermediate equivalent system that is carefully defined for the purpose of proving equivalence, such as the weakly positive subtyping rules. Each of the six soundness or completeness proofs in Figure 4 requires significant reasoning and many auxiliary lemmas. Therefore, although only two soundness and completeness proofs highlighted in gray in Figure 4 are needed to prove type soundness for QuickSub, the overall proof framework still has a high level of complexity.

Moreover, having a direct proof makes QuickSub easier to extend in the future with new features. If all we cared were the features that are already present in Zhou et al. [2022b]’s work, then an indirect proof framework like Figure 4 would be sufficient. However, most of the time one would like to study iso-recursive subtyping with other features, such as records, polymorphism, bounded quantification [Zhou et al. 2023], and intersection [Zhou et al. 2022a] or union types. In this case, if one wants to add new features to QuickSub using an indirect proof, it would require modifying the underlying systems, proving type soundness within those systems, and updating the equivalence proofs. As there are many complexities involved in all these steps, this would be a large burden. In contrast, with a direct type soundness proof, each new feature can be added and assessed for type soundness in isolation, simplifying the proof development process considerably.

A calculus with iso-recursive types and QuickSub subtyping. We develop a simple calculus to show how a direct proof of type soundness can be developed for QuickSub. The syntax, typing rules and reduction rules are presented in Figure 5. Meta-variables 𝑒 range over expressions, with conventional syntax for variables ( 𝑥 ), integers (n), applications ( 𝑒 1 𝑒 2), lambda abstractions ( 𝜆𝑥 : 𝐴. 𝑒 ), unfolding (unfold [ 𝐴 ] 𝑒 ) and folding (fold [ 𝐴 ] 𝑒 ) expressions for iso-recursive types.

The typing rules are standard. For base cases ⊢ Γ checks the well-formedness of the context Γ, which requires that all the variable types in the context are well-formed. A fold expression constructs a recursive type (rule Typing-fold), while an unfold expression opens a recursive type to its unfolding (rule Typing-unfold). One specialized rule is the subsumption rule Typing-sub, which calls QuickSub with an empty context · and positive polarity + to check the subtyping relation between types 𝐴 and 𝐵 . Both strict subtyping and equivalence are accepted in the subsumption rule.

The reduction rules for the calculus are also standard. In rules step-fold and step-unfold the expressions inside the fold and unfold constructs are reduced until they reach a value. The fold of values are treated as values, while for unfold expressions with fold values, the rule step-fld is applied to eliminate the pair of annotations.

Unfolding lemma. We prove the type soundness of the calculus using progress and preservation. As identified by previous works on iso-recursive subtyping [Ligatti et al. 2017; Zhou et al. 2022b] the key to the type soundness proof is the unfolding lemma :

Lemma 3.9 (Unfolding lemma) . If · ⊢+ 𝜇𝛼. 𝐴 ⪅ 𝜇𝛼. 𝐵 , then · ⊢+ 𝐴 [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ] ⪅ 𝐵 [ 𝛼 ↦→ 𝜇𝛼. 𝐵 ]

The unfolding lemma ensures the preservation property for iso-recursive typing in the presence of subtyping. To illustrate this, consider an expression unfold [ 𝜇𝛼. 𝐵 ] (fold [ 𝜇𝛼. 𝐴 ] 𝑣 ). The derivation below shows the typing of this expression.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:18

Fig. 5. Typing and Reduction Rules

By inversion we know that after reduction using rule step-fld, the result 𝑣 has the type 𝐴 [ 𝛼 ↦→ 𝜇𝛼. 𝐴 ], and that 𝜇𝛼. 𝐴 ⪅ 𝜇𝛼. 𝐵 . To prove preservation that 𝑣 has the type 𝐵 [ 𝛼 ↦→ 𝜇𝛼. 𝐵 ] after reduction, the unfolding lemma is necessary.

The unfolding lemma is proved as a corollary of the generalized lemma below:

Lemma 3.10 (Generalized unfolding lemma) . If Ψ2 ⊢⊕ 𝐶 ⪅1 𝐷 , then

(1) Ψ1 , 𝛼[⊕] , Ψ2 ⊢⊕ 𝐴 ⪅2 𝐵 and Ψ1 , 𝛼[⊕] , Ψ2 ∈⊕ 𝐴 ≤ 𝐵 implies that there exists ⪅[′] , such that Ψ1 , Ψ2 ⊢⊕ 𝐴 [ 𝛼 ↦→ 𝐶 ] ⪅[′] 𝐵 [ 𝛼 ↦→ 𝐷 ].
(2) Ψ1 , 𝛼 ⊕ , Ψ2 ⊢⊕ 𝐴 ⪅2 𝐵 and Ψ1 , 𝛼 ⊕ , Ψ2 ∈⊕ 𝐴 ≤ 𝐵 implies that there exists ⪅[′] , such that Ψ1 , Ψ2 ⊢⊕ 𝐴 [ 𝛼 ↦→ 𝐷 ] ⪅[′] 𝐵 [ 𝛼 ↦→ 𝐶 ].

The generalized unfolding lemma basically states that one can substitute variable 𝛼 in the types 𝐴 ⪅2 𝐵 in a subtyping judgment with a pair of types 𝐶 ⪅1 𝐷 that are also related by subtyping. When the polarity of 𝛼 is consistent with the polarity of the subtyping judgment, the substitution can be done covariantly, and contravariantly otherwise, as expressed by the two sub-cases in the lemma. The two sub-cases need to be proved simultaneously, as in rule QS-arrow the substitution direction may be swapped in the contravariant condition. For a similar reason as in the proof of

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:19

the generalized completeness lemma (Lemma 3.8), we need to generalize the unfolding lemma to a well bound context, so that problematic cases like the undefined composition ⪅1 • ⪅2 in case QS-arrow are avoided. Note that for defining the well bound context condition, only the weakly positive restriction (the upper part of Figure 3) is needed, not the full weakly positive subtyping rules. With Lemma 3.10 there is no need to go through QuickSub’s soundness or completeness to the weakly positive subtyping rules as we did in Section 3.2 for type soundness. For the detailed proof of the generalized unfolding lemma, we refer the readers to the Coq mechanization.

Next, we show how Lemma 3.10 is used to prove the unfolding lemma. There are two cases for the result of · ⊢+ 𝜇𝛼. 𝐴 ⪅ 𝜇𝛼. 𝐵 . When ⪅ = < , by inversion we know 𝛼[+] ⊢+ 𝐴 < 𝐵 . By Theorem 3.1 we know that 𝛼 ∈+ 𝐴 ≤ 𝐵 so that the well bound context condition is satisfied. By setting Ψ1 = ·, Ψ2 = ·, ⊕ = +, 𝐶 = 𝜇𝛼. 𝐴 , 𝐷 = 𝜇𝛼. 𝐵 , ⪅1 = ⪅2 = < , in Lemma 3.10, we can derive the unfolding lemma. When ⪅=≈, we directly know that 𝐴 = 𝐵 , and the unfolding lemma holds by reflexivity:

Theorem 3.11 (Reflexivity) . For any closed type 𝐴 , there exists 𝑆 , such that · ⊢+ 𝐴 ≈ 𝑆 𝐴 .

Transitivity. To prove type safety directly it is also required that the subtyping relation must be transitive. For algorithmic subtyping, transitivity is not a built-in inference rule and therefore needs to be proved as a theorem. The proof of transitivity for the Amber rules used to be a challenging task and required intricate proof techniques [Bengtson et al. 2011]. Zhou et al. [2022b] showed that with the nominal unfolding rules, they can have an easy proof of transitivity. We also prove the transitivity theorem for QuickSub directly.

Theorem 3.12 (Transitivity) . If Ψ ⊢⊕ 𝐴 ⪅1 𝐵 and Ψ ⊢⊕ 𝐵 ⪅2 𝐶 , then Ψ ⊢⊕ 𝐴 (⪅1 ◦ ⪅2) 𝐶 , where

< ◦ < = <, < ◦≈ 𝑆 = <, ≈ 𝑆 ◦ < = <, ≈ 𝑆 1 ◦≈ 𝑆 2 = ≈ 𝑆 1∪ 𝑆 2

The sequential composition operator ◦ can be regarded as a total function version of the composition operator • that does not rule out the case where < is composed with ≈ 𝑆 where 𝑆 ≠ ∅. The transitivity theorem is proved by induction on the intermediate type 𝐵 and then case analysis on the two subtyping relations in the conventional way.

Type Soundness. With the unfolding lemma and the transitivity theorem for QuickSub, the type soundness of the calculus in Figure 5 can be proved in a standard way.

Theorem 3.13 (Progress) . For any expression 𝑒 and type 𝐴 , if · ⊢ 𝑒 : 𝐴 then either 𝑒 is a value or there exists an expression 𝑒[′] such that 𝑒 ↩ → 𝑒[′] .

Theorem 3.14 (Preservation) . For any expression 𝑒 and type 𝐴 , if · ⊢ 𝑒 : 𝐴 and 𝑒 ↩ → 𝑒[′] then · ⊢ 𝑒[′] : 𝐴 .

4 Extension to Records

For practical uses of QuickSub, it is useful to extend the subtyping rules to features that are common in programming languages. In this section we show how QuickSub can be extended to handle record types with iso-recursive subtyping. We present an extension of QuickSub, which we call QuickSub[{}] and show its use in a calculus with records, iso-recursive types and subtyping.

4.1 Record Subtyping

We start by revisiting the standard subtyping rules for record types [Pierce 2002], which can be written as:

where { 𝑙𝑖 : 𝐴𝑖[𝑖][∈][1][···] [𝑚] } and { 𝑘 𝑗 : 𝐵 𝑗[𝑗][∈][1][···] [𝑛] } are two record types with 𝑚 and 𝑛 fields respectively. Two record types are in a subtyping relation when the fields of the right type are a subset of the left type, and the types of the corresponding fields are subtypes.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:20

Fig. 6. The QuickSub subtyping rules for record types.

In many cases, this rule can be directly added to an existing set of inference rules for subtyping without modifications to the existing rules, which is the case for the nominal unfolding rules in Zhou et al. [2022b]. However, this does not work for other variants of iso-recursive subtyping rules, such as the weakly positive subtyping rules and the Amber rules, as well as the rules for the QuickSub algorithm. The addition of record types makes the subtyping relation non-antisymmetric.

Our solution. We follow our previous design and extend the subtyping rules to handle record types directly, as shown in Figure 6. Similarly to the standard approach to record subtyping (rule S- rcd), in rule QS-rcd, we also check whether the fields of the two record types are in a set inclusion relation, and then we compute the subtyping results of all the corresponding fields as ⪅ 𝑖 . All the results are then combined with the • operator, which is the same composition operator in rule QSarrow. When interpreted algorithmically, the second premise of the rule can be implemented by traversing all the fields of { 𝑙𝑖 : 𝐵𝑖[𝑖][∈][1][···] [𝑚] } and looking up the corresponding field in { 𝑘 𝑗 : 𝐴 𝑗[𝑗][∈][1][···] [𝑛] }. Assuming a proper data structure for record types, such as a hash table, or a sorted list, the cost of record traversal should be linear to the number of fields in the record type so that the overall complexity of QuickSub[{}] remains the same as QuickSub.

One key design here is that we also distinguish strict label inclusion from equivalent label sets. When the two record types have the same set of labels, all the results can be combined directly, so that when all the record fields have equivalent types, the two record types should be equivalent. This is not the case when there are labels that only appear in the left type, since they prevent the two record types from being equivalent. Therefore, the record field subtyping results should be folded to a strict subtyping result < .

Unlike QuickSub, there is no equivalence result for QuickSub[{}] with respect to weakly positive rules and the Amber rules. This is because the extension to non-antisymmetric relations for weakly positive rules is not studied in the literature. One way to bridge this gap is to have a direct equivalence proof for QuickSub[{}] with respect to nominal unfolding rules, which have been extended with record types [Zhou et al. 2022b]. We leave this as future work.

4.2 A Calculus with QuickSub[{}]

Despite the lack of an equivalence result for QuickSub[{}] with respect to weakly positive rules and the Amber rules, we can still show that QuickSub[{}] is type sound, since the type soundness proof we have developed in Section 3.3 does not rely on other subtyping rules. We present a calculus with QuickSub[{}] in Figure 7, which extends the calculus in Figure 5 with expressions. The expression syntax is extended with record expressions and record projections, as indicated by the gray color, with standard typing and reduction rules.

We prove the unfolding lemma and transitivity theorem for QuickSub[{}] in the same way as we did for QuickSub. One technical detail in the proof of the unfolding lemma is that the generalized

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:21

|Expressions
𝑒
�
𝑥| i |𝑒_1_𝑒_2 | 𝜆𝑥:𝐴. 𝑒| unfold [𝐴]𝑒| fold [𝐴]𝑒|
{𝑙𝑖=𝑒𝑖𝑖_∈1···𝑛} |
𝑒.𝑙
Values
𝑣
�
i | 𝜆𝑥:𝐴. 𝑒| fold [𝐴]𝑣|
{𝑙𝑖=𝑣𝑖𝑖_∈1···𝑛}
Γ ⊢_𝑒:𝐴
(Record Typing)
typing-proj
Γ ⊢_e_: {𝑙𝑖:A𝑖𝑖_∈1···𝑛}
Γ ⊢_e.𝑙𝑖:A𝑖
typing-rcd
for each_𝑖_
Γ ⊢_e𝑖_:A𝑖
Γ ⊢{𝑙𝑖=e𝑖𝑖_∈1···𝑛} : {𝑙𝑖:A𝑖𝑖_∈1···𝑛}
𝑒_1 ↩_→_𝑒_2
(Record Reduction)
step-proj
e ↩_→_e′
e.𝑙𝑗↩_→_e′.𝑙𝑗
step-projrcd
{𝑙𝑖=v𝑖𝑖_∈1···𝑛}.𝑙𝑗↩_→_v𝑗_
step-rcd
e𝑗↩_→_e′
𝑗
{𝑙𝑖=𝑣𝑖𝑖_∈1···𝑗_−1, 𝑙𝑗=e𝑗, 𝑙𝑘=𝑒𝑘𝑘_∈_𝑗+1···𝑛} ↩_→{𝑙𝑖=𝑣𝑖𝑖_∈1···𝑗_−1, 𝑙𝑗=e′
𝑗, 𝑙𝑘=𝑒𝑘𝑘_∈_𝑗+1···𝑛}|Expressions
𝑒
�
𝑥| i |𝑒_1_𝑒_2 | 𝜆𝑥:𝐴. 𝑒| unfold [𝐴]𝑒| fold [𝐴]𝑒|
{𝑙𝑖=𝑒𝑖𝑖_∈1···𝑛} |
𝑒.𝑙
Values
𝑣
�
i | 𝜆𝑥:𝐴. 𝑒| fold [𝐴]𝑣|
{𝑙𝑖=𝑣𝑖𝑖_∈1···𝑛}
Γ ⊢_𝑒:𝐴
(Record Typing)
typing-proj
Γ ⊢_e: {𝑙𝑖:A𝑖𝑖_∈1···𝑛}
Γ ⊢_e.𝑙𝑖:A𝑖
typing-rcd
for each_𝑖_
Γ ⊢_e𝑖_:A𝑖
Γ ⊢{𝑙𝑖=e𝑖𝑖_∈1···𝑛} : {𝑙𝑖:A𝑖𝑖_∈1···𝑛}
𝑒_1 ↩_→_𝑒_2
(Record Reduction)
step-proj
e ↩_→_e′
e.𝑙𝑗↩_→_e′.𝑙𝑗
step-projrcd
{𝑙𝑖=v𝑖𝑖_∈1···𝑛}.𝑙𝑗↩_→_v𝑗_
step-rcd
e𝑗↩_→_e′
𝑗
{𝑙𝑖=𝑣𝑖𝑖_∈1···𝑗_−1, 𝑙𝑗=e𝑗, 𝑙𝑘=𝑒𝑘𝑘_∈_𝑗+1···𝑛} _↩_→{𝑙𝑖=𝑣𝑖𝑖_∈1···𝑗_−1, 𝑙𝑗=e′
𝑗, 𝑙𝑘=𝑒𝑘𝑘_∈_𝑗+1···𝑛}| |---|---| |_𝑒_1 _↩_→_𝑒_2|| ||| ||{𝑙𝑖=_𝑣𝑖𝑖_∈1···𝑗_−1, _|

Fig. 7. Extension to record expressions.

unfolding lemma requires a well bound condition, which makes use of the weakly positive restriction. To make the proof work for QuickSub[{}] , we extend the syntactic reflexivity of 𝜇𝛽. 𝐴 in rule Posvarrecself to a more general equivalence relation 𝜇𝛽. 𝐴 ≈ 𝜇𝛽. 𝐵 , considering record permutation. The two key lemmas for establishing type soundness, the unfolding lemma and transitivity, are:

Theorem 4.1 (Unfolding lemma for QuickSub[{}] ) .

Theorem 4.2 (Transitivity for QuickSub[{}] ) . If Ψ ⊢⊕ 𝐴 ⪅1 𝐵 and Ψ ⊢⊕ 𝐵 ⪅2 𝐶 , then Ψ ⊢⊕ 𝐴 (⪅1 ◦ ⪅2) 𝐶 .

With the unfolding lemma and transitivity theorem for QuickSub[{}] , we can show that the calculus in Figure 7 is type sound by standard progress and preservation lemmas.

5 Evaluation

We provide an OCaml implementation of QuickSub. The QuickSub rules in Figure 2 can be easily translated into a recursive function, as shown in Figure 8, by considering the subtyping results as outputs and the other components in the judgement Ψ ⊢⊕ 𝐴 ⪅ 𝐵 as inputs. However, the set union and computation of the free variables in the last case of the function, if implemented naively, such as using the OCaml Set module, can be costly in some cases. Consider the following application of rule QS-recsqin:

With functional Set operations, several meta-operations are required for this step: (1) determining the membership of 𝛼𝑛 in the set takes 𝑂 (log 𝑛 ) time, (2) computing the free variables of the type 𝛼 1 → … → 𝛼𝑛 → nat takes 𝑂 ( 𝑚 ) time, where 𝑚 is the size of the type, (3) computing the union of the sets takes 𝑂 ( 𝑛 ) time, and (4) removing 𝛼𝑛 from the set takes 𝑂 (log 𝑛 ) time.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:22

SubΨ (nat , nat , ⊕) = ≈∅ SubΨ (⊤ , ⊤ , ⊕) = ≈∅ SubΨ ( 𝐴, ⊤ , ⊕) = < (if 𝐴 ≠ ⊤) SubΨ ( 𝛼, 𝛼, ⊕) = ≈∅ (if 𝛼[⊕] ∈ Ψ) SubΨ ( 𝛼, 𝛼, ⊕) = ≈{ 𝛼 } (if 𝛼 ⊕ ∈ Ψ) SubΨ ( 𝐴 1 → 𝐴 2 , 𝐵 1 → 𝐵 2 , ⊕) = SubΨ ( 𝐴 2 ,𝐴 1 , ⊕) • SubΨ ( 𝐵 1 , 𝐵 2 , ⊕) SubΨ ( 𝜇𝛼. 𝐴 1 , 𝜇𝛼. 𝐴 2 , ⊕) = < (if SubΨ ,𝛼 ⊕ ( 𝐴 1 ,𝐴 2 , ⊕) = < ) SubΨ ( 𝜇𝛼. 𝐴 1 , 𝜇𝛼. 𝐴 2 , ⊕) = ≈ 𝑆 (if SubΨ ,𝛼 ⊕ ( 𝐴 1 ,𝐴 2 , ⊕) = ≈ 𝑆 and 𝛼 ∉ 𝑆 ) SubΨ ( 𝜇𝛼. 𝐴 1 , 𝜇𝛼. 𝐴 2 , ⊕) = ≈( 𝑆 ∪FV( A 1 )){ 𝛼 } (if SubΨ ,𝛼 ⊕ ( 𝐴 1 ,𝐴 2 , ⊕) = ≈ 𝑆 and 𝛼 ∈ 𝑆 ) otherwise, SubΨ ( 𝐴, 𝐵, ⊕) fails

Fig. 8. Functional implementation of QuickSub

To address this bottleneck, in our implementation we adopt a more efficient version SubImp of QuickSub, that carries two extra parameters, 𝑆 ev and 𝑆 fv, both of which are imperative boolean arrays that map all variables in the types to a boolean value. 𝑆 ev [ 𝛼 ] indicates whether the variable 𝛼 is in the equality variable set, while 𝑆 fv tracks the free variables on the fly. In the optimized subtyping function, for the QS-recsqin rule, SubImpΨ ( 𝜇𝛼. 𝐴 1 , 𝜇𝛼. 𝐴 2 , ⊕ ,𝑆 ev ,𝑆 fv) now performs the following operations:

(1) Before making the recursive call on the inner body, set 𝑆 fv [ 𝛼 ] to true, indicating that 𝛼 is considered as a free variable in the inner body, which takes 𝑂 (1) time.
(2) After the recursive call, determine the membership of 𝛼 in the set, which takes 𝑂 (1) time.
(3) Traverse 𝑆 fv and update 𝑆 ev for the union operation 𝑆 ∪ FV( 𝐴 1), which takes 𝑂 ( 𝑛 ) time.
(4) Set 𝑆 ev [ 𝛼 ] to false to discard 𝛼 from the equality variable set, which takes 𝑂 (1) time. (5) Update 𝑆 fv to remove 𝛼 , which takes 𝑂 (1) time.

With this optimization, the only costly operation is the set union operation, which is 𝑂 ( 𝑛 ), while the rest of the operations are 𝑂 (1), a large improvement over the functional implementation. Readers may refer to the OCaml code for the full implementation details.

In the rest of this section, we evaluate the imperative implementation of QuickSub on a set of benchmarks to evaluate its performance and scalability. For the sake of evaluation we add a new base type real and new type constructs, namely sum types ( 𝐴 + 𝐵 ) and product types ( 𝐴 × 𝐵 ), to the implementation so that useful benchmarks can be generated. The subtyping rules are standard:

Note that whether real can be a supertype of nat remains debatable [Harper 2016], but we use it here for benchmarking purposes. The nat ≤ real subtyping is not integral to the main system, and can be replaced with dummy records (e.g., { 𝑙 Real : nat ,𝑙 Nat : nat} ≤{ 𝑙 Real : nat}) if needed.

We compare the performance of QuickSub with several algorithms in the literature, including:

The slightly optimized implementation of the nominal unfolding rules for subtyping isorecursive types by Zhou et al. [2022b], which avoids substitutions in positive positions:

The polarized form of substitution [ 𝛼 ↦→ 𝐴 ][−] 𝐵 , only performs substitutions at negative occurrences of type variables. Zhou et al. [2022b, Section 2.7] discussed that special case of covariant subtyping, and mentioned that it would behave equivalently to rule SN-rec.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:23

|No.|QuickSub|Amber
1985|Complete
2017|Nominal
2022b|Equi
2002|Description||𝑆|max| |---|---|---|---|---|---|---|---| |1|0.0045|1.7230|2.0541|5.6194|42.0146|Disprove negative <|1| |2|0.0079|0.0004|1.9483|6.3181|41.6360|Prove negative≈(simple)|1| |3|0.0085|7.3775|3.7602|12.6697|Timeout|Prove positive < (simple)|0| |4|0.0221|5.7502|3.4782|91.0706|Timeout|Disprove positive <|0| |5|0.0054|0.0006|3.8383|22.2383|Timeout|Prove positive≈|0| |6|0.0038|0.1829|1.2995|0.6027|Timeout|Prove mixed tests|1| |7|0.0082|5.7185|3.5229|30.0276|Timeout|Prove positive < (nested)|0| |8|0.0817|0.0057|3.8423|Timeout|Timeout|Prove negative≈(worst)|500|

Table 1. Time (seconds) taken for benchmarks with depth 5000 for (1) to (7) and 500 for (8). Timeout means taking more than 100 seconds or causing a stack overflow. | 𝑆 |max denotes the maximum size of the equality variable set during execution.

The naive implementation of the Amber rules for subtyping iso-recursive types by Cardelli [1985]. When recursive types are encountered, the algorithm will first try rule Amber-self and then rule Amber-rec when the reflexivity check fails.
The efficient implementation by Ligatti et al. [2017] for subtyping iso-recursive types, with the ability to relate between recursive types and unfoldings. We remove the ⊥ type from the algorithm as it is not considered in other algorithms. The original implementation was written as an ML program, and we rewrite it in OCaml for comparison.
The efficiently subtyping equi-recursive types algorithm described by Gapeyev et al. [2002, Figure 2]. The algorithm is considered efficient in that it only requires at most 𝑂 ( 𝑛[2] ) recursive calls by remembering a seen set of recursive subtypes throughout the computation.

All these algorithms are implemented in OCaml using the same named representation of bindings for types as Ligatti et al.. For each test, we measure the execution time on a MacBook Pro with a 2 GHz Intel Core i5 processor and 16 GB of memory. The data are collected by averaging the execution time over 10 runs, excluding the maximum and minimum values, to reduce the impact of system noise.

5.1 Simple Recursive Types

We first test QuickSub without record types to evaluate the algorithm’s asymptotic complexity and efficiency across different scenarios, including the worst case scenario (case 8). The benchmarks for testing the algorithm are sets of recursive types that follow certain patterns with different levels of recursive depth or type size. As our focus is on the performance of the algorithm, instead of relying on randomly generated types or property based testing tools such as QuickCheck [Claessen and Hughes 2000], we manually write 8 pattern generators for testing the algorithms. The patterns essentially generalize the various patterns discussed in Section 2.1. For details on how the benchmarks are generated, please refer to the extended version of the paper. To give a general idea of how each algorithm performs in different scenarios, we first evaluate QuickSub and other algorithms on a fixed large depth of recursive types for 8 different patterns, namely 500 for the worst case pattern and 5000 for others. As we will show later, the size of types in worst case pattern will grow quadratic with the depth, so we choose a smaller depth for the worst case pattern to avoid a stack overflow. The results are shown in Table 1. In each row, the algorithm that takes the least time is highlighted in bold.

The results in Table 1 show that QuickSub generally performs the best across most scenarios. Notably, it outperforms other algorithms in 5 out of the 8 cases, with the Amber rules performing

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:24

−2 100 102 e (s)		Width Depth 100 1000 2000
10−6 10−4 10 Tim	1 2 3 4 5 6 7 8 9 Depth	1 0.02144 1.10701 4.73034 10 0.19642 34.11267 Timeout 100 53.19658 Timeout Timeout 200 Timeout Timeout Timeout

Fig. 9. Equi-recursive subtyping algorithm evaluation. Left: Time (seconds measured in log scale) taken for the worst-case pattern as the recursive depth increases. Right: Time (seconds) taken for subtyping recursive record types with varying recursive depths and record widths.

better in those cases where equivalent subtyping is checked. This is not a surprise, as our Amber rule implementation always tries the reflexivity rule first. For these cases the performance of Amber rules can vary if the non-deterministic choice order between the rules for recursive types changes in the implementation. Nonetheless, in these cases QuickSub is still competitive with the Amber rules and outperforms others by a significant margin.

Substitution overhead. In equi-recursive subtyping and the nominal unfolding rules, the substitution operation becomes a significant overhead when the number of recursive variables increases. For equi-recursive subtyping, although Gapeyev et al. [2002] showed that the number of recursive calls is at most 𝑂 ( 𝑛[2] ), the substitution operation is still frequently performed when recursive types are unfolded. So, the time complexity of the algorithm in practice, when measured by the number of meta-operations, can be significantly larger than 𝑂 ( 𝑛[2] ). To illustrate this point, we conduct a small experiment on the worst case pattern (case 8) with depth ranging from 1 to 10, as shown in the left plot of Figure 9. The results show that as the depth increases, the time taken by the equi-recursive subtyping algorithm grows exponentially, and a depth of 10 recursive variables already leads to a timeout.

For the nominal unfolding rules, substitution leads to a timeout in many patterns. The complete algorithm implementation by Ligatti et al. [2017] avoids this with an unroll table, but it remains unknown whether this design can be adapted to other subtyping rules. Both QuickSub and the Amber rules are not affected by the substitution overhead due to their algorithm design.

Worst case. It is worth noting that Table 1 also records the maximum size of the equality variable set | 𝑆 |max during the execution of QuickSub. Since the equality variable set operation is the main bottleneck of QuickSub, the size of this set can be a good indicator of the scenario where the algorithm performs the worst. For cases (1) to (6), the size is constant 0 or 1, since they follow a pattern where inner recursive types do not refer to outer recursive variables, as illustrated in Figure 10a. Nested recursive types are not problematic when they appear positively. Case (7) captures this pattern, which is illustrated in Figure 10b. When variables occur negatively and the subtyping result is equality ≈, all of the variables need to be added to the equality variable set. We test such a scenario in case (8), which basically compares a reflexive relation for types with a pattern shown in Figure 10c. The results show that QuickSub is still able to handle such a worst case scenario. Note that to achieve this, QuickSub needs to be optimized using the imperative boolean array technique, as discussed earlier. In contrast, the functional version of QuickSub, which uses the standard OCaml Set module for equality variable sets, takes 4.78 seconds for case (8) in Table 1.

Overall, QuickSub remains consistently efficient, demonstrating strong performance across various recursive type patterns.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:25

class A {	class A {
foo(Nat) : A	foo(Nat) : A	𝜇𝛼_1._	𝛼_1 →(𝜇𝛼_2.
…	…	_𝛼_1	→_𝛼_2 →(𝜇𝛼_3._
class B {	class B {		𝛼_1 →_𝛼_2 →_𝛼_3 →(𝜇𝛼_4.
bar(Real) : B	bar(Real) : A	…
}}	}}	…)))
(a) Simple Recursive Objects	(b) Nested Recursive Objects	(c) Worst Case Patern

Fig. 10. Illustrations of worst case pattern and corresponding objects.

----- Start of picture text -----
QuickSub Amber Complete
3 6
2 4
1 2
0 0
1 , 000 2 , 000 3 , 000 4 , 000 5 , 000 1 , 000 2 , 000 3 , 000 4 , 000 5 , 000
Depth Depth
Test (3) Proving simple negative subtyping Test (4) Disproving positive subtyping
0 . 8 6
0 . 6
4
0 . 4
2
0 . 2
0 0
1 , 000 2 , 000 3 , 000 4 , 000 5 , 000 1 , 000 2 , 000 3 , 000 4 , 000 5 , 000
Depth Depth
Test (6) Proving mixed tests Test (7) Proving nested positive subtyping
Time (s) Time (s)
Time (s) Time (s)
----- End of picture text -----

Fig. 11. Comparison of different works across multiple tests

Time complexity, empirically. Next, to reveal the time complexity of QuickSub and other algorithms, we fix the pattern and vary the depth of recursive types. We plot the results in Figure 11 for testing cases (3), (4), (6) and (7), which are all non-trivial cases (compared to reflexivity cases) that are commonly encountered in practice.

The results in Figure 11 show that QuickSub demonstrates a linear complexity trend across all tested scenarios. We do not present the results for the nominal unfolding rules or the equi-recursive algorithm as they time out or take a long time in all these selected cases. In all these cases, the performance of QuickSub is consistently better than other algorithms, with the execution time increasing linearly as the depth of recursive types increases, while other algorithms exhibit a steeper linear or even quadratic growth in execution time.

5.2 Subtyping Record Types

Next, we focus on scenarios frequently encountered in practical programming, where record types are used to encode objects or data structures. To evaluate how well the algorithms manage such

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:26

Test No.	QuickSub{}	Amber	Equi	Complete	Description
1	0.0124	0.0822	Timeout	3.5369	Disprove positive subtyping
2	0.0609	0.0758	Timeout	0.8942	Disprove negative subtyping
3	0.1051	4.1899	Timeout	5.7472	Prove positive subtyping
4	0.1147	4.2414	Timeout	0.9660	Prove negative subtyping with⊤types

Table 2. Runtime results (seconds) for subtyping record types (depth = 100, width = 1000). Timeout means taking more than 100 seconds or causing a stack overflow.

structures, we conducted tests on benchmarks that contain record types extending in both width and recursive depths. The detailed methodology for generating these benchmarks is discussed in the extended version of the paper. These benchmarks are designed to simulate realistic conditions, reflecting common patterns as also noted in related work on optimizing iso-recursive subtyping in practical settings like WebAssembly [Rossberg 2023], who observed that even with shallow recursive depths, nested record types can cause significant performance overhead for subtyping algorithms. Here, recursive record types typically involve a large number of fields with a relatively shallow recursive depth.

Evaluation Setup. We have already discussed extending QuickSub to QuickSub[{}] for supporting record types in Section 4. As for the other algorithms, we extend the nominal unfolding rules [Zhou et al. 2022b] and Ligatti et al. [2017]’s rules with an extra case for pointwisely comparing the fields of the record types. The extension to the Amber rules is more involved, as the algorithm relies on a reflexivity check to handle subtyping between recursive types. We extend the syntactic reflexivity check to a more generalized check that allows permutations of the fields in the record types, which leads to a slight cost in performance.

Overall Performance. We first fix the depth of the recursive types to 100 and the width of the record types to 1000 and test QuickSub[{}] against other algorithms over four scenarios. The results are shown in Table 2. Our evaluations reveal that QuickSub[{}] consistently performs best.

Scalability of QuickSub[{}] . We next extend our testing to benchmarks with varying widths and depths, focusing particularly on case (3) in Table 2 as it represents the most typical and practical scenario. We omit the results for the nominal unfolding rules and present the results for the equi-recursive algorithm in the right table of Figure 9 alone as they take significantly longer to complete compared to other algorithms or time out. The results, illustrated in Figure 12, show minimal differences in runtime among all algorithms when the depth is 1, reflecting a computational complexity of 𝑂 ( 𝑚 ), where 𝑚 denotes the type size. However, as the recursive depth increases, QuickSub[{}] starts to show significant advantages. For example, at a depth of 10, QuickSub[{}] already outperforms other algorithms when the record type has a certain number of fields. The margin of improvement becomes more pronounced as the depth increases, as can be seen by the increasing time scale in the four subplots. In practical programming tasks, where the definition of one object often relies on another, it is common to have nested recursive structures with a large number of fields to be compared, as we have shown in Figure 10. Our analysis shows that in such cases, QuickSub[{}] will demonstrate notable efficiency and scalability advantages over other algorithms.

Iso-recursive subtyping. We have reviewed the most related work on subtyping iso-recursive types in the overview, such as the iso-recursive Amber rules [Cardelli 1985], the nominal unfolding rules [Zhou et al. 2022b], and the complete subtyping rules [Ligatti et al. 2017]. While for this

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:27

----- Start of picture text -----
Complete Amber QuickSub
1 . 2 [·][10][−][2] 0 . 15
0 . 9
0 . 1
0 . 6
0 . 05
0 . 3
0 0
100 500 1 , 000 1 , 500 2 , 000 100 500 1 , 000 1 , 500 2 , 000
Record Width Record Width
Depth = 1 Depth = 10
12 80
60
8
40
4
20
0 0
100 500 1 , 000 1 , 500 2 , 000 100 500 1 , 000 1 , 500 2 , 000
Record Width Record Width
Depth = 100 Depth = 200
Time (s) Time (s)
Time (s) Time (s)
----- End of picture text -----

Fig. 12. Runtime results (seconds) for different algorithms with varying benchmark sizes in depth and width.

paper we have focused on efficiency and have shown that QuickSub has significant advantages in terms of performance, there are some other considerations that we have not discussed. For instance, an advantage of the nominal unfolding rules, compared to all other iso-recursive formulations (including QuickSub) is the modularity of the rules and proofs. That is, the nominal rules do not require changes to pre-existing rules (such as subtyping for functions) and they do not also require changes to proof cases that are not related to recursive types. QuickSub does not share this advantage and it does require changes to other rules, and cases that are not related to recursive types in the proofs. Nonetheless we have shown that QuickSub still allows us to develop the relevant metatheory without relying on other formulations of iso-recursive subtyping.

There are other alternative formulations for iso-recursive subtyping as well. Hofmann and Pierce [1995] introduced a subtyping relation that limits recursive subtyping to covariant types only. In other words, only functions with same input types can be related by subtyping, which makes their rules more restrictive than the Amber rules. Hosoya et al. [1998] restricted the recursive types to be top-level datatype declarations only, and formulated a subtyping relation that deals with mutually recursive declarations. However, this approach moves away from the standard conventional operational semantics and subtyping rules for recursive types as the rules rely on a special list of subtyping assumptions. Recently, Rossberg [2023] developed a calculus for higherorder declared subtyping with a standard formulation of iso-recursive types and subtyping, which effectively handles mutually recursive types without falling back to encodings of quadratic size as in the classic Amber rules. They observe that in practice, especially for languages more focused on nominal typing, the full power of equi-recursive subtyping or even iso-recursive subtyping is not needed. By restricting possible supertypes of recursive types to only types that have been declared to be in a subtyping relation, they can check the subtyping of recursive types only once when declaring the recursive types. In contrast, with general equi- or iso-recursive types, the recursive subtyping check needs to be done whenever needed. Compared to the line of work on declared

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:28

subtyping, we focus on the latter case, where the full power of iso-recursive subtyping is available, which could be helpful in languages with some form of structural typing.

Implementing iso-recursive subtyping. Some variants of iso-recursive subtyping already come with an algorithm for checking subtyping with efficiency in mind. For instance, both the complete subtyping rules [Ligatti et al. 2017] and the mutually iso-recursive subtyping rules [Rossberg 2023] have efficient algorithms. However, Ligatti et al. only presented their algorithm as an ML program and argued informally about the correspondence to his proposed complete rules (see also Section 2.1). In contrast, we formalize our algorithm as a set of inference rules and have formal results for the correctness of the algorithm in Section 3.2. For Amber-style subtyping, there are various algorithmic variants [Zhou et al. 2022b]. However, these variants were not designed for efficiency, but to help with theoretical issues. For example, the weakly positive rules that we discussed in Section 3.2, still rely on built-in reflexivity rule PosRes-self to ensure that the subtyping relation is reflexive for negative recursive types. Thus, a non-deterministic choice of the rules has to be made, requiring backtracking in an algorithm. Cardelli [1993] considered a recursive subtyping algorithm that is claimed to be equivalent to the iso-recursive Amber rules. As we discussed in Section 2.1, a formal proof of equivalence is missing, and due to the “tie” computation, and the way it checks equivalence by running twice the subtyping algorithm, the algorithm itself is not as efficient as QuickSub.

Equi-recursive types. Equi-recursive types, where a recursive type is considered as an infinite tree and equal to its unfoldings, also have a long history in the literature. They are widely used in various calculi and programming languages. Amadio and Cardelli [1993] laid the groundwork for equi-recursive subtyping, later refined by Brandt and Henglein [1998]; Gapeyev et al. [2002]; Kozen et al. [1993]. Equi-recursive types are used in session types [Castagna et al. 2009; Chen et al. 2014; Gay and Hole 2005; Gay and Vasconcelos 2010], gradual typing [Siek and Tobin-Hochstadt 2016], Scala’s Dependent object types (DOT) calculus [Amin et al. 2016; Rompf and Amin 2016], and so on. There have also been efforts to adapt equi-recursive subtyping algorithms to more advanced type systems, where the general equi-recursive subtyping problem is impractical or undecidable. A recent effort in this direction was made by DeYoung et al. [2024], who have shown that equirecursive subtyping with parametric polymorphism and recursively defined type constructors is undecidable. However it is still possible to obtain a sound (but incomplete) algorithm that works well in practice.

The relation between iso-recursive and equi-recursive types has also been studied in the literature [Abadi and Fiore 1996; Patrignani et al. 2021; Urzyczyn 1995; Zhou et al. 2024]. Notably, Abadi and Fiore argued that by inserting coercion functions, equi-recursive types can be encoded as iso-recursive types and vice versa. Thus, the two formulations have the same expressive power. Patrignani et al. further proved that the transformation from iso-recursive types to equi-recursive types, by erasing the unfold and fold operators, is fully abstract with respect to contextual equivalence. Abadi and Fiore’s encoding of equi-recursive types via iso-recursive types has an important drawback: the coercion functions employed in the encoding are computationally relevant. Zhou et al. presented a new formulation of iso-recursive types, called full iso-recursive types, that enables encoding all equi-recursive programs without computational overhead. This is achieved by generalizing fold and unfold operations to computationally irrelevant casts, that can replace the coercions in Abadi and Fiore’s work. Their results also extend to subtyping, which previous works have not considered. The subtyping rules used in their 𝜆𝐹𝑖[𝜇][<][:][calculus are based on the iso-recursive] Amber rules, which means that QuickSub can be directly applied to their calculus and obtain a more efficient version of full iso-recursive subtyping.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

QuickSub: Efficient Iso-Recursive Subtyping

33:29

Additionally, it is important to identify the different expressiveness results in the literature and their implications. Specifically, in terms of the expressive power of the subtyping relation, we have the iso-recursive Amber rules, which are less expressive than the complete rules by Ligatti et al. [2017], which in turn are less expressive than equi-recursive subtyping. However, the results by Abadi and Fiore [1996]; Zhou et al. [2024] show that by having more annotations (casts) or coercions in the term language, we can bridge this expressive power gap. Furthermore, Zhou et al. show that this can be done without any runtime performance cost with their full iso-recursive types. As implied by Zhou et al. and Amadio and Cardelli [1993], equi-recursive subtyping to some extent mixes the coinductive, infinite-tree view of recursive type equality with the inductive, finite-tree view of recursive subtyping. The two can be decomposed if needed. For example, let 𝐴 = nat →( 𝜇𝛼. ⊤→ 𝛼 ) and 𝐵 = 𝜇𝛼. nat →⊤→ 𝛼 , then the equi-recursive subtyping 𝐴 ≤ 𝑒 𝐵 is decomposed as follows:

𝐴 = 𝑒 nat →⊤→( 𝜇𝛼. ⊤→⊤→ 𝛼 ) ≤ nat →⊤→( 𝜇𝛼. nat →⊤→ 𝛼 ) = 𝑒 𝐵

where = 𝑒 denotes the coinductive equi-recursive equality relation and ≤ is an Amber-style isorecursive subtyping relation. In such scenarios, the iso-recursive subtyping part can be replaced by any equivalent set of rules, such as our QuickSub rules, and the equi-recursive expressive power can be recovered by other means, such as casts or coercions.

Mechanized proofs on recursive types. Amber-style iso-recursive subtyping rules were only recently mechanized in proof assistants by Zhou et al. [2020, 2022b]. They formalize the Amber rules, nominal unfolding rules, and the weakly positive rules and prove several properties and equivalence results between them in Coq. Our work aligns closely with these efforts, by formalizing the equivalence proof of QuickSub to their rules and the type soundness proof in Coq. There are a few works on mechanizing other variants of recursive subtyping. Appel and Felty [2000]; Backes et al. [2014] formalized subtyping relations for iso-recursive types in Coq, focusing on positive subtyping. Amin and Rompf [2017]’s formalization of DOT involves a special form of equi-recursive types. Patrignani et al. [2021] formalized three calculi in Coq: a simply typed lambda calculus extended with iso-recursive types, equi-recursive types, and term-level fixpoints and showed several contextual equivalence results between them. Zhou et al. [2024] formalized their full iso-recursive types in Coq and adopted Zhou et al. [2022b]’s formalization for subtyping iso-recursive types.

7 Conclusion

In this paper, we introduce QuickSub, a novel efficient algorithm for iso-recursive subtyping. We show its correctness by proving its equivalence to the well-known Amber rules. We also show a direct type soundness proof for a calculus with QuickSub. Our OCaml implementation, accompanied by empirical evaluations, shows that QuickSub significantly outperforms existing algorithms, particularly in practical scenarios involving positive subtyping and nested recursive types. We also extend QuickSub to handle record types, broadening its applicability. Future work includes extending QuickSub to incorporate additional features and providing a direct equivalence proof for QuickSub[{}] with existing systems, such as the nominal unfolding rules. Furthermore, we plan to leverage full iso-recursive types [Zhou et al. 2024] to encode equi-recursive subtyping, and enhance the algorithm’s expressiveness and efficiency in more complex type systems.

Data Availability Statement

The QuickSub formalization, implementation and evaluation examples are openly available in Zenodo [Zhou and Oliveira 2024] and https://github.com/ltzone/QuickSub.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:30

Acknowledgments

We are grateful to the anonymous reviewers for their valuable comments. This work has been sponsored by Hong Kong Research Grant Council project number 17209821.

References

Martin Abadi and Luca Cardelli. 1996. A theory of objects . Springer Science & Business Media. https://doi.org/10.1007/9781-4419-8598-9

Martin Abadi and Marcelo P Fiore. 1996. Syntactic considerations on recursive types. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science . IEEE, 242–252. https://doi.org/10.1109/LICS.1996.561324 Roberto M Amadio and Luca Cardelli. 1993. Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS) 15, 4 (1993), 575–631. https://doi.org/10.1145/155183.155231

Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (2016), 249–272. https://doi.org/10.1007/978-3-319-30936-1_14

Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages . 666–679. https://doi.org/10.1145/3009837.3009866

Andrew W Appel and Amy P Felty. 2000. A semantic model of types and machine instructions for proof-carrying code. In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages . 243–253.

Michael Backes, Cătălin Hriţcu, and Matteo Maffei. 2014. Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations. J. Comput. Secur. 22, 2 (mar 2014), 301–353.

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D Gordon, and Sergio Maffeis. 2011. Refinement types for secure implementations. ACM Transactions on Programming Languages and Systems (TOPLAS) 33, 2 (2011), 1–45. https://doi.org/10.1145/1890028.1890031

Michael Brandt and Fritz Henglein. 1998. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae 33, 4 (1998), 309–338. https://doi.org/10.3233/FI-1998-33401

Luca Cardelli. 1985. Amber, Combinators and Functional Programming Languages. Proc. of the 13th Summer School of the LITP, Le Val D’Ajol, Vosges (France) (1985). Luca Cardelli. 1993. An implementation of 𝐹< :. Digital Equipment Corporation Systems Research Center. Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. Comput. Surveys 17 (Dec. 1985), 471–522. https://doi.org/10.1145/6041.6042

Felice Cardone and Mario Coppo. 1991. Type inference with recursive types: Syntax and semantics. Information and Computation 92, 1 (1991), 48–80. https://doi.org/10.1016/0890-5401(91)90020-3

Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. 2009. Foundations of session types. In Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming . 219–230. https://doi.org/10.1145/1599410.1599437

Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2014. On the preciseness of subtyping in session types. In Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming . 135–146. https://doi.org/10.1145/2643135.2643138

Ravi Chugh. 2015. IsoLATE: A type system for self-recursion. In Programming Languages and Systems: 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 24 . Springer, 257–282. https://doi.org/10.1007/978-3-662-46669-8_11

Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the fifth ACM SIGPLAN international conference on Functional programming . 268–279. https://doi.org/10.1145/351240. 351266

Dario Colazzo and Giorgio Ghelli. 2005. Subtyping recursion and parametric polymorphism in kernel fun. Information and Computation 198, 2 (2005), 71–147. https://doi.org/10.1016/j.ic.2004.11.003

Mario Coppo. 1985. A completeness theorem for recursively defined types. In International Colloquium on Automata, Languages, and Programming . Springer, 120–129. https://doi.org/10.1007/BFb0015737 The Coq Development Team. 2024. The Coq Proof Assistant . https://doi.org/10.5281/zenodo.11551307 Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a recursive module?. In Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation . 50–63. https://doi.org/10.1145/301618.301641

Nils Anders Danielsson and Thorsten Altenkirch. 2010. Subtyping, declaratively: An exercise in mixed induction and coinduction. In Mathematics of Program Construction: 10th International Conference, MPC 2010, Québec City, Canada, June 21-23, 2010. Proceedings 10 . Springer, 100–118. https://doi.org/10.1007/978-3-642-13321-3_8

Nicolaas Govert De Bruijn. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In Indagationes mathematicae (proceedings) , Vol. 75. Elsevier,

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

33:31

QuickSub: Efficient Iso-Recursive Subtyping

381–392. Henry DeYoung, Andreia Mordido, Frank Pfenning, and Ankush Das. 2024. Parametric Subtyping for Structural Parametric Polymorphism. 8, POPL (2024). Derek Dreyer. 2005. Understanding and Evolving the ML Module System . Ph. D. Dissertation. School of Computer Science, Carnegie Mellon University. Derek R. Dreyer, Robert Harper, and Karl Krary. 2001. Toward a Practical Type Theory for Recursive Modules . Technical Report CMU-CS-01-112. School of Computer Science, Carnegie Mellon University. Dominic Duggan. 2002. Type-safe linking with recursive DLLs and shared libraries. ACM Transactions on Programming Languages and Systems (TOPLAS) 24, 6 (2002), 711–804. https://doi.org/10.1145/586088.586093 Vladimir Gapeyev, Michael Y Levin, and Benjamin C Pierce. 2002. Recursive subtyping revealed. Journal of Functional Programming 12, 6 (2002), 511–548. https://doi.org/10.1017/S0956796802004318 Simon Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. Acta Informatica 42 (2005), 191–225. https://doi.org/10.1007/s00236-005-0177-z Simon J Gay and Vasco T Vasconcelos. 2010. Linear type theory for asynchronous session types. Journal of Functional Programming 20, 1 (2010), 19–50. https://doi.org/10.1017/S0956796809990268 Giorgio Ghelli. 1993. Recursive types are not conservative over F≤. In International Conference on Typed Lambda Calculi and Applications . Springer, 146–162. https://doi.org/10.1007/BFb0037104 Robert Harper. 2016. Practical foundations for programming languages . Cambridge University Press. https://doi.org/10. 1017/CBO9781316576892 Martin Hofmann and Benjamin Pierce. 1995. Positive subtyping. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages . 186–197. Haruo Hosoya, Benjamin C Pierce, David N Turner, et al. 1998. Datatypes and subtyping. Unpublished manuscript. Available http://www.cis.upenn.edu/ bcpierce/papers/index.html (1998). Alan Jeffrey. 2001. A symbolic labelled transition system for coinductive subtyping of F 𝜇 ≤ types. In 2001 IEEE Conference on Logic and Computer Science (LICS 2001) , Vol. 323. Dexter Kozen, Jens Palsberg, and Michael I Schwartzbach. 1993. Efficient recursive subtyping. In Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages . 419–428. https://doi.org/10.1145/158511.158700 Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. 2015. A theory of tagged objects. In 29th European Conference on Object-Oriented Programming (ECOOP 2015) . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2021. The OCaml System, Release 4.12, Documentation and User’s Manual . https://ocaml.org/manual/4.12/index.html Accessed: 2024-07-06. Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. 2017. On subtyping-relation completeness, with an application to

iso-recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS) 39, 1 (2017), 1–36. https: //doi.org/10.1145/2994596

James H Morris. 1968. Lambda calculus models of programming languages. (1968).

Ulf Norell. 2007. Towards a practical programming language based on dependent type theory . Ph. D. Dissertation. Chalmers University of Technology.

Marco Patrignani, Eric Mark Martin, and Dominique Devriese. 2021. On the semantic expressiveness of recursive types. Proceedings of the ACM on Programming Languages 5, POPL (2021), 1–29. https://doi.org/10.1145/3434302 Benjamin C Pierce. 2002. Types and programming languages . MIT press.

Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications . 624–641. https://doi.org/10.1145/2983990.2984008

Andreas Rossberg. 2023. Mutually Iso-Recursive Subtyping. Proceedings of the ACM on Programming Languages 7, OOPSLA2 (2023), 347–373. https://doi.org/10.1145/3622809

Claudio V. Russo. 2001. Recursive Structures for Standard ML. In Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP ’01), Firenze (Florence), Italy, September 3-5, 2001 , Benjamin C. Pierce (Ed.). ACM, 50–61.

Jeremy G Siek and Sam Tobin-Hochstadt. 2016. The recursive union of some gradual types. In A List of Successes that can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday . Springer, 388–410. https://doi.org/10.1007/978-3-319-30936-1_21

Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed programming with value-dependent types. ACM SIGPLAN Notices 46, 9 (2011), 266–278. https://doi.org/10.1145/2034574. 2034811

Pawel Urzyczyn. 1995. Positive recursive type assignment. In International Symposium on Mathematical Foundations of Computer Science . Springer, 382–391.

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Litao Zhou and Bruno C. d. S. Oliveira

33:32

Litao Zhou and Bruno C. d. S. Oliveira. 2024. QuickSub: Efficient Iso-Recursive Subtyping (Artifact) . https://doi.org/10.5281/ zenodo.13906402

Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira. 2024. Full Iso-Recursive Types. Proc. ACM Program. Lang. 8, OOPSLA2, Article 278 (Oct. 2024), 30 pages. https://doi.org/10.1145/3689718

Litao Zhou, Yaoda Zhou, and Bruno C d S Oliveira. 2023. Recursive Subtyping for All. Proceedings of the ACM on Programming Languages 7, POPL (2023), 1396–1425. https://doi.org/10.1145/3571241

Yaoda Zhou, Bruno C d S Oliveira, and Andong Fan. 2022a. A Calculus with Recursive Types, Record Concatenation and Subtyping. In Asian Symposium on Programming Languages and Systems . Springer, 175–195. https://doi.org/10.1007/9783-031-21037-2_9

Yaoda Zhou, Bruno C d S Oliveira, and Jinxu Zhao. 2020. Revisiting iso-recursive subtyping. Proceedings of the ACM on Programming Languages 4, OOPSLA (2020), 1–28. https://doi.org/10.1145/3428216

Yaoda Zhou, Jinxu Zhao, and Bruno CDS Oliveira. 2022b. Revisiting Iso-recursive subtyping. ACM Transactions on Programming Languages and Systems (TOPLAS) 44, 4 (2022), 1–54. https://doi.org/10.1145/3549537

Received 2024-07-10; accepted 2024-11-07

Proc. ACM Program. Lang., Vol. 9, No. POPL, Article 33. Publication date: January 2025.

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

Tony's Wiki

Explorer

QuickSub: Efficient Iso-Recursive Subtyping

QuickSub: Efficient Iso-Recursive Subtyping

Metadata

Why this note exists

Extraction quality note

Technical landmarks detected automatically

Full converted paper text

QuickSub: Efficient Iso-Recursive Subtyping

CCS Concepts: • Theory of computation → Type theory ; • Software and its engineering → Object oriented languages .

ACM Reference Format:

1 Introduction

2 Overview

2.1 Subtyping Iso-Recursive Types

2.2 Algorithmic Iso-Recursive Subtyping

2.3 Key Ideas Towards an Efficient Algorithm

3 Efficient Subtyping Algorithm

3.1 QuickSub Subtyping

3.2 Correctness

3.3 Direct Proof of Type Soundness

4 Extension to Records

4.1 Record Subtyping

4.2 A Calculus with QuickSub[{}]

5 Evaluation

Fig. 8. Functional implementation of QuickSub

5.1 Simple Recursive Types

5.2 Subtyping Record Types

7 Conclusion

Data Availability Statement

Acknowledgments

References

Graph View

Table of Contents

Backlinks

Tony's Wiki

Explorer

QuickSub: Efficient Iso-Recursive Subtyping

QuickSub: Efficient Iso-Recursive Subtyping

Metadata

Why this note exists

Extraction quality note

Technical landmarks detected automatically

Full converted paper text

QuickSub: Efficient Iso-Recursive Subtyping

CCS Concepts: • Theory of computation → Type theory ; • Software and its engineering → Object oriented languages .

ACM Reference Format:

1 Introduction

2 Overview

2.1 Subtyping Iso-Recursive Types

2.2 Algorithmic Iso-Recursive Subtyping

2.3 Key Ideas Towards an Efficient Algorithm

3 Efficient Subtyping Algorithm

3.1 QuickSub Subtyping

3.2 Correctness

3.3 Direct Proof of Type Soundness

4 Extension to Records

4.1 Record Subtyping

4.2 A Calculus with QuickSub[{}]

5 Evaluation

Fig. 8. Functional implementation of QuickSub

5.1 Simple Recursive Types

5.2 Subtyping Record Types

6 Related Work

7 Conclusion

Data Availability Statement

Acknowledgments

References

Graph View

Table of Contents

Backlinks