Почему не может быть экземпляра MonadFix для продолжения монады?

Question

Как мы можем доказать, что у монады продолжения нет действительного экземпляра MonadFix?

Answer 1

Ну, на самом деле это не значит, что не может быть MonadFix Например, тип библиотеки слишком ограничен. Если вы определите ContT по всем возможным rс, то не только делает 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

Рассмотрим сигнатуру типа 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 поскольку монада продолжения очень похожа на реализацию mfix для IO монада.

       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 тогда как в реализации mfix для IO монада, которую мы использовали takeMVar. Это потому, что продолжение дано fможно вызывать несколько раз. Однако мы хотим сохранить только результат, полученный при первом обратном вызове. С помощью readMVar вместо takeMVarгарантирует, что изменяемая переменная останется заполненной. Следовательно, если продолжение вызывается более одного раза, второй обратный вызов будет заблокирован на неопределенное время на 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

Обратите внимание, что это очень похоже на монаду списка.

       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

Это имеет смысл, потому что в конце концов монада продолжения является матерью всех монад. Оставлю проверку MonadFix законы моей реализации JavaScript mfix как упражнение для читателя.