ZedneWeb
Insert motto here

Parameterized monads vs monads over indexed types

By Dave Menendez
Sunday, July 29, 2012, at 2:25 AM
Filed under: Haskell

Summary: Parameterized monads are a known way of extending the monadic interface. As an alternative, Conor McBride suggested using monads over indexed types. How do these approaches compare?

I’ve been meaning to write about this for a while, but I kept getting stuck trying to introduce the topic. So instead, I’ll just jump into it and refer people to the original paper for more detail. (If you’ve already read McBride’s “Kleisli arrows of outrageous fortune”, you may want to skip to the new stuff towards the end.)

Paramonads

One abstraction that’s been floating around the Haskell community for a while is the parameterized monad—or “paramonad”, as I like to call it. Dan Piponi has a good brief introduction to them, but the general idea is that paramonads extend the familiar monad abstraction by adding a type-level index which can change over the course of a computation.

Here’s a class definition:

class Paramonad m where
    preturn :: a -> m i i a
    pbind :: (a -> m j k b) -> m i j a -> m i k b

Here, x :: m i j a is a computation that returns a value of type a but also contains a transition from i to j. The nature of the transition depends on the specific paramonad. For state transformers, it indicates the type of the internal state:

newtype PState i j a = PState (i -> (a,j))

For delimited continuations, it indicates the return type:

newtype PCont i j a = PCont ((a -> j) -> i)

But the state may be entirely abstract: one can define a paramonad which keeps track of allocated resources in its type. In this way, the programmer can statically guarantee that all allocated resources are eventually de-allocated, and that no attempt is made to access a de-allocated resource.

For simplicity, imagine that we only want to work with one resource—say, a file—at a time. We’ll define some types to indicate whether a file is open:

data Open
data Closed

Here are the types of our basic operations:

open  :: FilePath -> FH Closed Open ()
read  :: FH Open Open (Maybe Char)
close :: FH Open Closed ()

The type of read indicates that it has to come between open and close. Similarly, we can use the type of our run function to ensure that all open files are eventually closed:

run :: FH Closed Closed a -> IO a

Now, bad programs such as run (open "Foo") and run read are rejected during compilation.

Adding dynamism

The problem with the scheme given above is that it’s too static. Some resource allocations may fail—for example, the file might not exist—but the interface given above can’t handle that. We might try exceptions, but there isn’t any good way to handle them inside the paramonad—especially once we start dealing with more complex states involving multiple resources.

One possibility is to remake open to require a continuations for handling successful and unsuccessful allocation:

open :: FilePath 
    -> FilePath Closed i a  -- on failure
    -> FilePath Open i a    -- on success
    -> FilePath Closed i a

Again, this becomes unweildy once we start to work with multiple resources.

Fortunately, Conor McBride has come up with an alternative, which he describes in his paper “Kleisli Arrows of outrageous fortune”. Instead of defining a variation on monads, McBride shifts attention to the category of indexed-types and index-preserving functions.

type p :-> q = forall i. p i -> q i

A simple example of an indexed type would be lists which indicate their length in their type—so List a n is a list with n elements. These can be defined using the GADTs extension to Haskell. A function which reverses the elements of a list without changing the length is index-preserving.

Because the monad abstraction isn’t tied to any particular category, we can define a class for monads over index-preserving functions.

class IMonad m where
    iskip   :: p :-> m p
    iextend :: (p :-> m q) -> (m p :-> m q)

Compare that to the familiar Monad class. Aside from names and the order of arguments, the only difference is the choice of category.

McBride also defines a more familiar-looking synonym:

(?>=) :: IMonad m => m p i -> (p :-> m q) -> m q i
m ?>= f = iextend f m

We can view the indexed types, such as p and m q, as making claims about the index. So a value of type p i indicates that claim p is possible in state i, and a function f :: p :-> m q says that m q is true when p is true. Similarly, the monads can indicate transitions in the index. In other words, x :: m p i says that m p is possible in state i, but claim p might be about some other state. That’s why the first argument to iextend has to be defined for all possible indicies.

