MonadFix instance for interpreter monad transforme

问题:

I have a simplified version of the standard interpreter monad transformer generated by FreeT:

data InteractiveF p r a = Interact p (r -> a)

type Interactive p r = FreeT (InteractiveF p r)

p is the "prompt", and r is the "environment"...one would run this using something like:

runInteractive :: Monad m => (p -> m r) -> Interactive p r m a -> m a
runInteractive prompt iact = do
  ran <- runFreeT iact
  case ran of
    Pure x -> return x
    Free (Interact p f) -> do
      response <- prompt p
      runInteractive prompt (f resp)

instance MonadFix m => MonadFix (FreeT (InteractiveF p r)) m a)
mfix = -- ???

I feel like this type is more or less just a constrained version of StateT...if anything, an Interactive p r IO is I think a constrained version of IO...I think...but... well, in any case, my intuiton says that there should be a good instance.

I tried writing one but I can't really seem to figure out. My closest attempt so far has been:

mfix f = FreeT (mfix (runFreeT . f . breakdown))
  where
    breakdown :: FreeF (InteractiveF p r) a (FreeT (InteractiveF p r) m a) -> a
    breakdown (Pure x) = x
    breakdown (Free (Interact p r)) = -- ...?

I also tried using a version taking advantage of the MonadFix instance of the m, but also no luck --

mfix f = FreeT $ do
  rec ran <- runFreeT (f z)
      z   <- case ran of
               Pure x -> return x
               Free iact -> -- ...
  return -- ...

Anyone know if this is really possible at all, or why it isn't? If it is, what's a good place for me to keep on looking?

---

Alternatively, in my actual application, I don't even really need to use FreeT...I can just use Free; that is, have Interactive be just a monad and not just a monad transformer, and have

runInteractive :: Monad m => (p -> m r) -> Interactive p r a -> m a
runInteractive _ (Pure x) = return x
runInteractive prompt (Free (Interact p f) = do
    response <- prompt p
    runInteractive prompt (f response)

If something is possible for this case and not for the general FreeT case, I would also be happy :)

回答1:

Imagine you already had an interpreter for Interactive.

interpret :: FreeT (InteractiveF p r) m a -> m a
interpret = undefined

It would be trivial to write a MonadFix instance:

instance MonadFix m => MonadFix (FreeT (InteractiveF p r) m) where
    mfix = lift . mfix . (interpret .)

We can directly capture this idea of "knowing the interpeter" without committing to an interpreter ahead of time.

{-# LANGUAGE RankNTypes #-}

data UnFreeT t m a = UnFree {runUnFreeT :: (forall x. t m x -> m x) -> t m a}
--   given an interpreter from `t m` to `m` ^                          |
--                                  we have a value in `t m` of type a ^

UnFreeT is just a ReaderT that reads the interpreter.

If t is a monad transformer, UnFreeT t is also a monad transformer. We can easily build an UnFreeT from a computation that doesn't require knowing the interpreter simply by ignoring the interpeter.

unfree :: t m a -> UnFreeT t m a
--unfree = UnFree . const
unfree x = UnFree $ \_ -> x

instance (MonadTrans t) => MonadTrans (UnFreeT t) where
    lift = unfree . lift

If t is a monad transormer, m is a Monad, and t m is also a Monad, then UnFree t m is a Monad. Given an interpreter we can bind together two computations that require the interpeter.

{-# LANGUAGE FlexibleContexts #-}

refree :: (forall x. t m x -> m x) -> UnFreeT t m a -> t m a
-- refree = flip runUnFreeT
refree interpreter x = runUnFreeT x interpreter

instance (MonadTrans t, Monad m, Monad (t m)) => Monad (UnFreeT t m) where
    return = lift . return
    x >>= k = UnFree $ \interpreter -> runUnFreeT x interpreter >>= refree interpreter . k

Finally, given the interpreter, we can fix computations as long as the underlying monad has a MonadFix instance.

instance (MonadTrans t, MonadFix m, Monad (t m)) => MonadFix (UnFreeT t m) where
    mfix f = UnFree $ \interpreter -> lift . mfix $ interpreter . refree interpreter . f

We can actually do anything the underlying monad can do, once we have the interpreter. This is because, once we have an interpreter :: forall x. t m x -> m x we can do all of the following. We can go from m x through t m x all the way up to UnFreeT t m x and back down again.

                      forall x.
lift               ::           m x ->         t m x
unfree             ::         t m x -> UnFreeT t m x
refree interpreter :: UnFreeT t m x ->         t m x
interpreter        ::         t m x ->           m x

Usage

For your Interactive, you'd wrap the FreeT in UnFreeT.

type Interactive p r = UnFreeT (FreeT (InteractiveF p r))

Your interpreters would still be written to produce a FreeT (InteractiveF p r) m a -> m a. To interpret the new Interactive p r m a all the way to an m a you'd use

interpreter . refree interpreter

The UnFreeT no longer "frees the interpreter as much as possible". The interpreter can no longer make arbitrary decisions about what to do wherever it wants. The computation in UnFreeT can beg for an interpreter. When the computation begs for and uses an interpreter, the same interpreter will be used to interpret that portion of the program as was used to start interpreting the program.

回答2:

It is not possible to write a MonadFix m => MonadFix (Interactive p r) instance.

Your InteractiveF is the base functor of the well studied Moore machines. A Moore machine provides an output, in your case the prompt, then determines the next thing to do based on an input, in your case the environment. A Moore machine always outputs first.

data MooreF a b next = MooreF b (a -> next)
    deriving (Functor)

If we follow C. A. McCann's argument about writing MonadFix instances for Free but constrain ourselves to the specific case of Free (MooreF a b), we will eventually determine that if there's a MonadFix instance for Free (MooreF a b) then there must exist a function

mooreFfix :: (next -> MooreF a b next) -> MooreF a b next

To write this function, we must construct a MooreF b (f :: a -> next). We don't have any bs to output. It's conceivable that we could get a b if we already had the next a, but a Moore machine always outputs first.

Like the let in State

You can write something close to mooreFfix if you are reading just one a ahead.

almostMooreFfix :: (next -> MooreF a b next) -> a -> MooreF a b next
almostMooreFfix f a = let (MooreF b g) = f (g a)
                      in (MooreF b g)

It then becomes imperative that f be able to determine g independently of the argument next. All of the possible fs to use are of the form f next = MooreF (f' next) g' where f' and g' are some other functions.

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = let (MooreF b g) = f (g a)
                          in (MooreF b g)
                          where
                              f next = MooreF (f' next) g'

With some equational reasoning we can replace f on the right side of the let

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = let (MooreF b g) = MooreF (f' (g a)) g'
                          in (MooreF b g)

We bind g to g'.

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = let (MooreF b _) = MooreF (f' (g' a)) g'
                          in (MooreF b g')

When we bind b to f' (g' a) the let becomes unnecessary and the function has no recursive knot.

almostMooreFFix :: (next -> b) -> (a -> next) -> a -> MooreF a b next
almostMooreFFix f' g' a = MooreF (f' (g' a)) g'

All of the almostMooreFFixes that aren't undefined don't even need a let.