使用MonadRef来实现MonadCont [英] Use MonadRef to implement MonadCont

问题描述

我们不能使用<$ c Cont 返回类型中的$ c> forall 类型。

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

  class Monad m => MonadCont'm其中
 callCC'::（（a  - > forall b。m b） - > m a） - > m a 
 shift：（全部（a→m r）→m r）→> m a 
 reset :: m a  - > m a 
  

然后找到一个有意义的实例。在本文中，作者声称我们可以实现 MonadFix 在 ContT rm 之上，假设 m 实现了 MonadFix 和 MonadRef 。但我认为如果我们有一个 MonadRef ，我们实际上可以实现 callCC'，如下所示：

   - 满足law：mzero>> = f === mzero 
 class Monad m => MonadZero m其中
 mzero :: m a 
 
实例（MonadZero m，MonadRef r m）=> MonadCont'm其中
 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 ，但我们总是可以提供<$ c $>类型的 mzero c> mb ，并根据法律它应该有效地阻止所有正在计算的进一步效果），并且捕获接收到的值作为 callCC'


所以我的问题是：



这个实现是否按照理想的 callCC ？我们可以用适当的语义来实现 shift 和 reset 吗？



除了上面的内容，我想知道：为了确保正确的行为，我们必须假设 MonadRef code>。那么为了使上面的实现像预期一样，法律 MonadRef 具有怎样的行为？



UPDATE

事实证明，上面的朴素实现不够好。为了让它满足延续当前的要求

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

我们必须调整执行到

  instance（MonadPlus m，MonadRef rm）=> MonadCont'm其中
 callCC'k = do 
 ref<  -  newRef mzero 
 mplus（k $ \ a  - > writeRef ref（return a）>> mzero）（ join（readRef ref））
  

换句话说，原始的 MonadZero 是不够的，我们必须能够用正常计算结合 mzero 值而不会取消整个计算。

上述内容并没有回答这个问题，只是因为最初的尝试被伪造成候选人而被调整。但对于更新版本，原始问题仍然是问题。特别是 reset 和 shift 仍然有待实施。

解决方案

（这还不是一个答案，但只有一些线索出现在我脑海中，我希望这将导致真实的答案，由我自己或某人）

按价值计算拨打电话是双向拨打电话 - Philip Wadler

在上面的文章中，作者介绍了Dual Calculus，这是一种与经典逻辑相对应的类型演算。在上一节中，有一段说：

与需求调用相对应的策略可以避免这种低效在第一次评估时，用它的价值
重写一个coterm。

正如Wadler的论文中所述，名称评估延续（它在所有值被评估前返回），而按值逐个评估延续（它只在所有值被评估后才返回）。

现在看看上面的 callCC'，我相信这是一个双重调用的例子在继续的一方需要。评估的策略是给给定的函数提供一个虚假的延续，但是缓存此时的状态以在稍后调用真实延续。这在某种程度上类似于对延续进行缓存，所以一旦计算完成，我们就恢复该延续。但是，缓存评估值是按需调用的。

一般而言，我怀疑，状态（计算到当前时间点）是双重的继续（未来计算）。这将解释一些现象。如果这是真的，那么 MonadRef （对应于全局和多态状态）与 MoncadCont （对应于全局和多态继续），因此它们可以用来实现彼此。

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.

解决方案

(This is not yet an answer, but only some clues came up in my mind. I hope this will lead to the real answer, by myself or by someone else.)

Call-by-Value is Dual to Call-by-Name -- Philip Wadler

In the above paper the author introduced the "Dual Calculus", a typed calculus that is corresponding to the classical logic. In the last section, there is a segment says

A strategy dual to call-by-need could avoid this inefficiency by overwriting a coterm with its covalue the first time it is evaluated.

As stated in Wadler's paper, call-by-name evaluating the continuations eagerly (it returns before all values being evaluated) whilst call-by-value evaluating the continuations lazily (it only returns after all values being evaluated).

Now, take a look at the callCC' above, I believe this is an example of the dual of call-by-need in the continuation side. The strategy of the evaluation, is that provide a fake "continuation" to the function given, but cache the state at this point to call the "true" continuation later on. This is somehow like making a cache of the continuation, and so once the computation finishes we restore that continuation. But cache the evaluated value is what it mean by call-by-need.

In general I suspect, state (computation up to the current point of time) is dual to continuation (the future computation). This will explain a few phenomenons. If this is true, it is not a surprise that MonadRef (correspond to a global and polymorphic state) is dual to MoncadCont (correspond to global and polymorphic continuations), and so they can be used to implement each other.

这篇关于使用MonadRef来实现MonadCont的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！