使用MonadRef来实现MonadCont

有一个众所周知的问题, 我们不能使用foralltypes中的所有types 。

但是应该可以有以下定义:

 class Monad m => MonadCont' m where callCC' :: ((a -> forall b. mb) -> ma) -> ma shift :: (forall r.(a -> mr) -> mr) -> ma reset :: ma -> ma 

然后find一个有意义的实例。 在本文中 ,作者声称我们可以在MonadFix上面实现MonadFix并提供m实现的MonadFixMonadRef 。 但是我想如果我们有一个MonadRef我们实际上可以实现callCC'

 --satisfy law: mzero >>= f === mzero class Monad m => MonadZero m where mzero :: ma instance (MonadZero m, MonadRef rm) => 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 = ... 

(不幸的是我不熟悉shiftreset的语义,所以我没有提供它们的实现)

这个实现对我来说似乎没问题。 直观地说,当callCC'被调用的时候,我们给k提供一个自己的效果总是失败的函数(虽然我们不能提供任意types的值b ,但是我们总是可以提供mbtypes的mzero ,并且依照定律它应该有效地阻止所有进一步的影响被计算),并且捕获接收到的值作为callCC'的最终结果。

所以我的问题是:

这个实现是否可以像理想的callCC ? 我们是否可以用适当的语义来实现shiftreset

除上述之外,我想知道:

为了确保正确的行为,我们必须假设MonadRef一些属性。 那么MonadRef为了使上面的实现具有如预期的那样的法律会有什么样的performance呢?

UPDATE

事实certificate,上述的天真实施不够好。 为了让它满足“持续的潮stream”

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

我们必须调整执行

 instance (MonadPlus m, MonadRef rm) => MonadCont' m where callCC' k = do ref <- newRef mzero mplus (k $ \a -> writeRef ref (return a) >> mzero) (join (readRef ref)) 

换句话说,原来的MonadZero是不够的,我们必须能够用一个正常的计算结合一个mzero值,而不需要取消整个计算。

以上并不回答这个问题,只是在原来的尝试被伪造成候选人时才进行调整。 但对于更新版本,原来的问题仍然是问题。 尤其是resetshift还有待落实。

(这还不是一个答案,但是只有一些线索出现在我的脑海里,希望这能够让我自己或者其他人得到真正的答案。)

按价值拨打电话是名副其实的呼叫 – Philip Wadler

在上面的论文中,作者介绍了“二元微积分”,这是一种与经典逻辑相对应的types微积分。 在最后一节中,有一段说

与需求呼叫相对应的策略可以通过在第一次评估时用其等价值重写一个等价值来避免这种低效率。

正如瓦德勒的论文所述,按名称评估延续(在所有值被评估前返回),而按值逐一评估延续(它只在所有值被评估后才返回)。

现在看看上面的callCC' ,我相信这就是延续方面call-by-need的一个例子。 评估的策略是给给定的函数提供一个假的“延续”,但是caching此时的状态,以后再调用“真正的”延续。 这有点像继续caching,所以一旦计算完成,我们恢复这个延续。 但是caching评估值是按需调用的。

一般而言,我怀疑,状态(到当前时间点的计算)对于延续(未来计算)是双重的。 这将解释一些现象。 如果这是真的,那么MonadRef (对应于全局和多态的状态)与MoncadCont是对MoncadCont (对应于全局和多态的延续)并不意外,所以它们可以用来实现彼此。

Interesting Posts