Существует хорошо известная проблема, заключающаяся в том, что мы не можем использовать типы forall в возврате Cont тип.
Однако должно быть нормально иметь следующее определение:
class Monad m => MonadCont' m where
callCC' :: ((a -> forall b. m b) -> m a) -> m a
shift :: (forall r.(a -> m r) -> m r) -> m a
reset :: m a -> m a
а затем найти экземпляр, который имеет смысл. В этой статье автор заявил, что мы можем реализовать MonadFix поверх ContT r m предоставления что m реализовал MonadFix и MonadRef. Но я думаю, что если у нас есть MonadRef, мы можем реализовать callCC' выше, как показано ниже:
--satisfy law: mzero >>= f === mzero
class Monad m => MonadZero m where
mzero :: m a
instance (MonadZero m, MonadRef r m) => MonadCont' m where
callCC' k = do
ref <- newRef Nothing
v <- k (\a -> writeRef ref (Just a) >> mzero)
r <- readRef ref
return $ maybe v id r
shift = ...
reset = ...
(К сожалению, я не знаком с семантикой shift и reset, поэтому я не предоставлял им реализацию)
Эта реализация кажется мне нормальной. Интуитивно понятно, что когда вызывается callCC', мы передаем k, который функция, которая сама по себе всегда терпит неудачу (хотя мы не можем предоставить значение произвольного типа b, но мы всегда можем предоставить mzero типа m b и в соответствии с законом это должен эффективно остановить вычисление всех дальнейших эффектов), и он фиксирует полученное значение как окончательный результат callCC'.
Итак, мой вопрос:
Работает ли эта реализация так, как ожидалось, для идеального callCC? Можем ли мы реализовать shift и reset с правильной семантикой?
В дополнение к вышесказанному, я хочу знать:
Чтобы обеспечить правильное поведение, мы должны принять некоторое свойство MonadRef. Итак, какие законы должны быть MonadRef, чтобы приведенная выше реализация работала так, как ожидалось?
ОБНОВЛЕНИЕ
Оказывается, приведенная выше наивная реализация недостаточно хороша. Чтобы он удовлетворял «Продолжение тока»
callCC $\k -> k m === callCC $ const m === m
Мы должны настроить реализацию на
instance (MonadPlus m, MonadRef r m) => MonadCont' m where
callCC' k = do
ref <- newRef mzero
mplus (k $ \a -> writeRef ref (return a) >> mzero) (join (readRef ref))
Другими словами, исходного MonadZero недостаточно, мы должны иметь возможность комбинировать значение mzero с обычным вычислением без отмены всего вычисления.
Вышеизложенное не дает ответа на вопрос, оно просто скорректировано, так как первоначальная попытка стать кандидатом была сфальсифицирована. Но для обновленной версии первоначальные вопросы остаются вопросами. В частности, reset и shift еще предстоит реализовать.
