具有布尔代数的合格类型

《Proceedings of the ACM on Programming Languages》：Qualified Types with Boolean Algebras

提出基于布尔代数的类型限定符，突破传统格结构限制，支持否定、多态和子限定。构建System F<:B形式系统，用于设计Flix语言类型与效果系统，实现效果多态、子效果及排斥。实验表明抽象位点子效果可消除Flix标准库所有效果升级问题。

　　

摘要

我们提出了基于布尔代数的类型限定符。传统的带有类型限定符的类型系统都是基于格（lattices）构建的，但格无法表达排他关系。我们认为，允许排他关系的布尔代数是作为类型限定符的实用且合适的数学基础。

在本文中，我们提出了一个名为System F<:B的计算系统，该系统在布尔代数上扩展了原有的System F<:，并支持否定操作、限定符多态性以及子限定（subqualification）功能。我们展示了如何利用System F<:B来设计一个具有效果多态性（effect polymorphism）、子效果操作（subeffecting）以及多态效果排他性（polymorphic effect exclusion）的类型与效果系统（System F<:BE）。我们利用System F<:BE为Flix编程语言的类型与效果系统建立了形式化基础。同时，我们还实现了一种实用形式的子效果操作——即“抽象位置子效果操作”（abstraction-site subeffecting）。实验结果表明，这种抽象位置子效果操作能够消除Flix标准库中存在的所有效果提升（effect upcasts）问题。