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.)
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
x :: m i j a is a computation that returns a value of type
a but also contains a transition from
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
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.
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
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
data (a := i) j where V :: a -> (a := i) i
Now we can define some more restricted versions of
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
x :: m (a := j) i is a computation that produces a value of type
a and changes the index from
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
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
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
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
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
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
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
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
Cont p i is isomorphic to
ICont Id p i.
A similar generalization is possible for
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)
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
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
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
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
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
Paramonad? Yes, it’s possible to define analogues to
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,
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.