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 `IMonad`

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