63

There is a well known issue that we cannot use forall types in the Cont return type.

However it should be OK to have the following definition:

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

and then find an instance that makes sense. In this paper the author claimed that we can implement MonadFix on top of ContT r m providing that m implemented MonadFix and MonadRef. But I think if we do have a MonadRef we can actually implement callCC' above like the following:

--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 = ...

(Unfortunately I am not familiar with the semantic of shift and reset so I didn't provide implementations for them)

This implementation seems OK for me. Intuitively, when callCC' being called, we feed k which a function that its own effect is always fail (although we are not able to provide a value of arbitrary type b, but we can always provide mzero of type m b and according to the law it should effectively stop all further effects being computed), and it captures the received value as the final result of callCC'.

So my question is:

Is this implementation works as expected for an ideal callCC? Can we implement shift and reset with proper semantic as well?

In addition to the above, I want to know:

To ensure the proper behaviour we have to assume some property of MonadRef. So what would the laws a MonadRef to have in order to make the above implementation behave as expected?

UPDATE

It turn out that the above naive implementation is not good enough. To make it satisfy "Continuation current"

callCC $\k -> k m === callCC $ const m === m

We have to adjust the implementation to

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

In other words, the original MonadZero is not enough, we have to be able to combind a mzero value with a normal computation without cancelling the whole computation.

The above does not answer the question, it is just adjusted as the original attempt was falsified to be a candidate. But for the updated version, the original questions are still questions. Especially, reset and shift are still up to be implemented.

4

1 回答 1

2

（这还不是答案，但我脑海中只有一些线索。我希望这会导致我自己或其他人的真正答案。）

Call-by-Value 与 Call-by-Name 是双重的——Philip Wadler

在上述论文中，作者介绍了“对偶微积分”，一种对应于经典逻辑的类型化微积分。在最后一节，有一段说

与按需调用双重策略可以通过在第一次评估时用其共值覆盖共项来避免这种低效率。

正如 Wadler 的论文中所述，按名称调用急切地评估延续（它在所有值被评估之前返回），而按值调用则懒惰地评估延续（它只在所有值都被评估之后返回）。

现在，看看callCC'上面的内容，我相信这是延续方面的按需调用对偶的一个例子。评估的策略是为给定的函数提供一个虚假的“延续”，但缓存此时的状态以稍后调用“真实”延续。这有点像对延续进行缓存，因此一旦计算完成，我们就会恢复该延续。但是缓存评估值是按需调用的意思。

一般来说，我怀疑状态（直到当前时间点的计算）与继续（未来的计算）是双重的。这将解释一些现象。MonadRef如果这是真的，那么（对应于全局和多态状态）与（对应于全局和多态延续）是对偶的也就不足为奇了MoncadCont，因此它们可以用来相互实现。

于 2015-07-03T08:00:29.633 回答