Based on my recap of monads from the week before, I talked about ideal monads.
Ideal monads in category theory
Let be a category with coproducts. An ideal monad on is a pair where and . Certain restrictions apply to the choice of , which we will discuss later.
From an ideal monad , we can derive a monad as follows:
Ideal monads in Haskell
In Haskell, we can implement ideal monads and the translation from ideal monads to monads as follows:
class Functor m' => IdealMonad m' where join' :: m' (WithPure m' a) -> m' a data WithPure m' a = Pure a | Impure (m' a) instance Functor m' => Functor (WithPure m') where fmap f (Pure a) = Pure (f a) fmap f (Impure m') = Impure (fmap f m') instance IdealMonad m' => Monad (WithPure m') where return = Pure join (Pure m) = m join (Impure m'm) = Impure (join' m'm)
Note that we use the alternative
Monad class from the previous lunch here.
Values of monad types describe computations that may have effects. Pure computations, that is, computations without effects, are allowed as a corner case. They can be constructed using
return. Ideal monad types, on the other hand, do not cover pure computations, but only effectful ones. The
WithPure type constructor turns an ideal monad type into a monad type by adding the pure case.
join method of the
Monad class composes effects. It takes a computation
mm of type
m (m a) and turns it into a computation that performs
mm, takes its result, which is again a computation, and executes this result. The
join' method of
IdealMonad works analogously. However, its argument and its result cannot be pure. So if we compose an effectful computation with either a pure or an effectful computation, the result must be an effectful computation again. Composing an effectful computation with a pure computation yields a computation with the original effect; so there is no problem at this point. However, composing two effectful computations might lead to a pure computation. If this case occurs, we cannot use an ideal monad to model our effects.
Let us now see whether the example monads from the previous lunch can be derived from ideal monads (up to isomorphism).
No problems here. We define the ideal monad
Unit as follows:
data Unit a = Unit instance Functor Unit where fmap _ _ = Unit instance IdealMonad Unit where join' _ = Unit
Maybe is now isomorphic to
WithPure Unit, with
Nothing corresponding to
Impure Unit and
Just corresponding to
Either monad can be derived from an ideal monad. This is just a generalization of the
 monad expresses nondeterminism. Its pure computations are the singleton lists, because a singleton list corresponds to a computation that yields exactly one result and thus does not employ nondeterminism. So an ideal monad type for nondeterminism must contain the empty list and all lists with two or more elements:
data TrulyNondet a = None | Several a a [a]
join method of
concat. So to define
TrulyNondet, we must come up with a function
concat' :: TrulyNondet [a] -> TrulyNondet a
that essentially works like
concat. This is not possible, however, since an expression
concat' (Several  [a] ), for example, would have to yield a singleton list, which cannot be represented as a value of
TrulyNondet. We face the problem that composing two effectful computations can result in a pure computation.
Note that a monad of nonempty lists can be derived from an ideal monad, namely from the ideal monad that covers only lists with two or more elements.
The values of a type
Reader r a are essentially functions from
a. The pure computations are the constant functions. If
r is nonempty, there is a one-to-one correspondence between the constant functions from
a and the values of
a. So the ideal monad type must be the type of nonconstant functions from
a. However, such a type cannot be defined in Haskell. Even if we would use a language where such a type would be definable, the derived monad would not be isomorphic to
Reader r, because
WithPure allows us to decide whether a computation is pure or not, but such a decision cannot be made with
If we would work in instead of , coproducts would just be disjoint unions. So there would not be an issue with decidability. Still, we could not come up with a suitable ideal monad, since there is again the problem that composing two effectful computations can lead to a pure computation. Consider the function
(==) :: Integer -> Integer -> Bool ,
for example. It is nonconstant, since different integers
i lead to different functions
(i ==). However, applying
(==) yields the function
\ i -> i == i, which is
The state monad cannot be derived from an ideal monad. Consider, for example, the stateful computation
State $ \ s -> (State $ \ s' -> ((),pred s'),succ s) :: State Integer (State Integer ()) .
It is not pure, since it increments the state. However if we apply
join to it, we get
State $ \ s -> ((),s), which is pure, since the state does not change and the result does not depend on the state.