[Haskell-cafe] Control.Monad.Cont fun

[Andrew Pimlott]

On Thu, Jul 07, 2005 at 07:08:23PM +0200, Tomasz Zielonka wrote:
> Hello!
> 
> Some time ago I wanted to return the escape continuation out of the
> callCC block, like this:
> 
>   getCC = callCC (\c -> return c)
> 
> But of course this wouldn't compile.
> 
> I thought that it would be useful to be able to keep the current
> continuation and resume it later, like you can in do in scheme. Well,
> it was easy to do this in Haskell in the (ContT r IO) monad, by using an
> IORef. But I wasn't able to solve this for all MonadCont monads.
> 
> After more then year of on-and-off trials, I've finally managed to do
> this! ;-)
> 
>   import Control.Monad.Cont
> 
>   getCC :: MonadCont m => m (m a)
>   getCC = callCC (\c -> let x = c x in return x)

I was inspired by this message, and thought I could simply this further
as

    getCC = callCC (\c -> let x = c x in x)

After all, c can give us a MonadCont with any result type.  The first
problem is that callCC is not polymorphic enough, but that is easily
fixed[1] (concerning myself just with Cont):

    ccc :: ((a -> (forall b. Cont r b)) -> Cont r a) -> Cont r a
    ccc f = Cont (\k -> runCont (f (\x -> Cont (\_ -> k x))) k)

ccc is just callCC with a more polymorphic type.  But still, try as I
might, I could not get getCC to typecheck, no matter what type
annotations I used.  This works:

    getCC' :: Cont r (Cont r a)
    getCC' = ccc (\c -> let x = c x in c x)

But eg

    getCC :: Cont r (Cont r a)
    getCC = ccc (\(c :: Cont r a -> (forall b. Cont r b)) ->
                    let x :: forall b. Cont r b = c x in x)

gives

    Couldn't match `forall b. Cont r a -> Cont r b'
           against `forall b. Cont r a -> Cont r b'
    In a lambda abstraction:
        \ (c :: Cont r a -> (forall b. Cont r b))
            -> let x :: forall b. Cont r b = c x in x
    In the first argument of `ccc', namely
        `(\ (c :: Cont r a -> (forall b. Cont r b))
              -> let x :: forall b. Cont r b = ... in x)'
    In the definition of `getCC'':
        getCC' = ccc (\ (c :: Cont r a -> (forall b. Cont r b))
                          -> let x :: forall b. Cont r b = ... in x)

for which I have no riposte.  Is this a bug?  Is there any way to type
this expression?  (I am using ghc 6.4.)

Andrew

[1] http://www.haskell.org/hawiki/ContinuationsDoneRight