First-class Names for Effect Handlers
summary
Claim: treating first-class handler names as values plus scoped effects with rank-2 polymorphism prevents name-escaping without new language primitives. Paper formalizes two sound type systems, proves preservation and progress for top-level programs, implements all variations in Koka, and demonstrates working examples: file handles, dynamically generated heap cells, and a neural-network of layered handlers. Result is practical and provably safe; two design variants trade expressiveness (dynamic handler generation) against simplicity.
AI-written summary · about
chapters (5)
- 0:00Introduction to named handlers
- 2:37Applications and use cases
- 9:45Type systems and soundness
- 17:41Implementation in Coca
- 20:54Conclusion and Q&A
related talks
15mEffect Handlers, Evidently
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
22mType-Safe Code Generation With Algebraic Effects and Handlers
22mLexical Effect Handler: Fast by Design, Correct by Proof
15mZero-Overhead Lexical Effect Handlers
12mCompiling Effect Handlers in Capability-Passing Style
18mLexical Effect Handlers, Directly