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.

The 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.

Examples

Let us now see whether the example monads from the previous lunch can be derived from ideal monads (up to isomorphism).

Maybe

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 Pure.

Either

Also the Either monad can be derived from an ideal monad. This is just a generalization of the Maybe case.

[]

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]

The join method of [] is concat. So to define join' for 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.

Reader

The values of a type Reader r a are essentially functions from r to a. The pure computations are the constant functions. If r is nonempty, there is a one-to-one correspondence between the constant functions from r to a and the values of a. So the ideal monad type must be the type of nonconstant functions from r to 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 Reader.

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 join to (==) yields the function \ i -> i == i, which is const True.

State

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.