Iso-recursive subtyping : new theory and extensions

Abstract

The Amber rules are well-known and widely used for subtyping iso-recursive types. They were first briefly and informally introduced in 1985 by Luca Cardelli in a manuscript describing the Amber language. Despite their use over many years, important aspects of the metatheory of the iso-recursive style Amber rules have not been studied in depth or turn out to be quite challenging to formalize.

This dissertation proposes a new theory of iso-recursive subtyping. After revisiting the problem of subtyping iso-recursive types, we introduce a novel declarative specification for Amber-style iso-recursive subtyping. Informally, the specification states that two recursive types are subtypes if all their finite unfoldings are subtypes. With the help of intermediate weakly positive subtyping rules, the Amber rules are shown to be sound and complete with respect to this declarative specification. We then show two variants of sound, complete and decidable algorithmic formulations of subtyping that employ the idea of double unfoldings. Compared to the Amber rules, the double unfolding rules have the advantage of: (1) being modular; (2) not requiring reflexivity to be built-in; (3) leading to an easy proof of transitivity of subtyping; and (4) being easily applicable to subtyping relations that are not antisymmetric. As far as we know, this is the first comprehensive treatment of iso-recursive subtyping dealing with unrestricted recursive types in a theorem prover.

The new formulations not only shed new insights on the theory of subtyping iso-recursive types, but they also enable extensions with more complex features. We show three extensions in this thesis. Firstly, at the type level, we present an extension with record types and intersection types, showing how our new formulations can be applied non-antisymmetric subtyping. Secondly, at the term level, we apply it to a record calculus with merge operators, solving a current open problem for such calculi of how to support recursive types and the binary methods. Finally, we combine iso-recursive types with bounded quantification conservatively, and show that such integration is helpful to encode positive f-bounded polymorphism and subtyping between algebraic datatypes.