Type-Safe Code Generation With Algebraic Effects and Handlers
summary
A two-stage calculus with algebraic effects and deep handlers enforces that well-typed generators never produce scope-extruding code and supports multi-level let-insertion; the design uses refined environment classifiers and classifier-polymorphic handlers, formalizing the ideas handlers as future-stage binders and handlers are universal. The paper proves type soundness (progress and preservation), demonstrates examples where swapped handler order causes free variables to appear, and reports a conservative but practical typing that distinguishes safe from unsafe generators.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 0:21Staging with meta and type safety
- 1:05Algebraic effects and handlers background
- 2:13Red insertion with effect handlers
- 4:33Scope extrusion problem
- 5:22Environment classifiers for free variables
- 7:08Handling effect handlers in staging
- 8:47Order-sensitive scope extrusion examples
- 9:37Handlers as future stage binders solution
- 11:02Typing rules with classifier annotations
- 12:34Classifier polymorphism in handlers
- 13:38Type soundness proof and guarantees
- 14:27Related work vs Oishi-Kameyama
- 15:59Effect handlers vs shift/reset
- 16:20Summary of contributions
- 16:43Q&A: Porting to OCaml
- 18:16Q&A: Fixing type errors
- 19:19Q&A: Compiler guidance vs user correction
- 20:01Q&A: Environment classifiers in MetaML
- 21:09Q&A
related talks
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
15mHandling Bidirectional Control Flow
29mA type safe calculus for generating syntax-directed editors
28mFirst-class Names for Effect Handlers
36mParallel Algebraic Effect Handlers
15mEffect Handlers, Evidently
20mGenerating Well-Typed Terms that are not "Useless"
46mThe Calculated Typer (Functional Pearl)