Dynamic Wind for Effect Handlers
summary
Adds three handler clauses (on suspend, on resume, on return) to lexical effect handlers and formalizes semantics and a type system that make multi‑shot continuation suspending/resuming well‑defined. Proves progress/preservation and a resource safety theorem that external state (files, globals) is closed on suspend and reinitialized on resume, shows examples where naive handlers double‑append but the new API backtracks globals correctly, and supplies an evaluated, reusable artifact and implementation reproducing the results.
AI-written summary · about
chapters (9)
- 0:00Dynamic wind introduction
- 1:05Lexical handlers context
- 3:33Problem backtracking motivation
- 4:58Solution with suspend/resume
- 6:22Stack unwinding semantics
- 9:13Symmetric resumption process
- 10:18Theoretical results
- 11:23Contributions summary
- 12:46Q&A
related talks
33mRethinking Effects with Effect Systems
46mFunctional effects in perspective
32mEffective Programming in OCaml
27mA General Fine-Grained Reduction Theory for Effect Handlers
32mExperience Report: Graph Rewriting with Lexical Effect Handlers
01h 16mDelimited Continuations, Demystified
29mPaella: algebraic effects with parameters and their handlers
25mHandling Higher-Order Effectful Operations with Judgemental Monadic Laws