MonadFix instance for interpreter monad transformer generated by FreeT?

Question

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 :)

Answer 1

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.