“单子变压器比效果更强大” - 例子？

Posted 2023-05-08

【中文标题】“单子变压器比效果更强大” - 例子？

【英文标题】："Monad transformers more powerful than effects" - Examples?

【发布时间】：2015-09-28 21:50:13

【问题描述】：

关于 Idris 影响的论文 "Programming and reasoning with algebraic effects and dependent types" by Edwin C. Brady 包含（未引用的）声明：

尽管 [效果和 monad 转换器] 在功率上不相等 - monad 和 monad 转换器可以表达更多概念 - 捕获了许多常见的有效计算。

有哪些例子可以用 monad 转换器建模但不能用效果器建模？

【问题讨论】：

这是一个有用的问题，可以由更多人回答，而不仅仅是论文的作者。更强大的一个例子是允许重复效果。

我想知道这个问题的答案。当我可以在这里找到论文时，我不想联系论文的作者。

这是一个很好的问题，即使它提到了一些论文......

如果我从Andrej Bauer's blog 找到的论文中没记错的话，代数效应只是定界延续单子的程式化用途。所以单子至少和代数效应一样强大。 Eff language 的主页是从头开始使用代数效应而构建的，其中包含指向其中一些论文的链接。我不会将此作为答案发布，因为我自己并不真正了解细节。

@EduardoLeón 定界延续在 Bauer 和 Pretnar 2010 中给出，Programming with Algebraic Effects and Handlers (pdf);论文以问题结尾“最后，延续是非代数计算效应的典型例子，所以 eff 提供了一种灵活而干净的定界控制形式有点令人惊讶，特别是因为延续根本不在我们的设计中议程。那么我们可以从 eff 中学到什么关于有效环境中的控制操作员的信息？”

【参考方案1】：

可以使用 CPS 将延续建模为单子，但它们不是代数效应，因为它们无法使用 Lawvere 理论建模。参见 Martin Hyland 和 John Power，2007，The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (pdf)，ENTCS 172:437-458。

【讨论】：

感谢您的回答。我正在考虑它，并试图将类别理论转化为更程序化的东西来让我明白。 @Eduardo 在上面评论说效果与定界延续是同构的。因此，我怀疑对于无限延续无法建模这一事实存在一些直觉。效果可能必须限定到给定区域并在有效值逃逸之前进行处理，而 monad 更具传染性。

@geoff_h 我说代数效应可以建模为定界延续单子的使用，而不是说它们是等价的 - 很可能是这种情况，但我真的不知道。

@Eduardo 但是 Eff 确实允许表示分隔的延续 - 尽管有时需要递归类型。这表明了同构-效果可以建模为定界延续，定界延续可以建模为效果-但也许 Eff 也可以表示一些非代数效果-尽管我不确定我是否很好地掌握了非代数效应意味着。

@geoff_h 我怀疑代数效应和定界延续之间的关系很像 monad 和 CPS 之间的关系：后者提供了前者控制结构的表现力，但不提供构造数据类型。