“ monad是计算模型”是什么意思

Question

人们说“ monad是计算模型”的确切含义是什么？从完整性的意义上讲，这意味着计算吗？如果是这样，怎么办？

澄清：这个问题不是要解释单子，而是人们在此上下文中对“计算模型”的含义以及它与单子的关系。有关此短语的典型用法，请参阅此答案的结尾。

在我对图灵机的理解中，递归函数理论，lambda微积分等都是计算模型，我完全看不出monad与它之间的关系。

Answer 1

单子作为计算模型的思想可以追溯到Eugenio Moggi的工作。在Haskell的从业者中，Moggi对此问题最著名的论文是“ 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]

A related older paper by Moggi, Computational lambda-calculus and monads (1989 -- thanks michid for the reference), speaks literally of "computational model[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]

This particular bit of terminology was dropped in the Notions of computations as monads, as Moggi sharpened the focus of his presentation on the "alternative description" (namely, Kleisli triples, which are composed by, in Haskell parlance, a type constructor, return and bind). The essence, though, remain the same throughout.

Philip Wadler presents the idea with a more practical bent in 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]

This is one of the roots of the usage of "computation" to refer to monadic values.

A significant body of later literature makes use of the concept of computation in this manner. For instance, this is the opening passage of Notions of Computation as Monoids by Exequiel Rivas and Mauro Jaskelioff (2014 -- thanks danidiaz for the suggestion):

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]

Another good example is Comonadic notions of computation by Tarmo Uustalu and 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]

Such uses of "computation" fit the usual computer science notion of models of computation (see danidiaz's answer for more on that). In the informal functional programming literature, allusions to monads as models of computation have varying degrees of precision. Still, they generally draw from, or at least are offshoots of, a rigorous idea.

Answer 2

没有。没什么意思 这是某人努力寻找隐喻的结果，这些隐喻使单子变成了他们已经知道的东西。这几乎意味着什么。例如，“可以构建形成单子的计算模型”是有意义的陈述。但是差异很大。“ Monad是计算模型”是试图将广泛的抽象转化为狭义的解释。另一个指定您可以为一个用例使用更广泛的抽象。

警惕还原性的解释。您是否认为，如果熟悉的术语传达相同的信息，那么整个开发人员社区都会继续使用陌生的术语吗？这个术语Monad在一个语言社区中已经存在了20年之久，该语言社区在寻求改进时迅速发明并放弃了抽象。唯一可能发生的方式是它传达有用且精确的信息。

很难写出对该思想在编程中的应用的解释，这对于那些对语言了解不足以理解所使用的构造的人没有任何意义。如果您不满意至少具有较高种类的类型，类型类和高阶函数，则无法理解该符号的含义。

学习先决条件将有所帮助。练习编写代码会有所帮助。在研究如何(>>=)对各种具体类型的作品会有所帮助。努力学习如何使用像Parsec这样的库（或像megaparsec这样的现代后代）会有所帮助。

试图迫使这个想法与通过隐喻已经知道的东西相匹配就不会了。