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

Question

How can we prove that the continuation monad has no valid instance of MonadFix?

Granary

Answer 1

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 )

Peyton

It looks like your type is actually the more constrained one. Are there real situations where forcing the argument to ContT to be polymorphic would block useful implementations? If not, this is probably just a matter of history—ContT has been around for a long time, quite possibly before rank 2 types were a well-accepted part of Haskell. – Ballon

Polymorphic argument ContT is also known as Codensity. It lacks the ability to define callCC. – Enuresis

This answer explains why your forall r. (a -> m r) -> m r ContT can't have callCC. https://mcmap.net/q/323274/-how-to-make-callcc-more-dynamic – Poesy

Well, it's true that I can't define the Control.Monad.Cont.callCC with this definition of Codensity (thank you, Ørjan, for teaching me a new word :-) ), but if we use a typeclass that looks like Scheme's continuations, the instance almost writes itself : class MonadCont m where callCC :: (forall b. (a -> m b) -> m b) -> m a. We can use this instance in a way more consistent with the idea that we do not directly get a value in our continuation, but rather the rest of the computation to run with the value that we generate, of which we do not yet know the type (hence the forall). – Peyton

Answer 2

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.

Cobblestone

That proof is not convincing in this particular setting because it only considers implementation without recursion, whereas recursion is the very point of MonadFix. – Thumbsdown

This MonadFix instance for ContT breaks referential transparency: the value of x depends on whether or not the continuation is called, which depends on evaluation order, even if it is applied at most once. – Thumbsdown

On the other hand, if you embrace the unsafety, it could be a fun way to tie knots. – Thumbsdown

@Li-yaoXia 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. – Cobblestone

@Li-yaoXia True. It does break referential transparency. – Cobblestone