monadideals: Ideal Monads and coproduct of Monads
Revives Control.Monad.Ideal
from old versions of categoryextras.
Ideal Monads
Ideal monads are certain kind of monads. Informally, an ideal monad M
is a Monad
which can be written as a disjoint union of "pure" values and "impure" values,
and its join
operation on "impure" values never produces "pure" values.
data M a = Pure a  Impure (...)
pure :: a > M a
pure = Pure
join :: M (M a) > M a
join (Pure ma) = ma
join (Impure ...) = Impure (...)
 Impure values of @M a@ never becomes pure again
Formally, an ideal monad m
is a Monad
equipped with
Functor m₀
, called the ideal part of m
 Natural isomorphism
iso :: ∀a. Either a (m₀ a) > m a
(and its inverse iso⁻¹ :: ∀a. m a > Either a (m₀ a)
)
 Natural transformation
idealize :: ∀a. m₀ (m a) > m₀ a
satisfying these two properties.
iso . Left === pure :: ∀a. a > m a
either id (iso . Right . idealize) . iso⁻¹ === join :: m (m a) > m a
This package provides MonadIdeal
, a type class to represent ideal monads in terms of
its ideal part m₀
(instead of a subclass of Monad
to represent ideal monad itself.)
class (Isolated m0, Bind m0) => MonadIdeal m0 where
idealBind :: m0 a > (a > Ideal m0 b) > m0 b
type Ideal m0 a
  Constructor of @Ideal@
ideal :: Either a (m0 a) > Ideal m0 a
  Deconstructor of @Ideal@
runIdeal :: Ideal m0 a > Either a (m0 a)
Here, Ideal m0
corresponds to the ideal monad which would have m0
as its ideal part.
Isolated
class
There is a generalization to ideal monads, which are almost ideal monads,
but lack a condition that says "an impure value does not become a pure value by the join
operation".
A monad m
in this class has natural isomorphism Either a (m₀ a) > m a
with some functor m₀
, and
pure
is the part of m
which is not m₀
. Formally, the defining data of this class are:
Functor m₀
, called the impure part of m
 Natural isomorphism
iso :: ∀a. Either a (m₀ a) > m a
(and its inverse iso⁻¹ :: ∀a. m a > Either a (m₀ a)
)
iso . Left === pure :: ∀a. a > m a
Combined with the monad laws of m
, join :: ∀a. m (m a) > m a
must be equal to the following natural transformation
with some impureJoin
.
join :: ∀a. m (m a) > m a
join mma = case iso⁻¹ mma of
Left ma > ma
Right m₀ma > impureJoin m₀ma
where
impureJoin :: ∀a. m₀ (m a) > m a
The Isolated
class is a type class for a functor which can be thought of as an
impure part of some monad.
newtype Unite f a = Unite { runUnite :: Either a (f a) }
class Functor m0 => Isolated m0 where
impureBind :: m0 a > (a > Unite m0 b) > Unite m0 b
Coproduct of monads
Coproduct m ⊕ n
of two monads m, n
is the coproduct (categorytheoretic sum) in the category of monad
and monad morphisms.
In basic terms, m ⊕ n
is a monad with the following functions and properties.

Monad morphism inject1 :: ∀a. m a > (m ⊕ n) a

Monad morphism inject2 :: ∀a. n a > (m ⊕ n) a

Function eitherMonad
which takes two monad morphisms and return a monad morphism.
eitherMonad :: (∀a. m a > t a) > (∀a. n a > t a) > (∀a. (m ⊕ n) a > t a)

Given arbitrary monads m, n, t
,

For all monad morphisms f1
and f2
,
eitherMonad f1 f2 . inject1 = f1
eitherMonad f1 f2 . inject2 = f2

For any monad morphism f :: ∀a. (m ⊕ n) a > t a
, f
equals to eitherMonad f1 f2
for some unique f1, f2
.
Or, equvalently, f = eitherMonad (f . inject1) (f . inject2)
.
Coproduct of two monads does not always exist, but for ideal monads or monads with Isolated
impure parts,
their coproducts exist. This package provides a type constructor (:+)
below.
 Control.Monad.Coproduct
data (:+) (m :: Type > Type) (n :: Type > Type) (a :: Type)
Using this type constructor, coproduct of monad can be constructed in two ways.

If m0, n0
are Isolated
i.e. the impure part of monads Unite m0, Unite n0
respectively,
m0 :+ n0
is also Isolated
and Unite (m0 :+ n0)
is the coproduct of monads Unite m0 ⊕ Unite n0
.

If m0, n0
are MonadIdeal
i.e. the ideal part of ideal monads Ideal m0, Ideal n0
respectively,
m0 :+ n0
is also MonadIdeal
and Ideal (m0 :+ n0)
is the coproduct of monads Ideal m0 ⊕ Ideal n0
.
Duals
This package also provides the duals of ideal monads and coproducts of them: Coideal comonads and products of them.
