This program is tentative and subject to change.
Capture checking in Scala 3 enables lightweight and practical effect and resource checking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. This limitation makes it impossible to express natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument.” Both constraints prevent the Scala 3 standard library from being fully capture-checked. For instance, the Try construct re-throws caught exceptions, so it captures only the control-flow capabilities of its body, and Future cannot capture thread-local resources.
We introduce capability classifiers: a tree-structured, user-extensible system for tagging capabilities by semantic role. Classifiers are organized in an open hierarchy, and projections filter kinds of capabilities based on classifiers, 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 foundational 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 via a big-step proof. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns.
This program is tentative and subject to change.
Mon 5 OctDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00 | |||
13:30 18mTalk | Implementing Set-Theoretic Types OOPSLA | ||
13:48 18mTalk | Modular Type Safety for Traits with Extensible Variants and Deep Pattern Matching OOPSLA Andong Fan University of Toronto, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology), Ningning Xie University of Toronto | ||
14:06 18mTalk | Type-Safe Monotonic Object Evolution OOPSLA Alexandra Mirrlees-Black Australian National University, Haoyu Wu Australian National University, Gregor Richards University of Waterloo, Fabian Muehlboeck Australian National University DOI Pre-print | ||
14:24 18mTalk | Classifying Capabilities OOPSLA Nguyen Pham EPFL, LAMP, Oliver Bračevac EPFL, LAMP, Yichen Xu EPFL, Yaoyu Zhao EPFL, LAMP, Martin Odersky EPFL | ||