Qualified Types with Boolean Algebras

We propose type qualifiers based on Boolean algebras. Traditional type systems with type qualifiers have been based on lattices, but lattices lack the ability to express exclusion. We argue that Boolean algebras, which permit exclusion, are a practical and useful choice of domain for qualifiers. In this paper, we present a calculus System F<:B that extends System F<: with type qualifiers over Boolean algebras and has support for negation, qualifier polymorphism, and subqualification. We illustrate how System F<:B can be used as a design recipe for a type and effect system, System F<:BE, with effect polymorphism, subeffecting, and polymorphic effect exclusion. We use System F<:BE to establish formal foundations of the type and effect system of the Flix programming language. We also pinpoint and implement a practical form of subeffecting: abstraction-site subeffecting. Experimental results show that abstraction-site subeffecting allows us to eliminate all effect upcasts present in the current Flix Standard Library.