Recursive subtyping for all

Abstract

<p>Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification, and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability, transitivity of subtyping, conservativity, and a sound and complete algorithmic formulation, has been a long-time challenge. This paper shows how to extend F≤ with iso-recursive types in a new calculus called F≤μ. F≤ is a well-known polymorphic calculus with bounded quantification. In F≤μ, we add iso-recursive types and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. In addition, we use so-called structural folding/unfolding rules for typing iso-recursive expressions, inspired by the structural unfolding rule proposed by Abadi et al. (1996). The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity; the conservativity of F≤μ over F≤; and a sound and complete algorithmic formulation of F≤μ. We study two variants of F≤μ. The first one uses an extension of the kernel F≤ (a well-known decidable variant of F≤). This extension accepts equivalent rather than equal bounds and is shown to preserve decidable subtyping. The second variant employs the full F≤ rule for bounded quantification and has undecidable subtyping. Moreover, we also study an extension of the kernel version of F≤μ, called F≤≥μ∧, with a form of intersection types and lower bounded quantification. All the properties from the kernel version of F≤μ are preserved in F≤≥μ∧. All the results in this paper have been formalized in the Coq theorem prover.</p>