The strongest claim is that the index is some specific value. The type a := i provides a value of type a and a claim that the current index is i.

data (a := i) j where
    V :: a -> (a := i) i

Now we can define some more restricted versions of iskip and iextend:

ireturn :: IMonad m => a -> m (a := i) i
ireturn = iskip . V

(=>=) :: IMonad m => m (a := j) i -> (a -> m p j) -> m p i
m =>= f = m ?>= \(V a) -> f a

A value x :: m (a := j) i is a computation that produces a value of type a and changes the index from i to j.

Now, we can describe that open can either succeed or fail. First, a type to indicate choice:

data (p :\/ q) i = L (p i) | R (q i)

Then, the operations over our monad FH:

open  :: FilePath -> FH (() := Closed :\/ () := Open) Closed
read  :: FH (Maybe Char := Open) Open
close :: FH (() := Closed) Open

Now it’s clear that open may result in one of two possible states: either the file is open or not. Furthermore, the type system will only allow us to call read and close if open succeeds.

In short, this will typecheck:

ex_good :: FH (Maybe Char := Closed) Closed
ex_good = open "Foo" ?>= \x ->
    case x of
        L (V ()) -> ireturn Nothing
        R (V ()) -> read =>= \c -> close =>= \() -> ireturn c

This will not:

ex_bad :: FH (Maybe Char := Closed) Closed
ex_bad = open "Foo" ?>= \_ -> read =>= \c -> close =>= \() -> ireturn c

At this point, it might not seem as we’ve gained much. Instead of writing,

open file on_failure on_success

we write

open file ?>= \x -> case x of
    L (V _) -> on_failure
    R (V _) -> on_success

But the fact that :\/ is just another indexed type allows us to work more within our framework. For example, if we have a convention that L is used for failure, we can create a general recovery form:

orElse :: m (() := j :\/ q) i -> m (p :\/ q) j -> m (p :\/ q) i
m1 `orElse` m2 = m1 ?>= \x ->
    case x of
        L (V _) -> m2
        R q -> iskip q

Now we can write things like this:

open file1 `orElse` open file2 ?>= \x -> case x of
    L (V _) -> on_failure
    R (V _) -> on_success

Doing this with the continuation-based open is possible, but it gets complicated very fast.

Back to paramonads

I mentioned that x :: m (a := i) j is a computation that produces an a and changes the index from i to j. This sounds an awful lot like what a paramonadic computation does, and in fact we can map any instance of IMonad to an instance of Paramonad.

newtype PI m i j a = PI (m (a := j) i)
unPI (PI m) = m

instance IMonad m => Paramonad (PI m) where
    preturn = PI . ireturn
    pbind m f = PI (unPI m =>= unPI . f)

This suggests that IMonad is at least as powerful as Paramonad.

We’ve already shown that one of the standard uses for paramonads can be expressed using IMonad, but what about state transforming and continuations?

For state, the index of the computation will determine the input state, and the index of the result will determine the output state. But since the result may have an arbitrary index, we will need an existential type.

data Dyn p = forall i. Dyn (p i) i

newtype State p i = State (i -> Dyn p)
unState (State f) = f

instance IMonad State where
    iskip p = State (\i -> Dyn p i)

    iextend f m = State (\i -> 
        case unState m i of
            Dyn p j -> unState (f p) j)

For continuations, the result determines the intermediate return type.

newtype Cont p i = Cont ((forall j. p j -> j) -> i)
unCont (Cont f) = f

instance IMonad Cont where
    iskip p = Cont (\k -> k p)
    iextend f m = Cont (\k -> unCont m (\p -> unCont (f p) k))

It’s worth convincing yourself that PI Cont is essentially the same as PCont from above. In particular, for Cont (a := k) i, the continuation will have the type forall j. (a := k) j -> k; but since (a := k) j can only have values when k equals j, we can easily transform a function f :: a -> k into the function (\(V a) -> f a) :: forall j. (a := k) j -> j.

