Three things I don't understand about monads

Monads are a remarkably powerful tool for building specialized programming languages. Some examples include:

But there’s a bunch of things I don’t understand about monads. In each case, my confusion involves some aspect of the underlying math that “bubbles up” to affect the design of specialized languages.

(Warning: Obscure monad geeking ahead.)

Commutative monads

A “commutative monad” is any monad where we can replace the expression:

do a <- ma
   b <- mb
   f a b

…with:

do b <- mb
   a <- ma
   f a b

…without changing the meaning. Examples of commutative monads include Reader and Rand. This is an important property, because it might allow us to parallelize the commonly-used sequence function across huge numbers of processors:

sequence :: (Monad m) => [m a] -> m [a]

Simon Peyton Jones lists this problem as Open Challenge #2, saying:

Commutative monads are very common. (Environment, unique supply, random number generation.) For these, monads over-sequentialise.

Wanted: theory and notation for some cool compromise.

Commutative monad morphisms

~~Monad morphisms are the category theory equivalent of Haskell's [monad transformers][transformers].~~

Haskell’s monad transformers can be expressed as monad layerings, which correspond to the monad morphisms of category theory.

Many complicated monads break down into a handful of monad transformers, often in surprising ways.

But composing monad transformers is a mess, because they interact in poorly-understood ways. In general, the following two types have very different semantics:

FooT (BarT m)
BarT (FooT m)

If FooT and BarT commute with each other, however, the two types would be equivalent. This is helpful when building large stacks of monad transformers.

Chung-chieh Shan encountered a related problem when applying monad morphisms to build a theory of natural language semantics:

It remains to be seen whether monads would provide the appropriate conceptual encapsulation for a semantic theory with broader coverage. In particular, for both natural and programming language semantics, combining monads---or perhaps monad-like objects---remains an open issue that promises additional insight.

Monad morphisms and abstract algebra

Dan Piponi has been drawing some fascinating connections between monad morphisms and abstract algebra. See, for example:

This approach seems to throw a lot of light on monad morphisms—but at least in my case, the light only highlights my confusion.

Of the three problems listed here, this is the one most likely to be discussed in a textbook somewhere. And a solution to this problem would likely help significantly with the other two.

So, my question: Does anybody have any books, papers or ideas that might help untangle this mess?

Update: Be sure to see the comment thread on the second Dan Piponi post above and Chung-chieh Shan’s excellent bibliography on monad transformers.

Josef Svenningsson wrote on Mar 05, 2007:

About commutative monads: I totally agree that we need some nicer ways of programming with them and make use of the commutativity. I anticipate that there's a lot of fun/useful things that can come out that. As for monad transformers and whether they commute or not: I don't see the problem. Some monad transformers commute, some don't. There might be deeper things to be said about it but you can get a long way if you just accept that commutativity is a property that some, but not all, monad transformer obeys.

Eric wrote on Mar 05, 2007:

Whether FooT and BarT commute (sometimes? often? always?) depends on the algebraic properties of Foo and Bar. There's all sorts of neat stuff going on that I can't quite grasp. For example, (ListT m) is only a monad when m is a commutative monad. And as Dan showed, this is related to properties of freely-generated semirings. I suspect that there's something deeper to be said about these issues, and that it might be important for monad-based DSLs. Anyway, here's a list of resources that might be relevant: - Mark Jones and Luc Duponcheel's Composing monads, an early paper on monad transformers that noticed some interesting limits to what could be composed. - Edmund Robinson's Variations on Algebra: monadicity and generalisations of equational theories, which describes a fascinating relationship between initial algebras and monads. (Thanks, alpheccar!) - According to Michi, enriched categories provide some insight into these kinds of layerings. So far, I've found Basic Concepts of Enriched Category Theory and a Wikipedia article, but I haven't dug into this area yet (it's getting a bit heavy for my current knowledge of category theory).

sigfpe wrote on Mar 05, 2007:

I agree with SPJ, I'd put a nice notation for commutative monads as my #2 want for Haskell. My #1 is a way to make efficient commutative monads in the first place eg. dealing with the problems of defining Set so that bind can use (==) without using ugly hacks. Hmmm...there would be a neat spinoff from a nice commutative monad notation. It would be easier to write strict code in Haskell.

Neel Krishnaswami wrote on Mar 07, 2007:

The connection between monads and algebras is one that I'm actually very surprised functional programmers don't use -- monads were invented to talk about algebras, and are really beautiful when you need to do things like enrich a syntax with variables (eg, for unification algorithms). Michi is right about enriched category theory being relevant here. One of the bad things about monads as they are commonly used is that there's no theory for the operations in a monad, and that's the most important part! Power and Plotkin have been looking at how to derive a monad given a set of algebraic operations (for example, if you've got get and set, can you derive the state monad?), and enriched categories show up.

Chung-chieh Shan wrote on Mar 11, 2007:

A quick observation about commutative monads: it seems that most (all?) examples of useful commutative monads also obey the law that "m >> n" is equivalent to "n". Intuitively, if you don't need the result of an action in a commutative monad, then you don't need the effect either. This law holds morally for environment, unique supply, and random-number generation. It also holds for the probability monad (yay!). It may or may not hold in the strictness monad, depending on your morality. This law makes me wonder if we can think of >>= in a commutative monad as expressing data flow. I guess I'm not the first person to wonder about overloading function application (aka whitespace or juxtaposition) for some purpose...

Stefan Ljungstrand wrote on Mar 13, 2007:

CCS : When 'o' is a commutative monoid, the 'Writer o' monad is commutative, but actions are still not discardable.

Commutative monads

Commutative monad morphisms

Monad morphisms and abstract algebra

More posts