Lambda the Ultimate

Wikipedia says that a 'monad' in mathematics can refer to something from both non-standard analysis and something from category theory. I'm only familiar with the latter usage of 'monad' in mathematics, and only to some degree; I've only recently begun to try to study category theory. In category theory, Monads have a relationship to concepts like Functors. I won't try to explain more since I'd probably put my foot in my mouth... However, there are some books on the topic which may be beneficial, including a quite short book from Benjamin Pierce on category theory as relevant to computer science.

As for the ML type (I assume you mean something like 'option'), the only difference between that and Haskell's Maybe monad is that, in addition to defining an ADT, there is also defined a set of functions over the type.

You need to understand type classes in Haskell to understand exactly how this works, but the simplified account is that you have two polymorphic higher-order functions: one called 'return', and one called 'bind', the latter usually denoted as the infix operator (>>=). By using the function 'return' and 'bind' in certain combinations with other functions, you can represent a composite computation which may produce an 'option' or 'Maybe' result at various intermediate stages. If at one of those stages the computation fails, or you have a result of something like 'none,' then you can cascade this failure across the remaining stages of computation without having to explicitly deal with possible failure at every single stage.

For example, say you wanted to add 3 potential numbers, all of which were embedded in the 'option' type. Without a monad, you'd have to check each potential number before adding it to the others, to see whether it was an actual number first; if it wasn't, you'd set the result of the entire addition expression to 'none'. In the Maybe monad, you don't have to do this. You just specify the entire computation up front, without any explitic nested failure checking. It is the responsibility of the higher-order functions 'return' and 'bind' to "handle the details" of the failure implicitly. If failure does occur somewhere early on in a complex computation, the effect of this will cascade in a safe and predictable way.

You can't get things out of the Maybe Monad (without additional operations), but you can get from the Maybe datatype:

data Maybe a = Just a | Nothing

instance Monad Maybe where
    Nothing >>= _  = Nothing
    (Just x) >>= k = k x
    return = Just

maybe :: b -> (a -> b) -> Maybe a -> b
maybe n f Nothing  = n
maybe n f (Just x) = f x


maybeM :: (Monad m) => b -> (a -> b) -> m a -> b
maybeM = error "impossible"

You can't get things out of the Maybe Monad (without additional operations), but you can get from the Maybe datatype:

I'm not sure I take your meaning. I would say that the Maybe type constructor is a monad; there's no distinction between the "maybe monad" and the "maybe datatype".

It's true that the monad operations don't provide any way out of the monad, but every notable monad supports additional operations. Every monad in Haskell has to provide a way to construct a transformation of the type ∀a.m a → IO a, or else it can't be used by main or any function called by main. Most of them also provide a way to construct a transformation of type ∀a.m a → a; the only exception I can think of is IO.

I'm not sure I take your meaning. I would say that the Maybe type constructor is a monad; there's no distinction between the "maybe monad" and the "maybe datatype".

No.

It is common to identify the monad with the functor/type constructor as both mathematicians and computer scientists are wont to do with nearly everything, but, as the alternate name "triple" for monad suggests, there is more to a monad than the type constructor. A monad is a triple (T,return,join) that satisfies some laws. To emphasize this point, Maybe is a monad in at least two ways (but not a "notion of computation" a la Moggi, a strong monad with a mono return, in the following); besides the typical way, the definition:
return = Nothing; m >>= f = Nothing also, though I haven't listed them, satisfies the monad laws (trivially).

I'm not sure I take your meaning. I would say that the Maybe type constructor is a monad; there's no distinction between the "maybe monad" and the "maybe datatype".

No.

Oops. I was thinking about Haskell, where you get at most one instance of Monad per type, but, as you say, monads are more general.

I should have remembered that, because I noticed the same thing when I was working with error monads, which can be defined as monads two ways. For example, Haskell's Either type constructor has two monads: (Either a, Right, either Left id) and (Λa.Either a b, Left, either id Right).

[W]hat is the distinction between the Haskell Maybe monad, and the union type of ML?

None. You can define return and bind in ML just as easily as in Haskell. The only differences are, (1) Haskell overloads the operation names using type classes, and (2) Haskell's do-notation provides a convenient way to write monadic code.

Where do monads crop up in classical mathematics?

There is a one-to-one, onto relation between finitary monads on the category Set and finitary algebraic theories on Set. This means that all of the ubiquitous algebraic varieties, like monoids, groups, rings and modules are monads (but not fields, because division is partial). The unit operation says what a variable is; the multiplication operation encodes substitution modulo the laws. This means that whenever you want to talk about algebraic theories in a way which does not depend on their syntax/presentation (choice of operators or laws) monads are the appropriate tool. And if you want to talk about properties of ALL algebraic theories, then you can do it in an abstract fashion by studying properties of monads in general.

In poset theory, a monad is a closure operation, so when you talk about order-theoretic fixpoints you are talking about monads. And these are closely related to Galois connections, which are pervasive.

And while I'm at it, what is the distinction between the Haskell Maybe monad, and the union type of ML?

ML has no (primitive) union type. It has a way to form (almost) finitary coproducts, more or less as Haskell does. It is because people subscribe to oversimplifications like these that they end up frustrating themselves, trying to apply set theory where it isn't sound.

ML has no (primitive) union type

Could you please explain why this:

datatype A = L of a1 | R of a2;

is not a union type ? How is it different from what Luca Cardelli defines as the union type in his "Type Systems" (1997):

