一句话：提出 System C，将能力与效果系统统一起来，并用盒式值恢复二等值限制，支持完整效应处理器并证明可靠性。
许多实际应用需要推理外部资源的使用。效应系统能把此类信息记录在类型中，却常使常见函数签名复杂化；能力（capabilities）配合逃逸分析可提供安全且自然的签名，但往往粒度过粗且限制过强。本文提出 System C，它在基于类型的逃逸分析思想之上进行推广，表明能力与效应可以协调统一。其核心是假设所有函数均为二等值，从而允许许多常见程序拥有自然签名；同时引入盒式值（boxed values）以突破二等值限制，代价是需要在类型中跟踪不纯度信息。System C 足以完整支持效应处理器（effect handlers）。作者通过实现进行实际评估，并证明了系统的可靠性。
Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present System C, which builds on and generalizes ideas from type-based escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are second class, we can admit natural signatures for many common programs. By introducing a notion of boxed values, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate System C in an implementation and prove its soundness.
@article{paperbot1524,
title = {Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back},
author = {Jonathan Immanuel Brachthäuser and Philipp Schuster and Edward Lee and Aleksander Boruch-Gruszecki},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527320}
}