How does the higher-order encoding of indexed monads work?

Question

The usual way to define an indexed monad a la Atkey is:

class IxMonad m where
  ireturn :: a -> m i i a
  ibind   :: m i j a -> (a -> m j k b) -> m i k b

Another approach is found in the work of McBride (also discussed by him here):

type f :-> g = forall i. f i -> g i

class MonadIx (m :: (state -> *) -> (state -> *)) where
  returnIx    :: f :-> m f
  flipBindIx  :: (f :-> m g) -> (m f :-> m g)

The type of flipBindIx is isomorphic to bindIx :: forall i. m f i -> (forall j. f j -> m g j) -> m g i. Whereas normal Haskell monads characterize m :: * -> * (and the 'normal' indexed monads characterize m :: state -> state -> * -> *), MonadIx characterizes monads m :: (state -> *) -> state -> *. That's why I'm calling the latter 'higher-order' (but if there's a better name, let me know).

While this makes a certain amount of sense, and I can see certain structural similarities between the two encodings, I am having difficulty with a few things. Here are a few questions that seem related:

• Most basically, I just don't understand how to use MonadIx to write a simple indexed state monad -- the one that in IxMonad looks just like the regular state monad, with more general types.

• Relatedly, in the previously linked SO question, Kmett discusses a way to 'recover the power of' IxMonad from MonadIx. The technique isn't completely demonstrated, however (and I can't get the associated code to compile, anymore).

• MonadIx is stronger than IxMonad. This suggests that there should be a mapping from any IxMonad m => m i o a to some MonadIx m => m f (or is is m f i?), but not the reverse, right? What is that mapping?

• Finally, parametricity abounds in the definition of MonadIx. But IxMonad actions can freely make demands about the shape of the incoming state, as in m :: IxMonad m (a, i) i a. How do these sorts of actions look in MonadIx?

Answer 1

I just don't understand how to use MonadIx to write a simple indexed state monad -- the one that in IxMonad looks just like the regular state monad, with more general types.

McBride-style indexed monads are about quantifying runtime uncertainty. If a normal monad m a models a computation which returns an a, an indexed monad m a i models a computation which starts in state* i and returns an a j for some unknown output state j. The only thing you can say about j is that it satisfies the predicate a.

^{*I'm using the words "state", "input" and "output" somewhat loosely here.}

That's why McBride's bind has a higher-rank type:

mcBind :: m a i -> (forall j. a j -> m b j) -> m b i

The continuation forall j. a j -> m b j must be agnostic about j, beyond what it can learn at runtime from examining the a j. (For nondeterministic monads which return multiple as, the j might be different for each of them.)

McBride's running example from the Outrageous Fortune paper is about a file API which may successfully return an open file or may fail (if the file doesn't exist). There's another example in the Hasochism paper about a tiling window manager — you have a 2D box which may be made up of smaller boxes placed next to each other. You can drill down into the individual boxes and replace them with other boxes. You don't know how big each individual box is statically, but when replacing a box with another they must have equal size.

So the indexed state monad (State i j a), which takes a known input state i and produces a known output state j, is simply not a good fit for a McBride-style indexed monad. The type of mcBind is wrong, since it discards the information about the output state.

[T]here should be a mapping from any IxMonad [to] MonadIx, but not the reverse, right? What is that mapping?

It's the other way around. McBride's indexed monads are more powerful than Atkey's ones — if you have an m :: (i -> *) -> i -> * with an instance of MonadIx you can always come up with a corresponding n :: i -> i -> * -> * with an instance of IxMonad. (Surprisingly the reverse is also true.) This is detailed in Section 5 of McBride's paper ("Angels, Demons and Bob"). Briefly:

-- McBride wittily pronounces this type "at key"
data (a := i) j where
    V :: a -> (a := i) i

newtype Atkey m i j a = Atkey { getAtkey :: m (a := j) i }

instance MonadIx m => IxMonad (Atkey m) where
    ireturn a = Atkey (returnIx (V a))
    ibind (Atkey m) f = Atkey $ m `bindIx` (\(V a) -> getAtkey (f a))