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.

翻译：延迟单子为在类型论中引入通用递归提供了一种途径。为了在类型论中直接编写利用广泛计算效应的程序，我们需要将延迟单子与这些效应的单子相结合。本文首次对此类组合进行了系统性研究。我们同时探讨了共归纳延迟单子及其受保护递归变体，并提供了将这些单子与常见计算效应相结合的具体示例。我们还建立了若干一般性定理，明确指出哪些代数效应可分布于延迟单子之上，哪些则不能。最后，通过考虑弱互模拟意义下的分配律，我们挽救了部分不可能实现的情形。