为什么连续单子不能有 MonadFix 的实例？

Question

我们如何证明the continuation monad 没有MonadFix 的有效实例？

Answer 1

考虑mfix 的类型签名作为延续单子。

(a -> ContT r m a) -> ContT r m a

-- expand the newtype

(a -> (a -> m r) -> m r) -> (a -> m r) -> m r

这是不存在这种类型的纯粹居民的证据。

---------------------------------------------
(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

如您所见，问题在于f 和k 都期望a 类型的值作为输入。但是，没有办法变出a 类型的值。因此，对于延续单子，mfix 没有纯粹的居民。​​

请注意，您也不能递归地定义mfix，因为mfix f k = mfix ? ? 会导致无限回归，因为没有基本情况。而且，我们无法定义 mfix f k = f ? ? 或 mfix f k = k ?，因为即使使用递归，也无法生成 a 类型的值。

但是，对于延续单子，我们可以有一个不纯的mfix 实现吗？请考虑以下内容。

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

出现的问题是如何将f 应用于x'。通常，我们会使用递归的 let 表达式，即let x' = f x'。但是，x' 不是f 的返回值。相反，给予f 的延续将应用于x'。为了解决这个难题，我们创建了一个空的可变变量m，懒惰地读取它的值x，并将f 应用到x。这样做是安全的，因为f 在其论点中不得严格。当f 最终调用给它的延续时，我们将结果x' 存储在m 中并将延续k 应用于x'。因此，当我们最终评估 x 时，我们会得到结果 x'。

上面的mfix 的延续monad 的实现看起来很像mfix 的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'

注意，在为延续单子实现mfix 时，我们使用readMVar，而在IO 单子的mfix 实现中，我们使用takeMVar。这是因为，可以多次调用f 的延续。但是，我们只想存储给第一个回调的结果。使用 readMVar 而不是 takeMVar 可确保可变变量保持完整。因此，如果不止一次调用 continuation，那么第二个回调将无限期地阻塞 putMVar 操作。

但是，只存储第一个回调的结果似乎有点随意。所以，这是一个mfix 的实现，用于允许多次调用提供的延续单子的延续单子。我用 JavaScript 编写它是因为我无法让它很好地适应 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);

这是等效的 Haskell 代码，没有 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

请注意，这看起来很像 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

这是有道理的，因为毕竟延续单子是the mother of all monads。我将验证我的 JavaScript 实现 mfix 的 MonadFix 定律作为练习留给读者。

Answer 2

实际上，并不是不能有MonadFix 实例，只是库的类型有点受限制。如果你在所有可能的rs 上定义ContT，那么不仅MonadFix 成为可能，而且直到Monad 的所有实例都不需要底层函子：

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 )