[Haskell-cafe] Re: Control.Monad.Cont fun

[Thomas Jäger]

Hello Tomasz,

This stuff is very interesting! At first sight, your definition of
getCC seems quite odd, but it can in fact be derived from its
implementation in an untyped language.

On 7/7/05, Tomasz Zielonka <tomasz.zielonka at gmail.com> wrote:
> Some time ago I wanted to return the escape continuation out of the
> callCC block, like this:
> 
>   getCC = callCC (\c -> return c)
We get the error message

test124.hs:8:29:
    Occurs check: cannot construct the infinite type: t = t -> t1
      Expected type: t -> t1
      Inferred type: (t -> t1) -> m b

Haskell doesn't support infinite types, but we can get close enough by
creating a type C m b such that C m b and C m b -> m b become
isomorphic:

newtype C m b = C { runC :: C m b -> m b }

With the help of C we can implement another version of getCC and
rewrite the original example.

getCC1 :: (MonadCont m) => m (C m b) 
getCC1 = callCC $ \k -> return (C k)

test1 :: ContT r IO ()
test1 = do
  jmp <- getCC1
  liftIO $ putStrLn "hello1"
  jmp `runC` jmp -- throw the continuation itself, 
                 -- so we can jump to the same point the next time.
  return ()

We can move the self-application of jmp into getCC to get the same
type signature as your solution, but we still rely on the auxiliary
datatype C.

getCC2 :: MonadCont m => m (m b)
getCC2 = do
  jmp <- callCC $ \k -> return (C k)
  return $ jmp `runC` jmp

In order to move the function (\jmp -> jmp `runC` jmp) into callCC,
the following law, that all instances of MonadCont seem to satisfy, is
very helpful.

f =<< callCC g === callCC (\k -> f =<< g ((=<<) k . f))

In particular (regarding Functor as superclass of Monad), it follows

f `fmap` callCC g === callCC (\k -> f `fmap` g (k . f))

Therefore, getCC2 is equivalent to

getCC3 :: MonadCont m => m (m b)
getCC3 = callCC $ \k -> return (selfApp $ C (k . selfApp)) where 
  selfApp :: C m b -> m b
  selfApp jmp = jmp `runC` jmp

It is easy to get rid of C here arriving exactly at your definition of getCC.

>   getCC :: MonadCont m => m (m a)
>   getCC = callCC (\c -> let x = c x in return x)

>   getCC' :: MonadCont m => a -> m (a, a -> m b)
>   getCC' x0 = callCC (\c -> let f x = c (x, f) in return (x0, f))
For what it's worth, this can be derived in much the same way from the
(not well-typed)

getCC' x = callCC $ \k -> return (k, x)

using the auxillary type

newtype C' m a b = C' { runC' :: (C' m a b, a) -> m b }

> 
> Besides sharing my happiness, I want to ask some questions:
> 
> - is it possible to define a MonadFix instance for Cont / ContT?
It must be possible to define something that looks like a MonadFix
instance, after all you can define generally recursive functions in
languages like scheme and sml which "live in a ContT r IO monad", but
this has all kinds of nasty consequences, iirc.

Levent Erkök's thesis suggests (pp. 66) that there's no implementation
of mfix that satisfies the purity law.
http://www.cse.ogi.edu/PacSoft/projects/rmb/erkok-thesis.pdf

> - do you think it would be a good idea to add them to
>   Control.Monad.Cont?
I think so, because they simplify the use of continuations in an
imperative setting and are probably helpful in understanding
continuations. Letting continuations escape is quite a common pattern
in scheme code, and painful to do in Haskell without your cool trick.
I'd also like to have shift and reset functions there :)


Best wishes,

Thomas