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 <em>decidability</em>, <em>transitivity</em> of subtyping, <em>conservativity</em> and a sound and complete algorithmic formulation has been a long time challenge. </p><p>This paper presents an extension of kernel ‍<em>F</em>≤, called <em>F</em>≤µ, with iso-recursive types. <em>F</em>≤ is a well-known polymorphic calculus with bounded quantification. In <em>F</em>≤µ 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 <em>F</em>≤. The first one is a generalization of the kernel ‍<em>F</em>≤ rule for bounded quantification that accepts <em>equivalent</em> rather than <em>equal</em> bounds. The second extension is the use of so-called <em>structural</em> 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 <em>F</em>≤µ over <em>F</em>≤; and a sound and complete algorithmic formulation of <em>F</em>≤µ. Moreover, we study an extension of <em>F</em>≤µ, called <em>F</em>≤≥µ, which includes <em>lower bounded quantification</em> in addition to the conventional (upper) bounded quantification of <em>F</em>≤. All the results in this paper have been formalized in the Coq theorem prover.</p>