Polymorphic Type Qualifiers

Abstract

Type qualifiers offer a simple yet effective mechanism for extending existing type systems to deal with additional constraints or safety requirements. For example, the const qualifier is a popular mechanism for annotating existing types to signify that the value in question is read-only in addition. A variable of type const int is both an integer and also cannot be written to.

While type qualifiers themselves are well-studied, polymorphism over type qualifiers remains an area less well examined. This has led to a number of ill-desired outcomes. For one, many practical systems implementing type qualifiers in their type systems simply ignore their interaction with generic types. Other systems implement polymorphism with seemingly unique and ad-hoc rules for dealing with qualifiers.

In this thesis, we show that this does not need to be the case. We start by examining three well-known qualifier systems: systems for tracking immutability, function colour, and captured variables, and show that despite their differences that they share surprising common structure. We then give a design recipe, inspired by that structure, using the mathematical structure of free lattices for modelling polymorphism over type qualifiers, to give a framework for polymorphic type qualifiers. We then show that our design recipe precisely captures this structure by recasting those three existing systems in our framework for qualifier polymorphism by free lattices. Finally, we extend type qualifiers from ranging over lattices to type qualifiers ranging over Boolean algebras, which we then use to extend an existing effect system with effect exclusion to support subeffecting as well via subqualification and subtyping.