Effect Handlers, Evidently
summary
Presents an evidence-passing translation that elaborates polymorphic algebraic effects into polymorphic lambda calculus, with a proof of soundness and coherence under a scoped resumptions restriction (dynamic check in the formalism). Handlers carry fresh marker identifiers in an evidence vector so lookup becomes constant-time; tail-resumptive operations execute in-place without capturing continuations. Also gives a multi-prompt delimited-control translation, a Koka implementation, a Haskell library, and initial benchmarks reported as promising.
AI-written summary · about
chapters (9)
- 0:00Effect Handlers Evidently
- 0:42Algebraic effects overview
- 3:59Implementing algebraic effects
- 5:26Evidence passing translation
- 8:25Scoped resumptions importance
- 10:39Efficiency with evidence passing
- 12:51Multi-prompt to lambda calculus
- 13:34Calculi and translations summary
- 14:15Implementation benchmarks
related talks
15mZero-Overhead Lexical Effect Handlers
18mLexical Effect Handlers, Directly
28mFirst-class Names for Effect Handlers
19mTowards a Reflection for Effect Handlers
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
22mLexical Effect Handler: Fast by Design, Correct by Proof
21mLift Inference for Lexical Effect Handlers with Second-Class Functions
36mParallel Algebraic Effect Handlers