Use MonadRef to implement MonadCont

Question

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.

Unloose

does your update amount to an answer to your question? if so, maybe you could post it as such so the question no longer is considered unanswered? – Hemocyte

Answer 1

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

Unloose