An introduction to ideal monads

Based on my recap of monads from the week before, I talked about ideal monads.

Ideal monads in category theory

Let \mathcal C be a category with coproducts. An ideal monad on \mathcal C is a pair (T', \mu') where T' : \mathcal C \to \mathcal C and \mu' : T'(\mathrm{Id} + T') \to T'. Certain restrictions apply to the choice of \mu', which we will discuss later.

From an ideal monad (T', \mu'), we can derive a monad (T, \eta, \mu) as follows:

\begin{array}{rcl}T & = & \mathrm{Id} + T' \\ \eta & = & \iota_1 \\ \mu & = & [\mathrm{id}_T, \iota_2\mu']\end{array}

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 \mathbf{Set} instead of \mathbf{Hask}, 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.

About these ads

4 thoughts on “An introduction to ideal monads

  1. 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 ())?

    • I don’t understand. All free monads are ideal monads, right?

      Yes.

      The free monad of the functor State S = get : 1 -> S + put : S -> 1, State S * X, can be used to express stateful computations.

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

      \mathrm{State}S = (S \to \mathrm{Id}) + (S \times \mathrm{Id})

      and take its free monad.

      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?

      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.

      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?

      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:

      newtype Parser t a = Parser
                               (Stream t -> [(a,Stream t)])

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

      data Parser t a = Read (t -> Parser t a)
                      | Output a (Parser t a)
                      | Stop

      With the latter definition, you can define an operator that turns parsers for languages L_1 and L_2 into a parser for L_1 \cup L_2 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.

      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 ())?

      This is fixed now. Thank you.

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

  3. Pingback: Three talks about ideal monads « Wolfgang Jeltsch

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s