Typestate via Revocable Capabilities
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914085829869568 |
|---|---|
| author | Jia, Songlin Liu, Craig He, Siyuan Deng, Haotian Bao, Yuyan Rompf, Tiark |
| author_facet | Jia, Songlin Liu, Craig He, Siyuan Deng, Haotian Bao, Yuyan Rompf, Tiark |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_08889 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Typestate via Revocable Capabilities Jia, Songlin Liu, Craig He, Siyuan Deng, Haotian Bao, Yuyan Rompf, Tiark Programming Languages 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. |
| title | Typestate via Revocable Capabilities |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2510.08889 |