Notions of Stack-manipulating Computation and Relative Monads (Extended Version)

TL;DR

This work addresses the gap between high-level monadic interfaces and low-level stack-based implementations of computational effects by introducing a polymorphic call-by-push-value (CBPV) framework that models explicit stack manipulation. It defines relative monads as the appropriate abstraction for representing stack-based continuations within CBPV, and develops monadic blocks and an algebra translation to overload CBPV do-notation for arbitrary relative monads. A fundamental theorem links CBPV-relative monads to an algebra-based model, enabling automatic construction of relative monad transformers from relative monads and facilitating modular effect composition. The Zydeco prototype demonstrates feasibility, with implications for compiler intermediate representations and stack-based effect implementations, offering a principled pathway to derive effect transformers and reason about stack-manipulating computations formally.

Abstract

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 combine different 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.