Is it possible to implement MonadFix for `Free`?

Question

http://hackage.haskell.org/package/free in Control.Monad.Free.Free allows one to get access to the "free monad" for any given Functor. It does not, however, have a MonadFix instance. Is this because such an instance cannot be written, or was it just left out?

If such an instance cannot be written, why not?

Geodesic

Answer 1

Consider the description of what mfix does:

The fixed point of a monadic computation. mfix f executes the action f only once, with the eventual output fed back as the input.

The word "executes", in the context of Free, means creating layers of the Functor. Thus, "only once" means that in the result of evaluating mfix f, the values held in Pure constructors must fully determine how many layers of the functor are created.

Now, say we have a specific function once that we know will always only create a single Free constructor, plus however many Pure constructors are needed to hold the leaf values. The output of 'once', then, will be only values of type Free f a that are isomorphic to some value of type f a. With this knowledge, we can un-Free the output of once safely, to get a value of type f a.

Now, note that because mfix is required to "execute the action only once", the result of mfix once should, for a conforming instance, contain no additional monadic structure than once creates in a single application. Thus we can deduce that the value obtained from mfix once must also be isomorphic to a value of type f a.

Given any function with type a -> f a for some Functor f, we can wrap the result with a single Free and get a function of type a -> Free f a which satisfies the description of once above, and we've already established that we can unwrap the result of mfix once to get a value of type f a back.

Therefore, a conforming instance (Functor f) => MonadFix (Free f) would imply being able to write, via the wrapping and unwrapping described above, a function ffix :: (Functor f) => (a -> f a) -> f a that would work for all instances of Functor.

That's obviously not a proof that you can't write such an instance... but if it were possible, MonadFix would be completely superfluous, because you could just as easily write ffix directly. (And I suppose reimplement it as mfix with a Monad constraint, using liftM. Ugh.)

Phytophagous

So far I've found that if I can implement retractFunctor :: f a -> a for a given f, then I can implement mfix f = fix (f . iter retractFunctor). I'm not sure if this is the right approach. – Geodesic

@singpolyma: My initial thought was that it should at least be possible to write the instance (Functor m, MonadFix m) => MonadFix (Free m). But I couldn't figure out how to do so correctly. – Phytophagous

This result also makes sense because "free" means that it's supposed to give you a monad and nothing more. But MonadFix is not part of Monad and, indeed, if Monad implied it then it would be superfluous. Could you make a "free MonadFix" by adding additional structure to Free? (My naive attempt was brought up short when it came to writing fmap for the Fix (a -> Free f a) constructor...) – Colloid

@illissius: Yeah, you probably won't get very far having the type parameter in contravariant position... I'd have to think about it, I was more concerned with figuring out what extra structure on f would allow mfix, not using something other than Free. – Phytophagous

@illissius, you could make a free monadfix by adding to Free the constructor forall s. Fix (s -> Free f (s,a)). It would not strictly satisfy the laws; however, that can be patched up by requiring properties for something to be a valid consumer (some formal variant of "it can make no important decisions based on seeing a Fix constructor"; e.g. one of them might be f (Fix (\s -> Pure (s,x)) = f (Pure x)). – Zuniga

Maybe if you take a functor from the category of monads with mfixes, such the monad homomorphisms have some sort of respect of the mfixes, to the category of functors, forgetfully, you could get some sort of "left adjunct" thingy. – Middling

Answer 2

Well, inspired by the MonadFix instance for Maybe, I tried this one (using the following definitions of Free):

data Free f a
    = Pure a
    | Impure (f (Free f a))

instance (Functor f) => Monad (Free f) where
    return = Pure
    Pure x >>= f = f x
    Impure x >>= f = Impure (fmap (>>= f) x)

instance (Functor f) => MonadFix (Free f) where
    mfix f = let Pure x = f x in Pure x

The laws are:

• Purity: mfix (return . h) = return (fix h)
• Left shrinking: mfix (\x -> a >>= \y -> f x y) = a >>= \y -> mfix (\x -> f x y)
• Sliding: mfix (liftM h . f) = liftM h (mfix (f . h)), for strict h
• Nesting: mfix (\x -> mfix (f x)) = mfix (\x -> f x x)

Purity is easy to prove -- but I came across a problem when trying to prove left shrinking:

mfix (\x -> a >>= \y -> f x y)
= let Pure x = (\x -> a >>= \y -> f x y) x in Pure x
= let Pure x = a >>= \y -> f x y in Pure x
-- case a = Pure z
  = let Pure x = Pure z >>= \y -> f x y in Pure x
  = let Pure x = f x z in Pure x
  = let Pure x = (\x -> f x z) x in Pure x
  = mfix (\x -> f x z)
  = Pure z >>= \y -> mfix (\x -> f x y)
-- case a = Impure t
  = let Pure x = Impure t >>= \y -> f x y in Pure x
  = let Pure x = Impure (fmap (>>= \y -> f x y) t) in Pure x
  = Pure _|_

but

  Impure t >>= \y -> mfix (\x -> f x y)
  = Impure (fmap (>>= \y -> mfix (\x -> f x y)) t)
  /= Pure _|_

So, at the very least, if the Pure and Impure constructors are distinguishable, then my implementation of mfix does not satisfy the laws. I can't think of any other implementation, but that does not mean it does not exist. Sorry I couldn't illuminate further.

Zuniga

I'm having a thought -- what if distinguishing Pure and Impure is not something you're supposed to be able to do; i.e. it feels like, categorically speaking, Free Identity should be isomorphic to Identity. Category-privy, am I on base? – Zuniga

Answer 3

No, it cannot be written in general, because not every Monad is an instance of MonadFix. Every Monad can be implemented using the FreeMonad underneath. If you could implement the MonadFix for Free, then you would be able to derive MonadFix from any Monad, which is not possible. But of course, you can define a FreeFix for the MonadFix class.

I think it might look somehow like this, but this is just a 3rd guess (still not tested):

data FreeFix m a = FreeFix { runFreeFix :: (forall r. (r -> m r) -> m r) -> m a }

instance (Monad m) => Monad (FreeFix m) where
    return a = FreeFix $ \_-> do
        return a
    f >>= g = FreeFix $ \mfx -> do
        x <- runFreeFix f mfx
        runFreeFix (g x) mfx

instance (Monad m) => MonadFix (FreeFix m) where
    mfix f = FreeFix $ \mfx -> do
        mfx (\r->runFreeFix (f r) mfx)

The idea is that m is a Monad that lacks an implementation for mfix; so mfix needs to be a parameter when FreeFix will be reduced.

Fistula

FreeFix m is not a functor. But you can make it one using the technique of Arrow's loop combinator: | forall r. Fix (r -> FreeFix m (r,a)). – Zuniga

@luqui: somehow i got this recursion scheme from your suggestion, don't know how. – Fistula