What is a monad in FP, in categorical terms?

Question

Every time someone promises to "explain monads", my interest is piqued, only to be replaced by frustration when the alleged "explanation" is a long list of examples terminated by some off-hand remark that the "mathematical theory" behind the "esoteric ideas" is "too complicated to explain at this point".

Now I'm asking for the opposite. I have a solid grasp on category theory and I'm not afraid of diagram chasing, Yoneda's lemma or derived functors (and indeed on monads and adjunctions in the categorical sense).

Could someone give me a clear and concise definition of what a monad is in functional programming? The fewer examples the better: sometimes one clear concept says more than a hundred timid examples. Haskell would do nicely as a language for demonstration though I'm not picky.

Answer 1

As a compliment to Carl's answer, a Monad in Haskell is (theoretically) this:

class Monad m where
  join :: m (m a) -> m a
  return :: a -> m a
  fmap :: (a -> b) -> m a -> m b

Note that "bind" (>>=) can be defined as

x >>= f = join (fmap f x)

According to the Haskell Wiki

A monad in a category C is a triple (F : C → C, η : Id → F, μ : F ∘ F → F)

...with some axioms. For Haskell, fmap, return, and join line up with F, η, and μ, respectively. (fmap in Haskell defines a Functor). If I'm not mistaken, Scala calls these map, pure, and join respectively. (Scala calls bind "flatMap")

Answer 2

This question has some good answers: Monads as adjunctions

More to the point, Derek Elkins' "Calculating Monads with Category Theory" article in TMR #13 should have the sort of constructions you're looking for: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

Finally, and perhaps this is really the closest to what you're looking for, you can go straight to the source and look at Moggi's seminal papers on the topic from 1988-91: http://www.disi.unige.it/person/MoggiE/publications.html

See in particular "Notions of computation and monads".

---

My own I'm sure too condensed/imprecise take:

Begin with a category Hask whose objects are Haskell types, and whose morphisms are functions. Functions are also objects in Hask, as are products. So Hask is Cartesian closed. Now introduce an arrow mapping every object in Hask to MHask which is a subset of the objects in Hask. Unit! Next introduce an arrow mapping every arrow on Hask to an arrow on MHask. This gives us map, and makes MHask a covariant endofunctor. Now introduce an arrow mapping every object in MHask which is generated from an object in MHask (via unit) to the object in MHask which generates it. Join! And from the that, MHask is a monad (and a monoidal endofunctor to be more precise).

I'm sure there is a reason why the above is deficient, which is why I'd really direct you, if you're looking for formalism, to the Moggi papers in particular.

Answer 3

Ok, using Haskell terminology and examples...

A monad, in functional programming, is a composition pattern for data types with the kind * -> *.

class Monad (m :: * -> *) where
    return :: a -> m a
    (>>=)  :: m a -> (a -> m b) -> m b

(There's more to the class than that in Haskell, but those are the important parts.)

A data type is a monad if it can implement that interface while satisfying three conditions in the implementation. These are the "monad laws", and I'll leave it to those long-winded explanations for the full explanation. I summarize the laws as "(>>= return) is an identity function, and (>>=) is associative." It's really not more than that, even if it can be expressed more precisely.

And that's all a monad is. If you can implement that interface while preserving those behavioral properties, you have a monad.

That explanation is probably shorter than you expected. That's because the monad interface really is very abstract. The incredible level of abstraction is part of why so many different things can be modeled as monads.

What's less obvious is that as abstract as the interface is, it allows generically modeling any control-flow pattern, regardless of the actual monad implementation. This is why the Control.Monad package in GHC's base library has combinators like when, forever, etc. And this is why the ability to explicitly abstract over any monad implementation is powerful, especially with support from a type system.

Answer 4

You should read the paper by Eugenio Moggi "Notions of computations and monads" which explain the then proposed role of monads to structure denotational semantic of effectful languages.

Also there is a related question:

References for learning the theory behind pure functional languages such as Haskell?

As you don't want hand-waving, you have to read scientific papers, not forum answers or tutorials.

Answer 5

A monad is a monoid in the category of endofunctors, whats the problem?.

Humor aside, I personally believe that monads, as they are used in Haskell and functional programming, are better understood from the monads-as-an-interface point of view (as in Carl's and Dan's answers) instead of from the monads-as-the-term-from-category-theory point of view. I have to confess that I only really internalized the whole monad thing when I had to use a monadic library from another language in a real project.

You mention that you didn't like all the "lots of examples" tutorials. Has anyone ever pointed you to the Awkward squad paper? It focuses manly in the IO monad but the introduction gives a good technical and historical explanation of why the monad concept was embraced by Haskell in the first place.

Answer 6

I don't really know what I'm talking about, but here's my take:

Monads are used to represent computations. You can think of a normal procedural program, which is basically a list of statements, as a bunch of composed computations. Monads are a generalization of this concept, allowing you to define how the statements get composed. Each computation has a value (it could just be ()); the monad just determines how the value strung through a series of computations behaves.

Do notation is really what makes this clear: it's basically a special sort of statement-based language that lets you define what happens between statements. It's as if you could define how ";" worked in C-like languages.

In this light all of the monads I've used so far makes sense: State doesn't affect the value but updates a second value which is passed along from computation to computation in the background; Maybe short-circuits the value if it ever encounters a Nothing; List lets you have a variable number of values passed through; IO lets you have impure values passed through in a safe way. The more specialized monads I've used like Gen and Parsec parsers are also similar.

Hopefully this is a clear explanation which isn't completely off-base.

Answer 7

Since you understand monads in the category-theoretic sense I am interpreting your question as being about the presentation of monads in functional programming. Thus my answer avoids any explanation of what a monad is, or any intuition about its meaning or use.

Answer: In Haskell a monad is presented, in an internal language for some category, as the (internalised) maps of a Kleisli triple.

Explanation: It is hard to be precise about the properties of the "Hask category", and these properties are largely irrelevant for understanding Haskell's presentation of monads. Instead, for this discussion, it is more useful to understand Haskell as an internal language for some category C. Haskell functions define morphisms in C and Haskell types are objects in C, but the particular category in which these definitions are made is unimportant.

Parameteric data types, e.g. data F a = ..., are object mappings, e.g. F : |C| -> |C|.

The usual description of a monad in Haskell is in Kleisli triple (or Kleisli extension) form:

class Monad m where
    return :: a -> m a
    (>>=) :: m a -> (a -> m b) -> m b

where:

• m is the object mapping m :|C| -> |C|
• return is the unit operation on objects
• >>= (pronounced "bind" by Haskellers) is the extension operation on morphisms but with its first two parameters swapped (cf. usual signature of extension (-)* : (a -> m b) -> m a -> m b)

(These maps are themselves internalised as families of morphisms in C, which is possible since m :|C| -> |C|).

Haskell's do-notation (if you have come across this) is therefore an internal language for Kleisli categories.

Answer 8

The Haskell wikibook page has a good basic explanation.