monad-ideals: Ideal Monads and coproduct of Monads
Revives Control.Monad.Ideal from old versions of category-extras.
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 (category-theoretic 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.
--------
