[Haskell-cafe] Origin of monad transformers (was: Algebraic Effects?)
Olaf Klinke
olf at aatal-apotheke.de
Thu Sep 20 19:35:35 UTC 2018
> The only monads with distributive laws are in Data.Distributive, and
> they're all isomorphic to (->) e for some e. So that's effectively
> ReaderT.
That is true for this particular signature of distributive law, and I find this a fascinating result. Especially because there are Haskell terms witnessing this categorical fact.
In [1, Theorem 2.4.2] it is stated (as I understand it) that if two monads H and K have a distributive law, then the first is a functor on the Kleisli category of the second while the second is a functor on the Eilenberg-Moore category of the first. In the same paper, Section 4 describes monads on Set (including e.g. trees, bags, Maybe) which distribute over all commutative monads.
But maybe one does not need such heavy categorical machinery to describe where monad transformers in Haskell come from. Consider the following.
There are at least three kinds of monad transformers t in mtl:
(1) t m a = m (t' a) for some monad t' (e.g. ExceptT)
(2) t m a = t' (m a) for some monad t' (e.g. ReaderT)
(3) t m a = g (m (f a)) for some functors g and f. (e.g. StateT)
Only (2) is of the Data.Distributive kind, but all three can be unified under the following scheme:
Lemma:
If F ⊣ G is an adjunction where F: C → D and G: D → C
are functors, and if M: D → D is a monad on D,
then G∘M∘F is a monad.
Proof:
One can factor M through the Kleisli category of M
L ⊣ R where L: D → Kleisli(M) and R: Kleisli(M) → D.
Since adjoints compose, we have
L∘F ⊣ G∘R and G∘R∘L∘F = G∘M∘F.
q.e.d.
There is another interesting paper [2] showing that for certain class of monads, checking the conditions for a distributive law is easier than the general case.
Olaf
[1] http://emis.ams.org/journals/TAC/volumes/18/7/18-07.pdf
[2] https://doi.org/10.1016/S0022-4049(01)00097-4
More information about the Haskell-Cafe
mailing list