分类能力（扩展版本）
Classifying Capabilities (Extended Version)
浏览论文内容
中文总结 AI 辅助
研究Scala 3捕获检查中能力种类推理问题，引入能力分类器，它是树形结构、用户可扩展的标签层次结构，通过语义角色对能力分类，能过滤捕获集，形式化分类器并扩展操作语义，实现类型安全等，还展示了其在标准库等中的应用。
中文摘要 AI 辅助
Scala 3中的捕获检查通过在类型中记录能力来实现轻量级且实用的效果和资源跟踪。然而，该系统无法对能力种类进行推理。诸如“仅保留此闭包的控制流能力”或“从此参数中排除所有线程局部能力”等自然约束变得无法表达。这在Scala 3标准库中有所体现：“Try”重新抛出捕获的异常，因此它仅保留其主体的控制流能力，而“Future”不能捕获线程局部资源。无法陈述这些约束使得库的部分内容无法进行捕获检查。我们引入了能力分类器：一种树形结构、用户可扩展的标签层次结构，通过语义角色对能力进行分类。投影根据分类器过滤捕获集，支持包含（“此http URL [C]”）和排除（“此http URL [C]”）。树形结构使得可判定的不相交推理成为可能：无论层次结构中其他未知扩展如何，不同分支上的分类器都保证不相交。我们将分类器形式化为捕获检查核心演算System Capless的扩展，引入基于分类器子树的交集、并集和减法的分类器种类代数。我们扩展操作语义以对异常拦截进行建模，并通过大步证明建立类型安全性、效果安全性和处理程序覆盖，在Lean 4中完全机械化。分类器在Scala 3捕获检查器中实现，我们展示了它们在标准库类型和实际效果排除模式中的使用。
英文摘要
Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as "retaining only the control-flow capabilities of this closure" or "excluding all thread-local capabilities from this argument" become inexpressible. Both arise in the Scala 3 standard library: "Try" re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and "Future" must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion ("c.only[C]") and exclusion ("c.except[C]"). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns.
