Recursive subtyping for all

Abstract

Abstract Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala, or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification, and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as decidability , transitivity of subtyping, conservativity , and a sound and complete algorithmic formulation, has been a long-time challenge. This paper shows how to extend $F_{\le}$ with iso-recursive types in a new calculus called $F_{\le}^{\mu}$ . $F_{\le}$ is a well-known polymorphic calculus with bounded quantification. In $F_{\le}^{\mu}$ , 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_{\le}^{\mu}$ over $F_{\le}$ ; and a sound and complete algorithmic formulation of $F_{\le}^{\mu}$ . We study two variants of $F_{\le}^{\mu}$ . The first one uses an extension of the $\textrm{kernel}~F_{\le}$ (a well-known decidable variant of $F_{\le}$ ). This extension accepts equivalent rather than equal bounds and is shown to preserve decidable subtyping. The second variant employs the $\textrm{full}~F_{\le}$ rule for bounded quantification and has undecidable subtyping. Moreover, we also study an extension of the kernel version of $F_{\le}^{\mu}$ , called $F_{\le\ge}^{\mu\wedge}$ , with a form of intersection types and lower bounded quantification . All the properties from the kernel version of $F_{\le}^{\mu}$ are preserved in $F_{\le\ge}^{\mu\wedge}$ . All the results in this paper have been formalized in the Coq theorem prover.