一句话：提出在类型中紧凑记录值所捕获自由变量的演算 CC<:□，并用于安全实现作用域能力与效应多态。
传统类型系统通常刻画值的形状，却不描述值所捕获的自由变量；然而若能在类型层面知道这些捕获变量，就可保证许多安全性质。本文提出演算 CC<:□，在类型中简洁地表示被捕获变量，并展示如何通过作用域能力（scoped capabilities）安全实现效应与效应多态。文章讨论了追踪捕获变量这一决定如何影响演算的关键设计，并表明 CC<:□ 能为常见数据结构及其典型用法给出简单直观的类型。最后，作者说明这些思想如何指导实际编程语言中 capture checking 的实现。
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC < :◻ , a calculus where such captured variables are succinctly represented in types, and show it can be used to safely implement effects and effect polymorphism via scoped capabilities. We discuss how the decision to track captured variables guides key aspects of the calculus, and show that CC < :◻ admits simple and intuitive types for common data structures and their typical usage patterns. We demonstrate how these ideas can be used to guide the implementation of capture checking in a practical programming language.
@article{paperbot2123,
title = {Capturing Types},
author = {Aleksander Boruch-Gruszecki and Martin Odersky and Edward Lee and Ondřej Lhoták and Jonathan Brachthäuser},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {4},
year = {2023},
doi = {10.1145/3618003}
}