Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operat...
summary
Formalizes four calculi (effect handlers vs delimited-control, static vs generative labels), gives a concrete type system for each and proves type soundness and effect safety, and implements explicit macro translations both directions that are type- and meaning-preserving. Translations extend prior untyped/macroscopic encodings to a typed setting, handle runtime-generated labels with lexical scoping, and show the two abstractions have equal expressive power—readying the framework for a future extension to first-class labels.
AI-written summary · about
chapters (11)
- 0:00Typed equivalence research
- 1:25Expressive power equivalence
- 2:55Direct vs incremental translation
- 3:39Effect safety with levels
- 5:28Formalizing labeled handlers
- 8:42Static-level control operators
- 10:10Effect safety for translation
- 12:02Type translations between calculi
- 14:56Generative labeled handlers
- 18:07Future work on labels
- 19:16Q&A
related talks
27mA General Fine-Grained Reduction Theory for Effect Handlers
27mWith or Without You: Programming with Effect Exclusion
46mFunctional effects in perspective
25mHandling Higher-Order Effectful Operations with Judgemental Monadic Laws
33mRethinking Effects with Effect Systems
45mA categorical view of computational effects
33mExtensible Effects: A Leaner Cake for Purely Functional Code
46mThe Calculated Typer (Functional Pearl)