Rows and Capabilities as Modal Effects
summary
Effect systems for handlers get a concrete bridge: a multimodal target MX encodes Koka-style row effects by translating each annotated arrow to an absolute modality and encodes Effekt-style capabilities by translating blocks to relative modalities plus type quantifiers so capabilities can appear in types. The paper gives macro translations from System Fε and System C that are type-and-semantic-preserving, models local labels to simulate named handlers, and ships a toy PLan prototype with basic modality inference.
AI-written summary · about
chapters (12)
- 0:00Introduction to effect systems and capabilities
- 1:09Row-based effect systems explained
- 4:45Capability-based effect systems overview
- 10:50Modal effects as a unifying framework
- 17:08Effect contexts and modalities in MX
- 25:01Encoding row-based systems in MX
- 28:23Encoding capability-based systems in MX
- 32:05Comparing row and capability systems via MX
- 34:17Handling effects and Q&A introduction
- 43:47Encoding effect handlers in MX
- 49:31Insights for language designers
- 51:39Conclusion and future work
related talks
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
29mLogical Relations for Effect Capabilities
14mModal Effect Types
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
12mA Unified View of Modalities in Type Systems
12mCompiling Effect Handlers in Capability-Passing Style
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
19mFrom Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect ...