Using MonadRef to Implement MonadCont

Question

There is a known problem: we cannot use forall types in the Cont return type .

However, it should be good to have the following definition:

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

and then find the instance that makes sense. In this article, the author claimed that we can implement MonadFix on top of ContT rm by providing m implemented MonadFix and MonadRef . But I think that if we have MonadRef , we can actually implement callCC' above, as shown below:

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

(Unfortunately, I am not familiar with the semantics of shift and reset , so I did not provide them with an implementation)

This implementation seems appropriate to me. Intuitively, when callCC' is callCC' , we are root k , which a function that has its own effect always fails (although we cannot provide a value of arbitrary type b , but we can always provide mzero of type mb and, in accordance with the law, it must effectively stop computing all subsequent effects), and it captures the resulting value as the final result of callCC' .

So my question is:

callCC this implementation work as expected for a perfect callCC ? Can we implement shift and reset with the correct semantics?

In addition to the above, I want to know:

To ensure proper behavior, we need to take some MonadRef property. So, what could the laws of a MonadRef do to make the implementation described above as expected?

UPDATE

It turns out that the naive implementation given above is not good enough. To satisfy the Continuation Current

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

We must configure the implementation to

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

In other words, the original MonadZero not enough, we should be able to combine the mzero value with a normal calculation without canceling the whole calculation.

The above does not answer the question, it is simply adjusted because the original attempt was falsified as a candidate. But for the updated version, the original questions remain questions. Especially, reset and shift should be implemented.

Answer 1

(This is not an answer yet, but only some clues have appeared in my mind. I hope this leads to a real answer, me or someone else.)

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

In the above article, the author introduced the "double calculus", a typed calculus corresponding to classical logic. The last section has a segment:

A dual-on-demand strategy can avoid this inefficiency by rewriting the kotherm with its covalent on its first evaluation.

As stated in Wadler's paper, a call by name evaluates the continuations with impatience (it returns before all the values ​​are evaluated), while by default it evaluates the continuations lazily (it returns only after evaluating all the values).

Now take a look at callCC' above, I think this is an example of a double call, if necessary, as a continuation. The evaluation strategy is to provide a fake "continuation" of the function specified, but caching the state at this stage for the subsequent continuation of the "true" continuation. It’s kind of like creating a continuation cache, and as soon as the calculation is complete, we will restore this continuation. But the estimated value cache is what it implies by request.

In general, I suspect that the state (calculation to the current point in time) is dual to the continuation (future calculation). This will explain several phenomena. If so, it is not surprising that MonadRef (corresponds to the global and polymorphic state) is dual to MoncadCont (corresponds to the global and polymorphic continuations), and therefore they can be used to implement each other.