Recursive Subtyping for All

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 presents an extension of kernel F-<= =, called F-<=(mu) , with iso-recursive types. F-<= is a well-known polymorphic calculus with bounded quantification. In F-<=(mu) we add iso-recursive types, and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. We also add two smaller extensions to F-<=. The first one is a generalization of the kernel F-<= rule for bounded quantification that accepts equivalent rather than equal bounds. The second extension is the use of so-called structural folding/unfolding rules, inspired by the structural unfolding rule proposed by Abadi, Cardelli, and Viswanathan [1996]. The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity and decidability of subtyping; the conservativity of F-<=(mu) over F-<= and a sound and complete algorithmic formulation of F-<=(mu). Moreover, we study an extension of F-<=(mu), called F-<=>=(mu) which includes lower bounded quantification in addition to the conventional (upper) bounded quantification of F-<=. All the results in this paper have been formalized in the Coq theorem prover.