“一个单子是一种计算模型”是什么意思？

Question

“一个单子是一种计算模型”是什么意思？

haskellmonadscategory-theory

17

人们说“monad是一种计算模型”，这究竟意味着什么？这是否意味着图灵完备的计算？如果是这样，它是如何实现的？

澄清：这个问题不是关于解释monad，而是在这个上下文中“计算模型”这个术语的含义，以及这与monad的关系。请参见这个答案末尾对这个短语的典型用法的解释。

在我的理解中，图灵机、递归函数理论、lambda演算等都是计算模型，我无法看出monad如何与它们相关（如果有）。

- michid

1

你是否在考虑某个特定的文本，它说“单子是计算模型”？在具体示例的情况下，更容易判断它是否只是一个错听，如卡尔所建议的，还是更实质性的东西。 - duplode

1

不要试图找到一个简单解释单子是什么的一行代码，这是一个相当复杂的概念，需要更多的解释。我听说过“单子是可编程分号”、“单子是单子范畴中的幺半群（当然）”、“单子就像卷饼”等等，但这些都对初学者没有帮助（即使它们在技术上是正确的）。尝试阅读单子教程，并关注示例和理论。 - chi

@chi，同意你的看法，但我很确定“单子就像玉米卷饼”这句话是个笑话，它（讽刺地）源自一篇正确指出了你所说的事情的帖子，即没有一个类比能够立即解释“单子是什么”的事实。这篇文章就是我想到的那篇文章。 - Robin Zigmond

3

编程语言中使用单子(monads)的思想来自Eugenio Moggi 1991年的论文《计算的概念和单子》(Notions of computation and monads)，链接为https://core.ac.uk/download/pdf/21173011.pdf。论文的最后一段包括以下句子："我们已经确认单子是用于建立计算概念模型的重要工具"。Rivas和Jaskelioff在后来发表的论文《计算概念作为幺半群》(Notions of Computation as Monoids)中如此开篇："当构建系统的语义模型或编写计算机代码时，有几种可能的计算概念可供考虑。单子是最流行的概念之一"。 - danidiaz

1

感谢@danidiaz，您的评论让我找到了Moggi的另一篇论文：https://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf。在这里，“计算模型”一词的意义类似于λ演算是一种计算模型。 - michid

显示剩余2条评论

3个回答

13

没有意义。这只是某人为了将单子（monads）转化为已知事物而努力寻找比喻的产物。它基本上有意义。例如，“可以构建形成单子的计算模型”是一个有意义的陈述。但差别很大。“单子是计算模型”试图将广泛的抽象强制解释为狭窄的解释，而另一种则指定你可以针对一个使用案例使用更广泛的抽象。

对简化解释要非常谨慎。如果熟悉的术语可以传达相同的含义，那么整个开发人员社区为什么还要继续使用不熟悉的术语？在追求改进的过程中，这个术语Monad在语言社区中已经流行了20年。唯一可能发生的情况是它传达了有用和精确的信息。

只是很难编写一篇解释如何将这个想法应用于编程的文章，让那些不了解语言中使用的结构的人感到有意义。如果你对至少高阶类型、类型类和高阶函数不熟悉，那么你无法理解符号表达的含义。

学习先决条件的想法是有帮助的。练习编写代码也是有帮助的。查看如何使 (>>=) 在不同的具体类型中工作也是有帮助的。艰苦地学习如何使用像Parsec这样的库（或现代后代像megaparsec）也是有帮助的。

试图通过隐喻将想法强制与自己已知的某些东西相匹配是无用的。

- Carl

2

我建议调整这个答案，减少对初学者的建议，因为现在楼主已经明确表示他们不需要一个单子教程，并且扩展一下关于谓词和身份混淆的问题，这似乎是您反对“单子是计算模型”的根源（如果“是”被解释为身份，则可以在还原方式中使用）。 - duplode

4

扩展一下@duplode的回答，我认为在谈论计算时，“模型”可以有至少两个略微不同的含义。

在编程中，"模型"（model）指的是一种执行计算的方式，能够表达任何算法。因此，图灵机、λ演算、邮递员问题等都属于"模型"的范畴。而"Church-Turing论题"(Church–Turing thesis)则是指出了任何可计算函数均可用图灵机计算出来的理论。

另一种模型是指编程语言语义。这个想法是将程序视为可组合的句法结构，并希望它们在某种意义上“意味着”某些东西，最好能够让我们从元素的含义确定组合的含义。从这个意义上说，λ演算有模型。

现在，一种语义学是指称语义学，其中我们分配给程序的含义是某种数学对象。以一个微不足道的例子为例，考虑二进制数字。这里“程序”是0和1的字符串，被视为纯粹的符号。而“模型”将会是自然数，以及将每个符号串映射到相应自然数的函数。

有时，程序的这些指示是用范畴论的术语表达的。这就是Moggi论文的背景：他利用范畴论中的机制（如单子）将编程语言概念（如异常、续延、输入/输出等）映射到数学模型中。单子成为构造程序含义的数学宇宙的方便方法。

- danidiaz

相关链接：https://cstheory.stackexchange.com/questions/944/solid-applications-of-category-theory-in-tcs - danidiaz

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- duplode · Accepted Answer

单子作为计算模型的概念可以追溯到Eugenio Moggi的工作。在Haskell从业者中，Moggi在此问题上最知名的论文是Notions of computations as monads (1991)。相关引用包括：

