Reputation: 3347
The 2002 paper "Composing monads using coproducts" seems to describe the following type construction:
Coprod R S a = ∀(T : Monad) → (∀b. R b → T b) → (∀b. S b → T b) → T a
Here R
, S
are lawful monads, and also the functions of types ∀b. R b → T b
and ∀b. S b → T b
are required to be lawful monad morphisms.
The paper does not show this construction explicitly but indicates it in words.
The cited paper's explicit results are limited to a certain subset of monads and, in particular, do not apply to the Reader monad, the State monad, the Continuation monad, the Selector monad, or the Codensity monad.
But it seems that Coprod
is a general construction that can completely replace the need for building monad stacks via monad transformers.
R
, is Coprod R
a universal way of constructing R
's monad transformer? If so, why aren't we using it, instead of complicated and limited monad transformers?Coprod
is equivalent to standard transformers for certain monads such as Maybe, Writer, and Either. Does Coprod R S
lead to different monad transformers than the known ones for standard monads (Reader, State, Continuation, etc.)?Coprod
in a library, or was that paper completely ignored? If so, why?Coprod R S
is a lawful monad.R a → Coprod R S a
and S a → Coprod R S a
.T
and for any monad morphisms of types R → T
and S → T
, there exist monad morphisms of types Coprod R S → T
, Coprod R S → Coprod T S
, and Coprod R S → Coprod R T
. In particular, this gives the hoist
functions for the resulting monad transformers.Coprod R S
is equivalent to Coprod S R
.Coprod R Id
is equivalent to R
. (Here, Id
is the identity monad.) This follows from the Yoneda lemma used in the category of monads.R
, Coprod R
is an endofunctor in the category of monads.Coprod R S
is a quotient of the free monad on R a + S a
. It is a "smaller" monad than the free monad on R a + S a
. The latter would be obtained by the same type formula as Coprod R S
but without the argument restrictions to monad morphisms.So, it appears that Coprod
is a nice, well-behaved construction that has all the nice properties one might wish for a monad transformer. (Not all standard monad transformers have all those properties. For instance, the continuation monad's standard transformer is not an endofunctor in the category of monads.)
The Coprod R S
constructor can be straightforwardly generalized to more monads (like, Coprod R S T U
and so on). This construction seems to replace the need for monad stacks.
Coprod R S
can be simplified to an equivalent type without quantifiers, for specific R
and S
, and whether Coprod R S
is equivalent to a combination of standard monad transformers.Coprod R S
is easier to use in practice than, say, MTL. Are there any pragmatic issues?IO
. Does it mean that we obtained a monad transformer for IO
? Several people argued that it would be impossible to have a lawful monad transformer for IO
. One argument is that a combination of IO
and Maybe
would sometimes need to revert the effects contained by IO
, which is impossible as not all IO
effects can be reverted.StateT
and MaybeT
do not commute: StateT s Maybe a
is a → Maybe (s, a)
while MaybeT (State s) a
is s → (s, Maybe a)
. But Coprod
is always symmetric, so Coprod (State s) Maybe
is the same as Coprod Maybe (State s)
. Is that yet another monad stack that combines State
and Maybe
in a way that is neither equivalent to StateT s Maybe
nor to MaybeT (State s)
?Upvotes: 0
Views: 47