Handling Bidirectional Control Flow
summary
Claims that algebraic effects can themselves raise effects and still be statically safe, implemented as a core calculus and type system that forbids unhandled and accidentally handled effects and proves type safety plus parametricity. Implements effectful effects (Yield with Replace, async generators and async/await with exception effects, recursive Ping-Pong protocols) using lexically scoped, stack‑bound handlers, mechanizes proofs in Coq, and shows the approach composes with an object‑style interface unification and handles the examples without runtime errors.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:17Languages race to add control-flow features...
- 3:20Algebraic effect signatures
- 3:38Generators, via algebraic effects
- 4:46Programming Challenge: Allow client to interrupt iterator to modify list
- 7:43Unifying effects and objects
- 8:25Other possibilities with effectful effects
- 10:53Message-passing concurrency à la session types
- 12:05Dynamically scoped handlers = Accidental handling
- 13:34Formalization and Soundness
related talks
22mType-Safe Code Generation With Algebraic Effects and Handlers
16mContextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract)
12mTowards Dependently-Typed Control Effects (Extended Abstract)
16mSoundly Handling Linearity
21mEffectful Software Contracts
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
36mParallel Algebraic Effect Handlers
15mEffect Handlers, Evidently