一句话：提出 System Capless 与 reach capabilities，使捕获类型能跟踪泛型数据结构内的能力，并在 Scala 3 中实现与验证。
Scala 的捕获类型（capturing types）把静态效应与资源跟踪同对象能力统一起来，但无法命名泛型数据结构（box）内嵌的能力，因而难以扩展到标准集合库。本文提出 System Capless，将全能能力细化为带存在与全称捕获集量化的新方案，并引入 reach capabilities（rcaps）来命名「盒中之物」：rcaps 见证泛型类型盒内存在量化的捕获集，而无须在表层语言暴露存在捕获类型。作者在 Lean 中完整机械化其元理论，证明类型健全性与作用域安全性，并通过类型保持翻译保证其支持原有捕获类型的轻量记号，同时提供可选的显式捕获集量化以增强表达力。最后在 Scala 3 中基于 System Capless 重新实现捕获检查，迁移整个 Scala 集合库与一个异步编程库。结果表明，rcaps 使生产代码能以极小改动与极低（多数为零）的记号开销采用捕获检查。
Capturing types in Scala unify static effect and resource tracking with object capabilities, enabling lightweight effect polymorphism with minimal notational overhead. However, their expressiveness has been insufficient for tracking capabilities embedded in generic data structures, preventing them from scaling to the standard collections library - an essential prerequisite for broader adoption. This limitation stems from the inability to name capabilities within the system's notion of box types. This paper develops System Capless, a new foundation for capturing types that provides the theoretical basis for reach capabilities (rcaps), a novel mechanism for naming "what's in the box". The calculus refines the universal capability notion into a new scheme with existential and universal capture set quantification. Intuitively, rcaps witness existentially quantified capture sets inside the boxes of generic types in a way that does not require exposing existential capture types in the surface language. We have fully mechanized the formal metatheory of System Capless in Lean, including proofs of type soundness and scope safety. System Capless supports the same lightweight notation of capturing types plus rcaps, as certified by a type-preserving translation, and also enables fully optional explicit capture-set quantification to increase expressiveness. Finally, we present a full reimplementation of capture checking in Scala 3 based on System Capless and migrate the entire Scala collections library and an asynchronous programming library to evaluate its practicality and ergonomics. Our results demonstrate that reach capabilities enable the adoption of capture checking in production code with minimal changes and minimal-to-zero notational overhead in a vast majority of cases.
@article{paperbot2940,
title = {What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures},
author = {Yichen Xu and Oliver Bračevac and Cao Nguyen Pham and Martin Odersky},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763112}
}