Ear*_*ine 63 continuations haskell delimited-continuations
有一个众所周知的问题是我们不能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
Run Code Online (Sandbox Code Playgroud)
然后找一个有意义的实例.在本文中,作者声称我们可以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 = ...
Run Code Online (Sandbox Code Playgroud)
(不幸的是我不熟悉的语义shift和reset,所以我没有为他们提供实现)
这个实现对我来说似乎没问题.直觉上,当callCC'被调用时,我们提供k一个它自己的效果总是失败的函数(虽然我们不能提供任意类型的值b,但我们总是可以提供mzero类型,m b并且根据法律它应该有效地停止所有正在计算的效果),它捕获接收的值作为最终结果callCC'.
所以我的问题是:
这种实现是否符合理想的预期效果callCC?我们可以实现shift并reset使用适当的语义吗?
除了上述内容,我想知道:
为了确保正确的行为,我们必须承担一些属性MonadRef.那么MonadRef,为了使上述实现符合预期,法律a 将会有什么作用?
UPDATE
事实证明,上述天真的实施还不够好.使其满足"延续电流"
callCC $\k -> k m === callCC $ const m === m
Run Code Online (Sandbox Code Playgroud)
我们必须调整实施
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))
Run Code Online (Sandbox Code Playgroud)
换句话说,原始MonadZero是不够的,我们必须能够在mzero不取消整个计算的情况下将值与正常计算组合在一起.
以上内容并没有回答这个问题,只是因为最初的尝试被伪造为候选人而进行了调整.但对于更新版本,原始问题仍然是问题.特别是,reset和shift仍然高达执行.
(这还不是答案,但我脑海中只出现了一些线索。我希望这将导致我自己或其他人真正的答案。)
按值呼叫与按名称呼叫是双重的-- Philip Wadler
在上面的论文中,作者介绍了“对偶演算”,一种与经典逻辑相对应的类型演算。在最后一节中,有一段说
与按需调用双重的策略可以通过在第一次评估时用其协值覆盖一个协项来避免这种低效率。
正如 Wadler 的论文中所述,按名称调用急切地评估延续(它在评估所有值之前返回),而按值调用延迟评估延续(它仅在评估所有值之后返回)。
现在,看看callCC'上面的内容,我相信这是延续端按需调用的双重示例。评估的策略是为给定的函数提供一个假的“延续”,但缓存此时的状态以便稍后调用“真实”的延续。这在某种程度上类似于对延续进行缓存,因此一旦计算完成,我们就恢复该延续。但缓存评估值就是按需调用的意思。
一般来说,我怀疑状态(截至当前时间点的计算)与延续(未来的计算)是对偶的。这将解释一些现象。MonadRef如果这是真的,那么(对应于全局和多态状态)是对偶的(对应于全局和多态延续)也就不足为奇了MoncadCont,因此它们可以用来相互实现。