Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Typestate via Revocable Capabilities

Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf

TL;DR

This paper tackles the challenge of safely managing stateful resources in the presence of aliasing by unifying scope-based and flow-sensitive approaches. It introduces revocable capabilities and path-dependent types to decouple capability lifetimes from lexical scopes, enabling functions to receive, revoke, and return capabilities in a flow-sensitive manner. The authors provide a Scala 3 prototype that combines a destructive effect system, per-object path-dependent capabilities, and a Sigma-based bundling mechanism with a type-directed ANF transformation to support a wide range of stateful patterns, including file I/O, locking protocols, DOM construction, and session types. Key contributions include the three interactions (receiving, revoking, returning) mediated by implicit resolution, the Sigma abstraction for resource-capability pairing, and practical case studies demonstrating safe and ergonomic typestate programming. The work demonstrates that expressive and safe typestate management can be achieved with minimal extensions to existing capability-based languages, offering a scalable path toward more robust stateful programming in real-world languages like Scala 3.

Abstract

Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. While scope-based constructs such as Java's synchronized blocks offer ease of reasoning, they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive management enables fine-grained control but demands sophisticated typestate analyses and often burdens programmers with explicit state tracking. In this work, we present a novel approach that unifies the strengths of both paradigms by extending flow-insensitive capability mechanisms into flow-sensitive typestate tracking. Our system decouples capability lifetimes from lexical scopes, allowing functions to provide, revoke, and return capabilities in a flow-sensitive manner, based on the existing mechanisms explored 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 stateful patterns, including file operations, advanced locking protocols, DOM construction, and session types. This work demonstrates that expressive and safe typestate management can be achieved with minimal extensions to existing capability-based languages, paving the way for more robust and ergonomic stateful programming.

Typestate via Revocable Capabilities

TL;DR

This paper tackles the challenge of safely managing stateful resources in the presence of aliasing by unifying scope-based and flow-sensitive approaches. It introduces revocable capabilities and path-dependent types to decouple capability lifetimes from lexical scopes, enabling functions to receive, revoke, and return capabilities in a flow-sensitive manner. The authors provide a Scala 3 prototype that combines a destructive effect system, per-object path-dependent capabilities, and a Sigma-based bundling mechanism with a type-directed ANF transformation to support a wide range of stateful patterns, including file I/O, locking protocols, DOM construction, and session types. Key contributions include the three interactions (receiving, revoking, returning) mediated by implicit resolution, the Sigma abstraction for resource-capability pairing, and practical case studies demonstrating safe and ergonomic typestate programming. The work demonstrates that expressive and safe typestate management can be achieved with minimal extensions to existing capability-based languages, offering a scalable path toward more robust stateful programming in real-world languages like Scala 3.

Abstract

Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. While scope-based constructs such as Java's synchronized blocks offer ease of reasoning, they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive management enables fine-grained control but demands sophisticated typestate analyses and often burdens programmers with explicit state tracking. In this work, we present a novel approach that unifies the strengths of both paradigms by extending flow-insensitive capability mechanisms into flow-sensitive typestate tracking. Our system decouples capability lifetimes from lexical scopes, allowing functions to provide, revoke, and return capabilities in a flow-sensitive manner, based on the existing mechanisms explored 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 stateful patterns, including file operations, advanced locking protocols, DOM construction, and session types. This work demonstrates that expressive and safe typestate management can be achieved with minimal extensions to existing capability-based languages, paving the way for more robust and ergonomic stateful programming.

Paper Structure

This paper contains 50 sections, 1 equation, 9 figures.

Table of Contents

  1. Introduction
  2. This Work.
  3. From Capabilities to Typestate, Step by Step
  4. Preliminary: Programming with Scoped Capabilities
  5. Prevent Leakage by Explicit Typing.
  6. Qualifiers: Sets of Variables.
  7. Tracking in Higher-Order Functions.
  8. Polymorphism and Leakage Prevention.
  9. A Naive Step towards Typestate
  10. I: Lack of invalidation for outdated capabilities.
  11. II: Inability to verify resource identity.
  12. III: Poor ergonomics.
  13. Pillar I: Flow-Sensitive Revocation of Capabilities
  14. Foundation: Reachability Types and Transitive Disjointness.
  15. Notations.
  16. ...and 35 more sections

Figures (9)

  • Figure 1: Written using scope-based blocks. Lock lifetimes are managed automatically, whereas table has to be locked longer then row.
  • Figure 2: Written in imperative style, table can be unlocked once row is acquired, enabling improved parallelism, at the cost of being explicit about lock lifetimes.
  • Figure 4: Table Locking Definitions
  • Figure 5: Table Locking API
  • Figure 6: DOM Tree Definitions
  • ...and 4 more figures