Classifying Capabilities (Extended Version)
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, Martin Odersky
cs.PL
Jul 27, 2026 · v1
TL;DR
Type safety, effect safety, and handler coverage for capability classifiers proven via a mechanized big-step proof in Lean 4.
Abstract
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.
Problem
Capture checking in Scala 3 tracks capabilities in types but cannot reason about kinds of capabilities, making natural constraints like retaining only control-flow capabilities or excluding thread-local resources inexpressible. This has kept parts of the Scala 3 standard library outside capture checking.
Approach
Capability classifiers are introduced as a tree-structured, user-extensible hierarchy of tags classifying capabilities by semantic role. Projections filter capture sets by classifier with inclusion and exclusion operators, and the tree structure enables decidable disjointness reasoning. Classifiers are formalized as an extension of System Capless with a classifier kind algebra over intersection, union, and subtraction of classifier subtrees.
Results
Type safety, effect safety, and handler coverage were established via a big-step proof fully mechanized in Lean 4. The classifiers were implemented in the Scala 3 capture checker and demonstrated on standard library types and real-world effect exclusion patterns.