haskell - "a monad is a model of computation"是什么意思

Question

当人们说“单子(monad)是计算模型”时，它到底是什么意思？这是否意味着图灵完整性意义上的计算？如果是这样，怎么做？

澄清 :这个问题不是关于解释单子(monad)，而是在这种情况下人们对“计算模型”的含义以及这与单子(monad)有何关系。见接近 this answer 的末尾这个短语的典型用法。

在我对图灵机的理解中，递归函数理论、lambda 演算等都是计算模型，如果有的话，我看不出 monad 与它有什么关系。

Answer 1

单子(monad)作为计算模型的想法可以追溯到 Eugenio Moggi 的工作。在 Haskell 实践者中，Moggi 关于这个问题最著名的论文是 Notions of computations as monads (1991)。相关报价包括:

The [lambda]-calculus is considered a useful mathematical tool in the study of programming languages, since programs can be identified with [lambda]-terms. However, if one goes further and uses [beta][eta]-conversion to prove equivalence of programs, then a gross simplification is introduced (programs are identified with total functions from values to values) that may jeopardise the applicability of theoretical results, In this paper we introduce calculi based on a categorical semantics for computations, that provide a correct basis for proving equivalence of programs for a wide range of notions of computation. [p. 1]

[...]

We do not take as a starting point for proving equivalence of programs the theory of [beta][eta]-conversion, which identifies the denotation of a program (procedure) of type A -> B with a total function from A to B, since this identification wipes out completely behaviours such as non-termination, non-determinism, and side-effects, that can be exhibited by real programs. Instead, we proceed as follows:

• 1. We take category theory as a general theory of functions and develop on top a categorical semantics of computations based on monads. [...] [p. 1]

[...]

The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category [C], we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations. [pp. 2-3]

[...]

We have identified monads as important to modeling notions of computations, but computational monads seem to have additional properties; e.g., they have a tensorial strength and may satisfy the mono requirement. It is likely that there are other properties of computational monads still to be identified, and there is no reason to believe that such properties have to be found in the literature on monads. [p. 27 -- thanks danidiaz]

Moggi 的一篇相关旧论文， Computational lambda-calculus and monads (1989 年——感谢 michid 的引用)，字面意思是“计算模型[s]”:

A computational model is a monad (T;[eta];[mu]) satisfying the mono requirement: [eta-A] is a mono for every A [belonging to] C.

There is an alternative description of a monad (see[7]), which is easier to justify computationally. [...] [p. 2]

这个特殊的术语在作为单子(monad)的计算概念中被删除了，因为 Moggi 将他的演讲重点放在“替代描述”(即 Kleisli 三元组，用 Haskell 的说法，由类型构造函数、返回和绑定(bind))。但是，本质始终保持不变。

Philip Wadler 在 Monads for functional programming 中以更实用的方式提出了这个想法。 (1992):

The use of monads to structure functional programs is described. Monads provide a convenient framework for simulating effectsfound in other languages, such as global state, exception handling, out-put, or non-determinism. [p. 1]

[...]

Pure functional languages have this advantage: all flow of data is made explicit.And this disadvantage: sometimes it is painfully explicit.

A program in a pure functional language is written as a set of equations. Explicit data flow ensures that the value of an expression depends only on its free variables. Hence substitution of equals for equals is always valid, making such programs especially easy to reason about. Explicit data flow also ensures that the order of computation is irrelevant, making such programs susceptible to lazy evaluation.

It is with regard to modularity that explicit data flow becomes both a blessing and a curse. On the one hand, it is the ultimate in modularity. All data in and all data out are rendered manifest and accessible, providing a maximum of flexibility. On the other hand, it is the nadir of modularity. The essence of an algorithm can become buried under the plumbing required to carry data from its point of creation to its point of use. [p. 2]

[...]

Say it is desired to add error checking, so that the second example above returns a sensible error message. In an impure language, this is easily achieved with the use of exceptions.

In a pure language, exception handling may be mimicked by introducing a type to represent computations that may raise an exception. [pp. 3 -4 -- note this is before monads are introduced as an unifying abstraction.]

[...]

Each of the variations on the interpreter has a similar structure, which may be abstracted to yield the notion of a monad.

In each variation, we introduced a type of computations. Respectively, M represented computations that could raise exceptions, act on state, and generate output. By now the reader will have guessed that M stands for monad. [p. 6]

这是使用“计算”​​来指代一元值的根源之一。

后来的大量文献以这种方式利用了计算的概念。例如，这是 Notions of Computation as Monoids 的开头段落。作者:Exequiel Rivas 和 Mauro Jaskelioff(2014 年——感谢 danidiaz 的建议):

When constructing a semantic model of a system or when structuring computer code,there are several notions of computation that one might consider. Monads (Moggi, 1989; Moggi, 1991) are the most popular notion, but other notions,such as arrows (Hughes, 2000) and, more recently, applicative functors (McBride & Paterson, 2008) have been gaining widespread acceptance. Each of these notions of computation has particular characteristics that makes them more suitable for some tasks than for others. Nevertheless, there is much to be gained from unifying all three different notions under a single conceptual framework. [p. 1]

另一个很好的例子是 Comonadic notions of computation Tarmo Uustalu 和 Varmo Vene(2000 年):

Since the seminal work by Moggi in the late 80s, monads, more precisely, strong monads, have become a generally accepted tool for structuring effectful notions of computation, such as computation with exceptions, output, computation using an environment, state-transforming, nondeterministic and probabilistic computation etc. The idea is to use a Kleisli category as the category of impure, effectful functions, with the Kleisli inclusion giving an embedding of the pure functions from the base category. [...] [p. 263]

[...]

The starting-point in the monadic approach to (call-by-value) effectful computation is the idea that impure, effectful functions from A to B must be nothing else than pure functions from A to TB. Here pure functions live in a base category C and T is an endofunctor on C that describes the notion of effect of interest; it is useful to think of TA as the type of effectful computations of values of a given type A.

For this to work, impure functions must have identities and compose. Therefore T cannot merely be a functor, but must be a monad. [p. 265]

“计算”的这种用法符合 models of computation 的常用计算机科学概念。 (参见 danidiaz's answer 了解更多信息)。在非正式的函数式编程文献中，将单子(monad)作为计算模型的暗示具有不同程度的精确度。尽管如此，它们通常都来自一个严谨的想法，或者至少是其分支。