What are Haskell's monad transformers in categorical terms?

31
votes

As a math student, the first thing I did when I learned about monads in Haskell was check that they really were monads in the sense I knew about. But then I learned about monad transformers and those don't quite seem to be something studied in category theory.

In particular I would expect them to be related to distributive laws but they seem to be genuinely different: a monad transformer is expected to apply to an arbitrary monad while a distributive law is an affair between a monad and a specific other monad.

Also, looking at the usual examples of monad transformers, while MaybeT m composes m with Maybe, StateT m is not a composition of m with State in either order.

So my question is what are monad transformer in categorical language?

3
haskellmonad-transformerscategory-theory
They say a monad transformer in C is a pointed endofunctor (a.k.a. pre-monad) on Monad(C). I'm not sure I understand this definition though. Maybe you do? Then please share ;) – n. 1.8e9-where's-my-share m.
This article looks like a good place to start. – hammar
@n.m. Unpacking "pointed endofunctor on Monad(C)" you get that a monad transformer t is something that (1) for each monad m gives you a monad t m and (2) for each monad morphism m->n gives you another monad morphism t m -> t n in a functorial way (i.e., respecting compositions) and t comes with (3) for any monad m, a monad morphism m -> t m which is natural (i.e., for a monad morphism the obvious square you get with vertices m, n, t m, t n commutes). (Endofunctor on Monad(C) is (1) and (2), pointed is (3).) – Omar Antolín-Camarena
OK, I think the article hammar linked to answers my question: for what they are used for in Haskell programming, monad transformers only need to send monads to monads and allow the extra operations of monads to be lifted. So they are just functions from the set of Monads to itself, not even endofunctors on Monad(Hask), although in practice all the useful ones save for ContT are functorial. If you post your link as answer, hammar, I'd be happy to accept it. – Omar Antolín-Camarena
@Omar: I would suggest you expand that comment into an answer of your own question, there is nothing wrong in doing that. Just make sure that it is selfcontained, ie. add hammars link to it =D. – HaskellElephant

3 Answers

8
votes

Monad transformers aren't exceedingly mathematically pleasant. However, we can get nice (co)products from free monads, and, more generally, ideal monads: See Ghani and Uustalu's "Coproducts of Ideal Monads": http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.2698

3
votes

Calculating monad transformers with category theory by Oleksandr Manzyuk is another article on the Monad transformers, and relates the concept to the important concept of adjunction in the category theory.
Also it uses the most pleasant feature of the category theory, in my opinion, i.e. diagram-chasing, which naturalises the concept a lot.
Hope this helps.

0
votes

A monad transformer is a pointed endofunctor in the category of monads. "What's the problem?"

Here are some more details:

Start with some category, in which we consider those endofunctors M that are monads. All those monads M form a category whose morphisms are natural transformations M -> M' that satisfy the laws of monad morphisms.

A monad transformer is a pointed endofunctor in this category of monads. What is an endofunctor T in this category of monads? This endofunctor is a mapping from a monad M to a monad T(M), together with a mapping of any monad morphism M -> M' into a monad morphism T(M) -> T(M').

The endofunctor T is "pointed" if there exists a natural transformation from the identity endofunctor (Id) to T.

The identity endofunctor is an identity map of monads and monad morphisms. A natural transformation Id ~> T is defined by its components at all the monads M. Its component at M is a monad morphism M -> T(M). In addition, there must be a naturality law ("monadic naturality") which says that, for any monads M and M' and any monad morphism M -> M', the diagram consisting of M, M', T(M), T(M') commutes.

This data more or less coincides with the usual data required of a monad transformer. The required monad morphism M -> T(M) is the lifting of the "foreign" monad M into the transformed monad.

The construction also includes the "hoist" function (this is the action of the endofunctor T on monad morphisms), that lifts monad morphisms M -> M' to T(M) -> T(M').

If we consider the image of the identity monad, T(Id), this must be some other monad. Call that the "base monad" of the transformer and denote it by B. We have then the monad morphism B ~> T(M) for any M. This is the lifting from the base monad to the transformed monad.

However, this definition excludes the "non-functorial" monad transformers, such as that of the continuation monad and the codensity monad.

The distributive laws are only relevant to certain monad transformers. There are two kinds of transformers where distributive laws exist: for these transformers, the component at M of the natural transformation Id ~> T is given either by M -> B∘M or by M ->M∘B. But other monads have transformers that are not functor compositions, and there are no distributive laws for them.

More details are written up in Chapter 14 of the upcoming book "The Science of Functional Programming": https://github.com/winitzki/sofp