Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What does "a monad is a model of computation" mean

What does it mean exactly when people say "a monad is a model of computation"? Does this mean computation in the sense of turing completeness? If so, how?

Clarification: This question is not about explaining monads but what people mean with "model of computation" in this context and how this relates to monads. See towards the end of this answer for a typical use of this phrase.

In my understanding a turing machine, the theory of recursive functions, lambda calculus etc. are all models of computation and I cannot see how a monad would relate to that if at all.

like image 783
michid Avatar asked May 07 '19 15:05

michid


People also ask

What is a monad in simple terms?

A monad is an algebraic structure in category theory, and in Haskell it is used to describe computations as sequences of steps, and to handle side effects such as state and IO. Monads are abstract, and they have many useful concrete instances. Monads provide a way to structure a program.

What is a monadic computation?

Idea. In computer science, a monad describes a “notion of computation”. Formally, it is a map that. sends every type X of some given programming language to a new type T(X) (called the “type of T-computations with values in X”);

What is a monad example?

Monads are simply a way to wrapping things and provide methods to do operations on the wrapped stuff without unwrapping it. For example, you can create a type to wrap another one, in Haskell: data Wrapped a = Wrap a. To wrap stuff we define return :: a -> Wrapped a return x = Wrap x.

What is a monad in math?

A monad is a certain type of endofunctor. For example, if and are a pair of adjoint functors, with left adjoint to , then the composition is a monad. If and are inverse functors, the corresponding monad is the identity functor. In general, adjunctions are not equivalences—they relate categories of different natures.


2 Answers

The idea of monads as models of computation can be traced back to the work of Eugenio Moggi. Among Haskell practitioners, the best known paper by Moggi on this matter is Notions of computations as monads (1991). Relevant quotes include:

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.

like image 105
duplode Avatar answered Sep 30 '22 20:09

duplode


Nothing. It doesn't mean anything. It's the output of someone struggling to find metaphors which make monads into something they already know. It almost means something. "It is possible to construct models of computation which form monads," for instance, is a meaningful statement. But the difference is significant. "Monads are models of computation" is an attempt to force a broad abstraction into a narrow interpretation. The other specifies that you can work with a broader abstraction for one use case.

Be very wary of reductive explanations. Do you think that an entire community of developers would keep using unfamiliar terminology if familiar terminology communicated the same thing? The term Monad has stuck around for 20 years in a language community that rapidly invents and discards abstractions as it searches for improvements. The only way that can happen is if it communicates something useful and precise.

It's just hard to write an explanation of the application of the idea to programming that makes any sense to people who don't know enough of the language to understand the constructs in use. If you aren't comfortable with at least higher-kinded types, type classes, and higher-order functions there's no way to understand what the notation is saying.

Learning prerequisite ideas will help. Practice writing code will help. Looking at how (>>=) works for various concrete types will help. Struggling through learning how to use a library like Parsec (or modern descendants like megaparsec) will help.

Trying to force the idea to match something you already know via metaphor will not.

like image 43
Carl Avatar answered Sep 30 '22 21:09

Carl