Reputation: 1144
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?
Upvotes: 34
Views: 1926
Reputation: 3347
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
Upvotes: 0
Reputation: 571
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.
Upvotes: 3
Reputation: 38891
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
Upvotes: 8