We can generalize further, incidentally, by adding another indexed type:

newtype ICont q p i = ICont ((p :-> q) -> q i)
newtype Id a = Id a

Now, Cont p i is isomorphic to ICont Id p i.

A similar generalization is possible for State.

Now that all of our paramonad examples turn out to be expressible as monads over indexed types, it’s worth considering whether every paramonad can be mapped to IMonad. For a long time, I was convinced this was impossible, because paramonads require the index transitions be known statically, but monads over indexed types allow dynamic transitions. But it turns out that such a construction is possible after all:

newtype IP m p i = IP (forall k z. (forall j. p j -> m j k z) -> m i k z)
unIP (IP f) = f

instance Paramonad m => IMonad (IP m) where
    iskip p = IP (\k -> k p)
    iextend f m = IP (unIP m (\p -> unIP (f p) k))

liftP :: Paramonad m => m i j a -> IP m (a := j) i
liftP m = IP (\k -> m `pbind` k . V)

Since pbind requires the index transition to be known statically, it can’t be in iextend. Instead, we use iextend to build up a continuation, and then call pbind in liftP, where the transition is known statically.

Even better, we can translate the higher-order operations needed to handle dynamic transitions into simple dynamic computations:

liftBranch :: Paramonad m =>
    (forall l z. (a -> m j l z) -> (b -> m k l z) -> m i l z)
    -> IP m (a := j :\/ b := k) i
liftBranch branch = IP (\k -> branch (k . L . V) (k . R . V))

So which is better?

So now we’ve seen that Paramonad and IMonad are essentially equally powerful: whereever one can be used, the other can be transformed into it. So is one preferable? I’m not sure. On the one hand, paramonads are a new concept without much theoretical basis at this point, whereas IMonads are just monads in a context we haven’t seen before. On the other hand, (?>=) is hard to use: you need to use GADTs at some level to do anything useful with it, and it’s not always obvious where you need to put type signatures so that GHC can figure out what you’re doing.

Furthermore, instances of Monad are not just monads but strong monads. This strength turns out to be essential for making monads easy to work with; almost all the utility functions in Control.Monad require strength. The obvious definition for a strength for monads over indexed types would probably look like this:

data (p :*: q) i = p i :*: q i

strength :: (p :*: m q) :-> m (p :*: q)

but this can only work if m never involves an index transition. (That is, p starts out having the initial index and ends up having the final index.)

Aside from illustrating the difference between strong and non-strong monads (something I had never appreciated before), this unforunately limits the utility of IMonad. (For example, IMonad cannot be made an instance of a hypothetical IArrow class, because there’s no way to define first.)

McBride gets around this by defining analogues to ap and other functions in the case where the transitions are known statically:

ap :: IMonad m => m ((a -> b) := j) i -> m (a := k) j -> m (b := k) i
m1 `ap` m2 = m1 =>= \f -> m2 =>= \x -> ireturn (f x)

But, as we saw before, this is essentially limiting ourselves to what we can do with Paramonad.

Even with that limitation, I think the ability to handle dynamic transitions makes IMonad more useful than Paramonad. But that leaves the question of whether either of them is useful. Are there any interesting algorithms that operate over any instance of IMonad or Paramonad? Yes, it’s possible to define analogues to mapM or traverse, but they don’t allow for index transitions.

imapM :: IMonad m => (a -> m (b := i) i) -> [a] -> m ([b] := i) i
imapM f [] = ireturn []
imapM f (x:xs) = f x =>= \b -> imapM f xs =>= \bs -> ireturn (b:bs)

Without index transitions, IMonad and Paramonad are no more powerful than Monad. I don’t have an answer here; I think IMonad is interesting and deserves further study, but it’s not yet clear that its advantages outweigh its complexity for practical programming.