一句话：提出基于布尔代数的类型限定符，扩展 System F<: 并奠定 Flix 效果系统的形式基础。
传统带类型限定符的系统多基于格，难以表达排除关系。论文主张布尔代数能自然表达排除，是限定符的实用域，并提出 System F<:B：在 System F<: 上增加布尔代数限定符，支持否定、限定符多态和子限定。作者进一步给出类型与效果系统设计配方 System F<:BE，支持效果多态、子效果及多态效果排除，并用其为 Flix 语言的效果系统建立形式基础。实现层面提出并实现 abstraction-site subeffecting 这一实用子效果形式。实验表明，该机制可消除当前 Flix 标准库中的所有效果上转（effect upcasts）。
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}
}