[lambda]演算被认为是研究编程语言的有用数学工具，因为程序可以与[lambda]项进行识别。但是，如果进一步使用[beta][eta]-转换来证明程序的等价性，则会引入严重的简化（将程序与从值到值的总函数进行识别），这可能危及理论结果的适用性。在本文中，我们介绍了基于范畴语义的演算，为证明各种计算概念下的程序等价性提供了正确的基础。我们不以[beta][eta]-转换理论为证明程序等价性的起点，它将类型为A -> B的程序（过程）的表示与从A到B的总函数进行识别，因为这种识别完全抹去了例如非终止、非确定性和副作用等真实程序可能展现出的行为。相反，我们按照以下方式进行：

- 我们将范畴论视为函数的一般理论，并在其上开发了基于单子的计算的范畴语义。[第1页] - 下面范畴语义的基本思想是，为了在范畴[C]中解释编程语言，我们将类型A的值对象（类型A的值）与类型TA的计算对象（类型A的计算）区分开来，并将程序（类型A）的表示形式识别为TA的元素。特别地，我们将类型A与值对象（类型A的值）的对象进行识别，并通过将一元类型构造子T应用于A来获得计算对象（类型A的计算）。我们称T为<计算概念>，因为它抽象出计算可能产生的值类型。对于TA有许多选择，对应于不同的计算概念。[第2-3页] - 我们已经确定了单子作为建模计算概念的重要性，但是<计算单子>似乎具有其他属性；例如，它们具有张量强度并可以满足单一要求。可能还有其他计算单子属性有待确定，在单子文献中找到这些属性的原因无法确定。[第27页 - 感谢danidiaz]

一篇相关的旧论文由Moggi撰写，题为计算λ演算和单子（1989年 - 感谢michid提供参考），字面上讲述了“计算模型”：

一个计算模型是一个单子(T;[eta];[mu])，满足单要求：对于每个属于C的A，[eta-A]都是单调的。

有一个单子的另一种描述方法（见[7]），更容易从计算角度进行证明。[...] [第2页]

这个特定的术语在《计算作为单子的概念》中被删除，因为Moggi将他的演示焦点放在了“替代描述”上（即Kleisli三元组，由类型构造器、返回和绑定组成，在Haskell中称为）。然而，本质始终保持不变。

菲利普·沃德勒在函数式编程的单子(1992)一书中更注重实际应用方面来阐述这个想法:

介绍了使用单子来构建函数式程序的方法。单子提供了一个方便的框架，用于模拟其他语言中发现的效果，例如全局状态、异常处理、输出或非确定性。[第1页]

纯函数式语言具有这个优点：所有数据流都是明确的。但缺点是有时过于明显。在纯函数式语言中，程序被写成一组方程。显式的数据流确保表达式的值仅取决于其自由变量。因此，等号代替等号总是有效的，使得这样的程序特别易于理解。显式的数据流也确保计算顺序无关紧要，使得这样的程序容易受到惰性评估的影响。

就模块化而言，显式数据流成为祝福和诅咒。一方面，它是最大化模块化的极致。所有数据进出都清晰可见，提供了最大的灵活性。另一方面，它是模块化的最低点。算法的本质可能会淹没在所需的管道下，以将数据从创建点传递到使用点。[第2页]

假设希望添加错误检查，以使上述第二个示例返回合理的错误消息。在不纯的语言中，可以通过使用异常轻松实现这一点。在纯语言中，可以通过引入表示可能引发异常的计算的类型来模拟异常处理。[第3-4页--请注意，这是在单子被引入为统一抽象之前。]

解释器的每个变体具有类似的结构，可以将其抽象化以得出单子的概念。在每个变体中，我们引入了一种计算类型。分别，M表示可能引发异常、作用于状态和生成输出的计算。现在读者可能已经猜到M代表单子。[第6页]

这是“计算”一词用于指代单子值的起源之一。

一大部分后期文献都使用了计算概念。例如，Exequiel Rivas和Mauro Jaskelioff（2014）的Notions of Computation as Monoids开篇如下：在构建系统的语义模型或编写计算机代码时，有几种计算概念可以考虑。单子范畴（Moggi，1989；Moggi，1991）是最流行的概念，但其他概念，如箭头（Hughes，2000）和最近出现的适用函子（McBride＆Paterson，2008）已经获得广泛认可。每种计算概念都有特定的特征，使它们更适合某些任务而不是其他任务。然而，将这三个不同的概念统一到一个概念框架下可以获得很多收益。[第1页]另一个很好的例子是Tarmo Uustalu和Varmo Vene（2000）的Comonadic notions of computation。

自从Moggi在80年代末的开创性工作以来，单子（更准确地说是强单子）已成为一种通用的工具，用于构造有副作用的计算概念，例如异常计算、输出计算、使用环境的计算、状态转换、非确定性和概率计算等。其思想是使用Kleisli范畴作为不纯的、有副作用的函数的范畴，其中Kleisli包含将纯函数从基础范畴嵌入其中。[...] [第263页]

[...]

单子方法论对（按值调用）有副作用的计算的起点是这样一个观点：从A到B的不纯的、有副作用的函数必须仅仅是从A到TB的纯函数。这里，纯函数位于基础范畴C中，T是C上的一个自函子，描述所关心的副作用；TA有助于将给定类型A的带有副作用的计算的类型。

为了使这个方法能够运行，不纯函数必须具有标识和组合。因此，T不能仅仅是一个函子，而必须是一个单子。[第265页]

这里的“计算模型”通常符合计算机科学中计算模型的概念（有关此内容，请参见danidiaz的答案）。在非正式的函数式编程文献中，对单子作为计算模型的暗示具有不同程度的精确性。然而，它们通常源于一个严谨的想法或者至少是其分支。