Relative Monads in CBPV for Stack-based Effects
summary
Claim: modeling stack-based implementations of effects uses relative monad structure inside Call-by-push-value (CBPV), not ordinary endo-monads. Uses CBPV’s split of value vs computation types, Church encodings, and free relative monads to derive two concrete implementations: a double-barreled continuation and a stack-walking exceptions encoding, and a state cell implemented as a chosen stack slot. Extension is linear (stack-linear), and composition of continuations is presented as explicit stacks rather than first-class monadic values.
AI-written summary · about
chapters (7)
- 0:00Monads and their limits
- 3:02Compiling real-world effects
- 6:28Call-by-push-value
- 9:39Values versus computations
- 14:43Stack-based interpretation
- 17:20Relative monads
- 20:55Applications and conclusion
related talks
17mNotions of Stack-manipulating Computation and Relative Monads
13mComputation Focusing
54mRevisiting the Evolution of Effects (Invited Talk)
27mThe Relative Monadic Metalanguage
15mHandling Bidirectional Control Flow
30mContinuations and Coexponentials
14mAdequacy for Algebraic Effects Revisited
35mStrongly-Typed Multi-View Stack-Based Computations