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.

Questions

1. For a fixed monad 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?
2. The paper showed that 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.)?
3. Did anyone implement this Coprod in a library, or was that paper completely ignored? If so, why?

What I can figure out

• Coprod R S is a lawful monad.
• There are monad morphisms of types R a → Coprod R S a and S a → Coprod R S a.
• For any monad 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.
• For a fixed 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.

Remarks

• It is far from obvious whether 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.
• It is not obvious whether Coprod R S is easier to use in practice than, say, MTL. Are there any pragmatic issues?
• The construction is applicable to all monads, including opaque external monads such as 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.
• Standard monad transformers 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)?