¶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 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.

¶Related

[Zhou2022] A Calculus with Recursive Types, Record Concatenation and Subtyping