Typestate via Revocable Capabilities

Abstract

Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based constructs like Java's synchronized blocks offer ease of reasoning, but they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive approaches enable fine-grained control, but they require sophisticated typestate analyses and often burden programmers with explicit state tracking. In this work, we present a novel approach that unifies the ease of scoped reasoning with the expressiveness of imperative typestate management. Our design extends traditional flow-insensitive capability mechanisms to a flow-sensitive setting. In particular, we decouple capability lifetimes from lexical scopes, allowing functions to receive, revoke, or return capabilities in a flow-sensitive manner, building on existing mechanisms for the safety and ergonomics of scoped capability programming. We implement our approach as an extension to the Scala 3 compiler, leveraging path-dependent types and implicit resolution to enable concise, statically safe, and expressive typestate programming. Our prototype generically supports a wide range of patterns, including file operations, advanced locking protocols, DOM construction, and session types, showing that expressive and safe typestate management can be achieved with minimal extensions to an existing language with capability support.