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

Posted

技术标签:

【中文标题】“单子变压器比效果更强大” - 例子?【英文标题】:"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 之间的关系:后者提供了前者控制结构的表现力,但不提供构造数据类型。

以上是关于“单子变压器比效果更强大” - 例子?的主要内容,如果未能解决你的问题,请参考以下文章

变压器骨架

变压器里的Lp代表啥参数?

环形工频变压器线圈参数

环形工频变压器线圈参数

基础知识环形变压器基础知识及问答

易电务大课堂:配电智能运维之变压器运行安全