Title: Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness Show Chinese title

Title: 类型、能力与效果系统：关于纯粹性、语义和表达性的观点

Abstract: 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 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 a variety of effect typing disciplines. Show Chinese abstract

Abstract: 编程从纯数学计算与不纯的、涉及世界的效果交互之间的清晰分离中受益。 现有的强制这种分离的方法包括单子、类型和效果系统以及能力系统。 它们都存在精确性与可用性之间的张力，每种方法都有其不明显的优点和缺点。 本文旨在提高评估此类系统的标准。 首先，我们提出了一种基于上下文等价的纯度语义定义，作为独立于任何特定类型体系的基准。 其次，我们认为表达能力应通过完备性的程度来衡量，即有多少语义上纯的项可以被类型化为纯的。 使用这个度量，我们专注于最小有意义的效果和能力系统，并表明它们是不可比较的，即在表达能力方面，没有一个包含另一个。 基于这个结果，我们提出了一种综合方法，并表明类型、能力和效果系统结合了各自的优势，同时避免了它们的弱点。 作为我们形式模型的一部分，我们提供了一个逻辑关系，以促进对各种效果类型体系的纯度和其他属性的证明。