"An element of a union type A=A1+A2 can be thought of as an element of A1 tagged with a left token [...], or an element of A2 tagged with a right token [...]."

trying to apply set theory where it isn't sound

What exacly do you mean by that ? Could you give an example of such application ?

I essentially agree with the parent poster on the points raised. I think there is another, perhaps more general way of looking at monads as well though, and that is by regarding them as a way of specifying a very particular type of computational abstraction.

To understand what I mean by this, it is beneficial to looking at the types of monads already defined in the Haskell libraries. Consider the following:

• Error Monad - computations which may throw exceptions or produce well-known types of errors.
• IO Monad - computations which may depend on the success of input or output, or which may refer to values operating beyond the scope of the nominal purely functional evaluation.
• Maybe Monad - computations which may fail.
• Reader Monad - computations which maintain an environment (e.g., a set of lexically scoped variable bindings).
• State Monad - computations which may utilize mutable state (more general than the Reader monad)
• Writer Monad - computations which may produce some sort of additional 'notification' kind of output in addition to the nominal result.
• ...

From the above, it can be seen that each monad describes a sort of computation with particular characteristics. The monad abstraction facility is used to ensure that computations of a certain sort maintain a consistent handling of these characteristics across a program in a way that is verifiable by the type checker. Thus, monads provide a way to encode the behavior of computations themselves in the type system of the language.

As a side note, it makes even more sense to look at monads this way when you consider them as a special case of arrows, which are an even more flexible way of specifying the characteristcs of a computational style in the type system.

When do you use monads? Well, it depends. Some languages only expose certain functionality through a monadic interface, e.g., Haskell requires you to use the IO Monad to perform IO. In many other cases where monads are used, they are often not strictly necessary, but using them allows for a very neat and consistent way of handling certain styles of computational abstraction. For example, one may perform computations which are context sensitive by constantly passing the context around to different functions as an explicit parameter. Such a case, however, can be represented much more elegantly as a type of monadic computation in which the monad abstraction (e.g., Reader) handles the contextual details of the computation. By using a monad, a simplified interface to the necessary functionality can be provided, while the hard work of maintaining and passing the context is handled behind the scenes.

Thanks, that is the best explanation I've gotten so far. Most of the answers seemed to assume that the reader understands the basics of Haskel or have a degree in advanced math. Some follow up questions…

Without these monads, is there a way to control the sequence in which calculations are performed? Or is that strictly decided by the compiler/interpreter?

Without these monads, is there a way to control the sequence in which calculations are performed? Or is that strictly decided by the compiler/interpreter?

In a lazy functional language, the evaluation order of functions is deliberately left unspecified. That said, there are various things you can do within the framework of function application to ensure that function evaluations are ordered, by making the result of one function depend on the value returned by a second function (which must then be evaluated before the first function can be evaluated). Ultimately though, this can get pretty hairy, and what you end up doing is pretty much exactly what a monad does, except in an ad hoc fashion.

Monads provide a generalized, structured way to approach this problem. Understand, monads don't add anything new to an FP language, in terms of altering the semantics of the language. They're just a (to steal a term from another recent story) rather convenient design pattern. With the added advantage that the pattern in question obeys certain useful algebraic laws that make it easy to compose with other monads in interesting ways. Languages like Haskell have provided some convenient syntactic sugar to make this design pattern even easier to use. The resulting code ends up looking suspiciously like imperative code, but is really functional "under the hood".

Disclaimer:The preceding is, again, based on my own rather limited understanding of monads and their use in FP languages.

That's just the interface. It's important that the box of apples you get from return is a fresh box, and that the new box you get from join (aka mult) is somehow the combination of the boxes you had before.

The monad laws are:

• if you have a box of apples (m a) and get a fresh box of boxes of apples (m (m a)) and then combine all the boxes back into a box of apples, you get (the equivalent of) your original box of apples
• if you have a box of apples (m a) and, since I will give you a fresh box of apples for each apple (a -> m a), you get from me a box of fresh boxes of apples, and then combine all the boxes back into a box of apples, you get your original box of apples
• if you
  1. have a box of boxes of boxes of apples (m (m (m a))), and you take all the boxes of apples from each, combine all the now empty boxes into a new box and put the boxes of apples back in to get a box of boxes of apples, and then take out all the apples, combine all the boxes, and put the apples in, you get a box of apples which is exactly the same as if you
  2. have a box of boxes of boxes of apples (m (m (m a))), and since I will give you a box of apples for each box of boxes of apples (m (m a) -> m a), you get from me a box of boxes of apples, and then take all the apples and combine all the boxes to get a box of apples

I think that explanation would be really quite seriously terrific if it were animated, like the classic Project Mathematics stuff. Anybody reading this any good with Flash?

While I've read several things that say "monads are more than one thing" I think the extra note that it thus can easily lead to confusion helps it stay more clear in my mind.

The second class of examples can also fit in the first class. We may think of programming effectful computations with monads as some sort of meta-programming where the abstract data type represents a computation returning a value of some type.

To put it simply (hopefully), unit takes a value and returns a chunk of code that produces that value. Function bind takes two parameters, a code chunk and a code chunk generator (a function). The result (also a code chunk) reminds of run-time code generation: the result of the first chunk (when it is run) will steer the generation of the remaining code chunk by the second parameter.

In the case of the IO monad we build the pieces of code that do IO using the do notation, bind, unit and what have you. Then, we tell the IO interpreter to run our produced IO code by placing it in main.