Syntactically Restricting Bounded Polymorphism for Decidable Subtyping

Abstract

Subtyping of Bounded Polymorphism has long been known to be undecidable when coupled with contra-variance. While decidable forms of bounded polymorphism exist, they all sacrifice either useful properties such as contra-variance (Kernel F< :), or useful metatheoretic properties (F<:⊤). In this paper we show how, by syntactically separating contra-variance from the recursive aspects of subtyping in System F< :, decidable subtyping can be ensured while also allowing for both contra-variant subtyping of certain instances of bounded polymorphism, and many of System F< :’s desirable metatheoretic properties. We then show that this approach can be applied to the related polymorphism present in D< :, a minimal calculus that models core features of the Scala type system. Show more