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:

classFunctor m' => IdealMonad m'wherejoin' :: m' (WithPure m' a) -> m' adataWithPure m' a = Pure a | Impure (m' a)instanceFunctor m' => Functor (WithPure m')wherefmap f (Pure a) = Pure (f a) fmap f (Impure m') = Impure (fmap f m')instanceIdealMonad m' => Monad (WithPure m')wherereturn = 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:

dataUnit a = UnitinstanceFunctor Unitwherefmap _ _ = UnitinstanceIdealMonad Unitwherejoin' _ = 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:

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

I don’t understand. All free monads are ideal monads, right? The free monad of the functor State S = get : 1 -> S + put : S -> 1, State S * X, can be used to express stateful computations. I can believe that State S * X isn’t isomorphic to the state monad as defined in Haskell’s prelude (even though I don’t understand why), but what practical difference does it make? Is there anything you can’t do with State S * X that you can with the state monad from Haskell’s prelude? If there is a free monad of state that is, practically, as good as the prelude one, then there ought to be an ideal one as well?

PS. I believe the type of the stateful computation at the end of the post is wrong; shouldn’t it be: State Int (State Int ())?

Yes.

Hmm, is it really that functor? With “1”, you mean the identity functor, right? I would take the functor defined by

and take its free monad.

At least the free monad of my functor is not isomorphic to the ordinary state monad, because it conveys more information. In the example from the article above, the

`join`

result tells only that the initial state and the final state are the same. If we would use the free monad, it would also tell that the state changes temporarily.What is “practically as good”? Both kinds of state monads are different also in practice. You cannot do exactly the same things with them. There is a similar case for parsers. You can define parsers based on state monads:

And you can define them such that they explicitly talk about atomic operations (reading a token and emitting one of possibly many outputs):

With the latter definition, you can define an operator that turns parsers for languages and into a parser for that runs both given parsers in parallel by interleaving them, so to say. This is only possible, because we know the internal structure of the parser. It is not possible with the parser definition based on state monads.

This is fixed now. Thank you.

Pingback: What is the correct definition of ideal monads? | Theory Lunch

Pingback: Three talks about ideal monads « Wolfgang Jeltsch