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.

@article{paperbot2981,
  title = {Qualified Types with Boolean Algebras},
  author = {Edward Lee and Jonathan Lindegaard Starup and Ondřej Lhoták and Magnus Madsen},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763096}
}