一句话：系统研究 delay monad 与代数效应的组合，刻画哪些效应可分配，并用弱双模拟挽救部分不可行情形。
在类型论中，delay monad 可用于引入一般递归，而要在类型论中直接使用多种计算效应，则需将 delay monad 与相应效应 monad 组合。本文首次系统研究此类组合：同时考察共归纳 delay monad 及其 guarded recursive 版本，给出它们与若干知名计算效应组合的具体例子。进一步地，文章给出一般性定理，刻画哪些代数效应可以分配到 delay monad 上、哪些不能。对于不可分配的情形，作者通过考虑弱双相似意义下的分配律，挽救了部分原本不可能的组合。该工作为在类型论中统一处理递归与代数效应提供了基础性认识。
The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations. We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MogelbergZ25,
title = {What Monads Can and Cannot Do with a Few Extra Pages},
author = {Rasmus Ejlers Møgelberg and Maaike Zwart},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:5)2025}
}