为什么不能有延续 monad 的 MonadFix 实例？

Question

我们如何证明连续monad没有MonadFix的有效实例？

Answer 1

实际上，并不是说不能有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 )

Answer 2

考虑连续monad的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类型的值。因此，对于连续monad，不存在mfix的纯居民。

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

但是，对于continuation monad，我们是否可以有一个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'。

CCD_ 38的上述实现方式与CCD_ 40 monad的CCD_ 39的实现方式非常相似。

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'

请注意，在为连续monad实现mfix时，我们使用了readMVar，而在为IO monad实现的mfix中，我们使用takeMVar。这是因为，给f的延拓可以被多次调用。但是，我们只想存储第一次回调的结果。使用readMVar而不是takeMVar可以确保可变变量保持满。因此，如果连续调用不止一次，则第二次回调将无限期地阻止putMVar操作。

然而，只存储第一次回调的结果似乎有点武断。因此，这里有一个用于continuation monad的mfix的实现，它允许多次调用所提供的continuation。我用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

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

这是有道理的，因为在所有的延续之后，monad是所有monad之母。我将把对mfix的JavaScript实现的MonadFix定律的验证留给读者练习。