一句话：提出树状、可扩展的 capability 分类器，按语义角色过滤捕获集并支持可判定的不相交推理，在 Scala 3 中实现并于 Lean 4 机器化验证。
Scala 3 的 capture checking 通过在类型中记录 capability，实现轻量而实用的 effect 与资源追踪，但系统无法对 capability 的“种类”进行推理：诸如“只保留该闭包的控制流能力”“从该参数中排除所有线程局部能力”这类自然约束无法表达。前者出现在标准库 Try 的重新抛出中，后者则是 Future 不得捕获线程局部资源的要求，缺失这些表达能力使库的部分代码被排除在 capture checking 之外。本文提出 capability classifiers：一种树状、用户可扩展的标签层级，按语义角色对 capability 分类；投影 only[C] 与 except[C] 按分类器过滤捕获集。树结构带来可判定的不相交推理——位于不同分支的分类器即使在其他位置存在未知扩展也保证不相交。作者将分类器形式化为 System Capless 的扩展，引入基于分类器子树交、并、差的 kind algebra，扩展操作语义以建模异常拦截，并以大步语义证明类型安全、effect safety 与 handler coverage，全部证明在 Lean 4 中机器化。分类器已实现于 Scala 3 capture checker，并演示于标准库类型与真实 effect 排除模式。
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.
@article{paperbot12090,
title = {Classifying Capabilities},
author = {Cao Nguyen Pham and Oliver Bračevac and Yichen Xu and Yaoyu Zhao and Martin Odersky},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839474}
}