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

Cite as @jiang_xue_new_2025 (helia, typst) · \cite{jiang_xue_new_2025} (LaTeX)
BibTeX
bibtex · 12 lines
@article{jiang_xue_new_2025,
 title = {Notions of Stack-manipulating Computation and Relative Monads},
 author = {Jiang, Yuchen and Xue, Runze and New, Max S.},
 year = {2025},
 doi = {10.1145/3720434},
 url = {https://arxiv.org/abs/2502.15031},
 publisher = {ACM},
 journal = {Proceedings of the ACM on Programming Languages},
 volume = {9},
 number = {OOPSLA1},
 pages = {563--589}
}
hayagriva YAML (typst)
yaml · 18 lines
jiang_xue_new_2025:
  type: article
  title: Notions of Stack-manipulating Computation and Relative Monads
  author:
  - Jiang, Yuchen
  - Xue, Runze
  - New, Max S.
  date: 2025
  page-range: 563-589
  url: https://arxiv.org/abs/2502.15031
  serial-number:
    doi: 10.1145/3720434
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: ACM
    issue: OOPSLA1
    volume: 9
Cited by (1)

Syntax and semantics of focalisation with relative monads and comonads mangel-2026-syntax

The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of adjunctions over non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad ! (refining □) and a strong monad ◊. The starting point of our contribution is noticing that the completeness for a polarised syntax for ! and ◊ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads: more precisely, comonads relative to ↓ (the positive shift functor) for ! and monads relative to ↑ (the negative shift functor) for ◊. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared. Yet the syntax we present arose from proof-theoretic consideration, without the link with relative (co)monads being noticed at the time. Our first remark is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the notion of adjunction over non-associative categories, and establish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model ! and ◊.
arXiv
Cites 33 works (3 here)
With notes (3)

Do be do be do lindley-2017-do

PDF · DOI · arXiv · pldb

A theory of effects and resources: adjunction models and polarised calculi curien-2016-a

DOI · pldb

Models of a Non-associative Composition munchmaccagnoni-2014-models

DOI
External (30)
jiang_xue_new_2025 reference entries/refs/jiang_xue_new_2025/jiang_xue_new_2025.hel