Why can't there be an instance of MonadFix for the continuation monad?

Well actually, it's not that there can't be a MonadFix instance, just that the library's type is a bit too constrained. If you define ContT over all possible rs, then not only does MonadFix become possible, but all instances up to Monad require nothing of the underlying functor :

newtype ContT m a = ContT { runContT :: forall r. (a -> m r) -> m r } instance Functor (ContT m) where fmap f (ContT k) = ContT (\kb -> k (kb . f)) instance Monad (ContT m) where return a = ContT ($a) join (ContT kk) = ContT (\ka -> kk (\(ContT k) -> k ka)) instance MonadFix m => MonadFix (ContT m) where mfix f = ContT (\ka -> mfixing (\a -> runContT (f a) ka<&>(,a))) where mfixing f = fst <$> mfix (\ ~(_,a) -> f a ) 

Consider the type signature of mfix for the continuation monad.

(a -> ContT r m a) -> ContT r m a -- expand the newtype (a -> (a -> m r) -> m r) -> (a -> m r) -> m r 

Here's the proof that there's no pure inhabitant of this type.

--------------------------------------------- (a -> (a -> m r) -> m r) -> (a -> m r) -> m r introduce f, k f :: a -> (a -> m r) -> m r k :: a -> m r --------------------------- m r apply k f :: a -> (a -> m r) -> m r k :: a -> m r --------------------------- a dead end, backtrack f :: a -> (a -> m r) -> m r k :: a -> m r --------------------------- m r apply f f :: a -> (a -> m r) -> m r f :: a -> (a -> m r) -> m r k :: a -> m r k :: a -> m r --------------------------- --------------------------- a a -> m r dead end reflexivity k 

As you can see the problem is that both f and k expect a value of type a as an input. However, there's no way to conjure a value of type a. Hence, there's no pure inhabitant of mfix for the continuation monad.

Note that you can't define mfix recursively either because mfix f k = mfix ? ? would lead to an infinite regress since there's no base case. And, we can't define mfix f k = f ? ? or mfix f k = k ? because even with recursion there's no way to conjure a value of type a.

But, could we have an impure implementation of mfix for the continuation monad? Consider the following.

import Control.Concurrent.MVar import Control.Monad.Cont import Control.Monad.Fix import System.IO.Unsafe instance MonadFix (ContT r m) where mfix f = ContT $ \k -> unsafePerformIO $ do m <- newEmptyMVar x <- unsafeInterleaveIO (readMVar m) return . runContT (f x) $ \x' -> unsafePerformIO $ do putMVar m x' return (k x') 

The question that arises is how to apply f to x'. Normally, we'd do this using a recursive let expression, i.e. let x' = f x'. However, x' is not the return value of f. Instead, the continuation given to f is applied to x'. To solve this conundrum, we create an empty mutable variable m, lazily read its value x, and apply f to x. It's safe to do so because f must not be strict in its argument. When f eventually calls the continuation given to it, we store the result x' in m and apply the continuation k to x'. Thus, when we finally evaluate x we get the result x'.

The above implementation of mfix for the continuation monad looks a lot like the implementation of mfix for the IO monad.

import Control.Concurrent.MVar import Control.Monad.Fix instance MonadFix IO where mfix f = do m <- newEmptyMVar x <- unsafeInterleaveIO (takeMVar m) x' <- f x putMVar m x' return x' 

Note, that in the implementation of mfix for the continuation monad we used readMVar whereas in the implementation of mfix for the IO monad we used takeMVar. This is because, the continuation given to f can be called multiple times. However, we only want to store the result given to the first callback. Using readMVar instead of takeMVar ensures that the mutable variable remains full. Hence, if the continuation is called more than once then the second callback will block indefinitely on the putMVar operation.

However, only storing the result of the first callback seems kind of arbitrary. So, here's an implementation of mfix for the continuation monad that allows the provided continuation to be called multiple times. I wrote it in JavaScript because I couldn't get it to play nicely with laziness in Haskell.

// mfix :: (Thunk a -> ContT r m a) -> ContT r m a const mfix = f => k => { const ys = []; return (function iteration(n) { let i = 0, x; return f(() => { if (i > n) return x; throw new ReferenceError("x is not defined"); })(y => { const j = i++; if (j === n) { ys[j] = k(x = y); iteration(i); } return ys[j]; }); }(0)); }; const example = triple => k => [ { a: () => 1, b: () => 2, c: () => triple().a() + triple().b() }, { a: () => 2, b: () => triple().c() - triple().a(), c: () => 5 }, { a: () => triple().c() - triple().b(), b: () => 5, c: () => 8 }, ].flatMap(k); const result = mfix(example)(({ a, b, c }) => [{ a: a(), b: b(), c: c() }]); console.log(result);

Here's the equivalent Haskell code, sans the implementation of mfix.

import Control.Monad.Cont import Control.Monad.Fix data Triple = { a :: Int, b :: Int, c :: Int } deriving Show example :: Triple -> ContT r [] Triple example triple = ContT $ \k -> [ Triple 1 2 (a triple + b triple) , Triple 2 (c triple - a triple) 5 , Triple (c triple - b triple) 5 8 ] >>= k result :: [Triple] result = runContT (mfix example) pure main :: IO () main = print result 

Notice that this looks a lot like the list monad.

import Control.Monad.Fix data Triple = { a :: Int, b :: Int, c :: Int } deriving Show example :: Triple -> [Triple] example triple = [ Triple 1 2 (a triple + b triple) , Triple 2 (c triple - a triple) 5 , Triple (c triple - b triple) 5 8 ] result :: [Triple] result = mfix example main :: IO () main = print result 

This makes sense because after all the continuation monad is the mother of all monads. I'll leave the verification of the MonadFix laws of my JavaScript implementation of mfix as an exercise for the reader.