Generalised Type Preprocessing for Integrated Subtyping

Abstract

Subtyping is a common feature that organises types into hierarchies, which is used for encoding various forms of polymorphism. Subtype relations are typically defined syntactically using axioms and inference rules, but they do not always directly translate to a decision procedure. Therefore, in addition to a declarative system that consists of more modular and intuitive rules, it is a normal practice to devise an equivalent reductive system that corresponds to an algorithm. However, some desirable relations, such as distributivity, cannot be easily incorporated into the latter. This work presents the integrated subtyping framework. Upon standardising the methodology to prove equivalence between declarative and reductive subtyping, we present a systematic way to extend subtyping systems through a type preprocessing scheme. The normalisation scheme is specified by the framework user as integrator functions. We outline a set of requirements and, in turn, offer guarantees regarding the reflexivity, transitivity, equivalence and decidability of the extended systems. With the mutually inductive design, we establish the (co)monadic properties of the integrators, abstract away complexities and decompose the obligations for the user into smaller, more manageable proof goals. Following the metatheory, we study the practical applicability of integrated subtyping with framework instantiations involving union and intersection types as well as predicative higher-rank polymorphic types, drawing reference to Scala 3’s type system. As we promote modularity and composability, the framework reduces the need for repetitive, tedious proofs. We therefore envision the framework to be a flexible tool to develop more expressive programming languages by supporting decidable subtyping, which is increasingly significant for features such as gradual typing. Show more