一句话：提出一种支持抽象、聚合与上下界层级的效果系统，并集成到 Wyvern 语言中。
通用效果系统虽已研究近四十年，但除 Java 受检异常等少数实践外，通常缺乏异常系统所具备的抽象、聚合与层次能力。本文围绕保护系统资源设计了一种有界抽象效果系统，并集成到 Wyvern 语言中。类似类型成员，Wyvern 对象可拥有效果成员：它们能抽象底层效果、支持效果聚合，并带有下界与上界，从而形成细粒度的效果层次。作者给出了该效果系统的完整形式化，证明其支持对 authority 与 attenuation 的推理，并通过一个安全相关案例研究进行评估。结果表明，该设计在编程语言设计视角下兼顾了表达力与实用性。
Effect systems have been a subject of active research for nearly four decades, with the most notable practical example being checked exceptions in programming languages such as Java. While many exception systems support abstraction, aggregation, and hierarchy (e.g., via class declaration and subclassing mechanisms), it is rare to see such expressive power in more generic effect systems. We designed an effect system around the idea of protecting system resources and incorporated our effect system into the Wyvern programming language. Similar to type members, a Wyvern object can have effect members that can abstract lower-level effects, allow for aggregation, and have both lower and upper bounds, providing for a granular effect hierarchy. We argue that Wyvern’s effects capture the right balance of expressiveness and power from the programming language design perspective. We present a full formalization of our effect-system design, showing that it allows reasoning about authority and attenuation. Our approach is evaluated through a security-related case study.
@article{paperbot1621,
title = {Bounded Abstract Effects},
author = {Darya Melicher and Anlun Xu and Valerie Zhao and Alex Potanin and Jonathan Aldrich},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {1},
year = {2022},
doi = {10.1145/3492427}
}