Notions of Stack-manipulating Computation and Relative Monads
summary
Adapts the category-theoretic notion of relative monads to a polymorphic call-by-push-value calculus to model concrete stack-based implementations of effects (exceptions, state, continuations). Presents a generalized do-notation called monadic blocks and an algebra translation that reinterprets CBPV code into arbitrary relative monads. Shows that relative monad transformers arise automatically, with a prototype language Zidico and a stack-machine interpreter; artifacts are available, evaluated reusable, and results reproduced.
AI-written summary · about
chapters (9)
- 0:00Effects and monads intro
- 1:48Compiling effects low-level
- 3:30Relative monads intro
- 5:17Call-by-push-value stack types
- 8:08Monadic blocks in CBPV
- 10:15Relative monad transformers
- 12:42Implementation and future work
- 13:45Summary and contributions
- 14:08Q&A
related talks
25mRelative Monads in CBPV for Stack-based Effects
27mThe Relative Monadic Metalanguage
35mStrongly-Typed Multi-View Stack-Based Computations
42mMonads you already use without knowing it
31mThe Eff monad, one monad to rule them all
54mRevisiting the Evolution of Effects (Invited Talk)
34mGraded Monads and Type-Level Programming for Dependence Analysis
13mComputation Focusing