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_≤^µ, with iso-recursive types. 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. 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_≤^µ over F_≤; and a sound and complete algorithmic formulation of F_≤^µ. Moreover, we study an extension of F_≤^µ, called F_≤≥^µ, 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.