一句话：提出基于上下文等价的纯度语义基线与完备度表达力度量，证明效应与能力系统不可比较，并综合出兼具优势的类型-能力-效应系统。
该论文关注纯计算与带效应交互的分离问题。现有 monad、类型与效应系统、能力系统等方案在精度与可用性之间存在张力，且优缺点不显。作者首先受上下文等价启发，提出纯度的语义定义，作为独立于具体类型规则的效应可靠性基线；其次提出以完备度衡量表达力，即多少语义纯的项可被类型化为纯。基于该度量，论文比较最小的有意义效应系统与能力系统，证明二者在表达力上不可比较。进而提出一种综合方案，使类型、能力与效应系统取长补短。形式模型中还给出逻辑关系，以支持纯度等性质的证明。
Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation include monads, type-and-effect systems, and capability systems. All share a tension between precision and usability, and each one has non-obvious strengths and weaknesses. This paper aims to raise the bar in assessing such systems. First, we propose a semantic definition of purity, inspired by contextual equivalence, as a baseline for effect soundness independent of any specific typing discipline. Second, we propose that expressiveness should be measured by the degree of completeness, i.e., how many semantically pure terms can be typed as pure. Using this measure, we focus on minimal meaningful effect and capability systems and show that they are incomparable, i.e., neither subsumes the other in terms of expressiveness. Based on this result, we propose a synthesis and show that type, ability, and effect systems combine their respective strengths while avoiding their weaknesses. As part of our formal model, we provide a logical relation to facilitate proofs of purity and other properties for different effect typing disciplines.
@article{paperbot12075,
title = {Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness},
author = {Yuyan Bao and Tiark Rompf},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839518}
}