盒子里有什么：基于人体工程学的捕捉技术，以及超越通用数据结构的表现力追踪功能

《Proceedings of the ACM on Programming Languages》：What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures

System Capless提出新型捕获机制，通过existential capture sets量化解决通用数据结构的能力追踪问题，在Scala 3中验证其有效性和易用性。

　　

摘要

在Scala中，捕获类型的功能将静态效果和资源跟踪与对象特性统一起来，实现了轻量级的效果多态性，同时减少了符号表示的复杂性。然而，这种表达能力对于追踪嵌套在泛型数据结构中的特性来说仍然不足，从而阻碍了它们被纳入标准集合库——而这正是广泛采用这些特性的关键前提。这一限制源于系统无法在“箱型类型”的概念中对这些特性进行命名。

本文提出了System Capless这一新的类型捕获框架，为“reach capabilities”（rcaps）提供了理论基础。rcaps是一种用于命名“箱内内容”的新机制。该框架将“通用能力”的概念细化为一种新的体系，引入了存在量化和全称量化的概念。直观而言，rcaps能够在泛型类型的“箱内”以不暴露存在量化捕获类型的方式对其进行验证。我们使用Lean语言完全实现了System Capless的形式化元理论，包括类型正确性和作用域安全性的证明。System Capless支持与捕获类型相同的轻量级符号表示方式，并且还支持完全可选的显式捕获集量化，从而增强了表达能力。

最后，我们基于System Capless重新实现了Scala 3中的捕获类型检查机制，并将整个Scala集合库及异步编程库进行了迁移，以评估其实用性和易用性。测试结果表明，在绝大多数情况下，通过引入reach capabilities，可以在生产代码中以极少的修改和几乎零的符号表示开销实现捕获类型检查。