Modal Effect Types
summary
Replaces pervasive effect variables with an ambient effect context and explicit modalities so higher‑order library signatures no longer need ubiquitous effect quantifiers; uses absolute modality to override context (marking pure definitions) and relative modality to add and handle specific operations like ask, plus masking to remove effects. Claims a multimodal type theory, a prototype implementation, and artifacts with reproducible results (DOI and Zenodo archive). Examples show much shorter types and handler encodings that compose without changing millions of library signatures.
AI-written summary · about
chapters (7)
- 0:00Modal effect types intro
- 3:56Effect variables problem
- 5:22Ambient effect context
- 7:28Relative modality for handlers
- 8:56Advantages of modal types
- 11:48Takeaways and future work
- 12:15Q&A
related talks
12mA Unified View of Modalities in Type Systems
55mRows and Capabilities as Modal Effects
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
20mModal Mu-Calculus for Free in Agda
18mA modal deconstruction of Löb induction
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
15mLatent Effects for Reusable Language Components