Reference. Notions of Stack-manipulating Computation and Relative Monads
Monads provide a simple and concise interface to user-defined computational effects in functional programming languages. This enables equational reasoning about effects, abstraction over monadic interfaces and the development of monad transformer stacks to allow for multiple effects. Compiler implementors and assembly code programmers similarly virtualize effects, and would benefit from similar abstractions if possible. However, the implementation details of effects seem disconnected from the high-level monad interface: at this lower level much of the design is in the layout of the runtime stack, which is not accessible in a high-level programming language.
We demonstrate that the monadic interface can be faithfully adapted from high-level functional programming to a lower level setting with explicit stack manipulation. We use a polymorphic call-by-push-value (CBPV) calculus as a setting that captures the essence of stack-manipulation, with a type system that allows programs to define domain-specific stack structures. Within this setting, we show that the existing category-theoretic notion of a relative monad can be used to model the stack-based implementation of computational effects. To demonstrate generality, we adapt a variety of standard monads to relative monads. Additionally, we show that stack-manipulating programs can benefit from a generalization of do-notation we call “monadic blocks” that allow all CBPV code to be reinterpreted to work with an arbitrary relative monad. As an application, we show that all relative monads extend automatically to relative monad transformers, a process which is not automatic for monads in pure languages.
Cite
Cited by (1)
Syntax and semantics of focalisation with relative monads and comonads mangel-2026-syntax
Cites 33 works (3 here)
With notes (3)
Do be do be do lindley-2017-do
A theory of effects and resources: adjunction models and polarised calculi curien-2016-a
Models of a Non-associative Composition munchmaccagnoni-2014-models
External (30)
- Zydeco Implementation (2025)
- Notions of Stack-manipulating Computation and Relative Monads (Extended Version) (2025)
- The formal theory of relative monads (2024)
- Call-by-Unboxed-Value (2024)
- The fire triangle: how to mix substitution, dependent elimination, and effects (2019)
- What is a Monoid? (Levy, CT2019 talk) (2019)
- Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing (2018)
- Structural Operational Semantics for Control Flow Graph Machines (2018)
- Contextual isomorphisms (2017)
- An effectful way to eliminate addiction to dependence (2017)
- Sequent calculus as a compiler intermediate language (2016)
- Copatterns (2013)
- Monads Need Not Be Endofunctors (2010)
- Modular Monad Transformers (2009)
- Relational Parametricity for Computational Effects (2007)
- Adjunction Models for Call-by-Push-Value with Stacks (2005)
- Modular correspondence between dependent type theories and categories including pretopoi and topoi (2005)
- Stack-based typed assembly language (2003)
- Call-by-Push-Value (Levy, PhD thesis, Queen Mary) (2001)
- Semantics for Algebraic Operations (2001)
- Comparing Control Constructs by Double-barrelled CPS Transforms (2001)
- Deriving backtracking monad transformers (2000)
- Monad transformers and modular interpreters (1995)
- Imperative functional programming (1993)
- Notions of computation and monads (1991)
- Comprehending monads (1990)
- Types, Abstraction and Parametric Polymorphism (1983)
- Continuation-Based Program Transformation Strategies (1980)
- Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (1972)
- Definitional interpreters for higher-order programming languages (1972)