by Mauro Jaskelioff on February 4, 2008. Tagged as: Lunches.

Monad transformers were introduced as a programming technique many years ago, but we are still not sure what mathematical structure they are. For example, we still don’t know if every monad has an associated monad transformer, or even if every monad should have just one associated monad transformer.

John Power argues that monad transformers should come before monads since every M-monad transformer gives raise to a monad M by applying it to the identity monad. One structure that comes before monads is adjunctions: every adjunction gives rise to a monad . Also, every monad can be split into an adjunction. There are usually many adjunctions a monad can be split into, but there are two canonical ones: the Kleisli and the Eilenberg-Moore (which are the initial and the final splittings in some sense).

Now, given an adjunction and a monad on , we can choose any adjunction giving rise to it and use adjoint composition to obtain a monad on .

So, a monad transformer for a monad might be explained by a choice of an adjunction splitting and a lifting of monads in to monads in .

If the choice of the adjunction is the Eilenberg-Moore one, then the lifting of is given by a distributive law of monads , and the obtained monad is . For example, this explains the standard Haskell monad transformers for Maybe and Writer.

If the choice of the adjunction is the Kleisli one, then the lifting of is given by a distributive law of monads , and the obtained monad is . For example, this explains the standard Haskell monad transformers for Reader and Cont.

The State monad transformer is not explained by any of the canonical adjunctions splitting the monad, but by the currying/uncurrying adjunction characterizing exponentials: