Towards a Reflection for Effect Handlers
summary
Attempts to establish a reflection for algebraic effects use a simplest CPS translation (two continuations plus an aspirant construct) and a precisely annotated target calculus; this proves monotonicity for both compiling and decompiling and shows decompiling◦compiling = identity, but fails to prove compiling◦decompiling = reduction of the source because the kernel lacks an h-let rule that moves let-frames into handler returns. The proof isolates two remedies — separate frames from return in the CPS or make handlers enforce deep semantics — and proposes trying a more complex CPS from a recent JFP paper.
AI-written summary · about
chapters (10)
- 0:00Reflections for effect handlers
- 1:45Existing reflections approach
- 2:28Search calculus
- 3:34Compiling with CPS
- 8:09Decompiling to direct style
- 11:05Compiling versus decompiling
- 12:54Proof failure and fix
- 15:56Lessons learned next steps
- 16:38Comparison with shift zero dollar
- 18:02Conclusion future work
related talks
29mA Typed and Unified Reflection for Shift and Shift0
15mEffect Handlers, Evidently
12mCompiling Effect Handlers in Capability-Passing Style
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
29mHigher-Order Weakest Precondition Transformers via a CPS Transformation
12mTowards Dependently-Typed Control Effects (Extended Abstract)
13mOne-Pass CPS Translation of Dependent Types (Talk Proposal)
18mLexical Effect Handlers, Directly