[Prev][Next][Index][Thread]
monad composition as a relation
It is possible to view monad composition as a relation, rather than a
function.
The notion of "monad compatibility" is described in Triples, Toposes,
and Theories by Barr and Wells, page 316. They also describe the Swap
construction, rediscovered by Jones and Duponcheel in their Yale
Research Report (number 1004) on monad composition.
Suppose we have three monads
T = (T, unit, map, join)
T1 = (T1, unit1, map1, join1)
T2 = (T2, unit2, map2, join2)
For T to be the composition of T1 and T2, we require
T = T2 o T1
unit = map2(unit1) o unit2 = unit2 o unit1 (C1)
join o map(unit2) = map2(join1) (C2)
join o map2(unit1) = join2 (C3)
Barr and Wells also give (C4) and (C5) which are exactly (J1) and (J2)
from Jones and Duponcheel, but these seem to pertain specifically to
the Swap construction rather than to monad composition in general.
These three laws permit a "relational category" with monads as arrows.
That is, composition of two arrows yields a SET of arrows, rather than
a single arrow. We require that composition with the identity yields
a singleton set and that associativity holds (which I haven't
checked).
The notion of a "relational category" can't be new; I would appreciate
the proper name and a reference. It would also be nice to see pairs
of monads with multiple (interestiing) compositions.
Although we can't compute compositions directly, we can use these
ideas to reason about compositions derived from other methods
(distributive laws, monad transformers).
David