Effects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
summary
Claims a middle ground: System C reconciling capability-based and traditional effect systems by tracking which lexical capabilities a binding transitively captures, adding explicit boxed values to lift second-class restrictions, and moving capture information between binder annotations and first-class function types. Implements an online playground with the paper’s examples, gives an implementation and a mechanized soundness proof, and targets the FX language (spelled with a K) from Jonathan Schuster’s Tübingen group.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:17Roadmap
- 1:44A puzzle
- 5:36A change of approach
- 6:32Traditional and Capability-based Effect Systems
- 8:52Example: Scope-based Reasoning
- 10:03Effect Safety: Closing over Capabilities
- 11:15A Solution: Second-Class Values
- 14:52Fine-grained Notion of Second-Classiness
- 17:40Syntax of System C (ed. 1)
- 18:31Block Typing
- 19:42Statement Typing
- 21:23First-class Functions by Boxing
- 24:58Summary
related talks
29mLogical Relations for Effect Capabilities
55mRows and Capabilities as Modal Effects
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
19mFrom Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ...
12mCompiling Effect Handlers in Capability-Passing Style
15mHandling Bidirectional Control Flow
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...
19mAssociated Effects: Flexible Abstractions for Effectful Programming