一句话：用 CBPV 与 relative monad 统一低层栈操作效果，并推广 do 记法为 monadic blocks。
函数式编程用 monad 简洁抽象用户定义的计算效果，支持等式推理、接口抽象与 monad transformer 栈。然而编译器与汇编程序员虽然也虚拟化效果，其实现细节却在于运行时栈布局，与高层 monad 接口脱节。本文用多态 call-by-push-value（CBPV）演算刻画显式栈操作，其类型系统允许定义领域特定栈结构；并证明范畴论中的 relative monad 可建模计算效果的基于栈实现。作者将多种标准 monad 适配为 relative monad，并推广 do-notation 为 monadic blocks，使全部 CBPV 代码能针对任意 relative monad 重新解释。作为应用，论文证明所有 relative monad 自动扩展为 relative monad transformer，而纯语言中该过程并不自动。该工作连接了高层效果抽象与低层栈实现。
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.
@article{paperbot3165,
title = {Notions of Stack-Manipulating Computation and Relative Monads},
author = {Yuchen Jiang and Runze Xue and Max S. New},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720434}
}