[Haskell-cafe] Re: ANNOUNCE: GotoT-transformers version 1.0

[oleg at okmij.org]

Let us look at GoTo from several angles: (un)delimited continuations,
exceptions and trampolines.

Gregory Crosswhite wrote regarding the definition
	goto (ContT m) = ContT $ \_ -> m return

> *HOWEVER*, if we replace main with
>
>      main = runContT myComp (const $ putStrLn "I can't wait to print
> this string!")
>
> Then the program will be eternally disappointed because it will never
> actually get to print that string at the end [if goto had been used]
>
> it just seems to me like at that point the spirit of the
> continuation monad is being violated since the final continuation is
> never actually called.  That isn't necessarily a big deal, but it is the
> kind of behavior that could bite someone if they weren't aware or forgot
> about it.

Let us start by looking at the problem from the point of view of
undelimited continuations. Although that is not my preferred one, it
could be instructive. An undelimited continuation -- the kind that is
typically associated with call/cc -- has no ``final continuation'' to
run at the end. There is no end. The value produced by the undelimited
continuation can never be used by the program itself, because by the
time that value is produced the program shall be dead. It may help to
think of the return value of an undelimited continuation as the value
produced when a computer crashes or the universe ends.

Therefore the type ContT from mtl or MonadLib is not a good model of
undelimited continuations. Better is the following

> data Falsum                             -- it doesn't exist
>
> type K m a = a -> m Falsum              -- NOT a, or the continuation from a
>
> newtype ContT m a = ContT{unC:: K m a -> m Falsum} -- NOT NOT a
>
>
> instance Monad m => Monad (ContT m) where
>     return x = ContT $ \k -> k x
>     m >>= f  = ContT $ \k -> unC m (\v -> unC (f v) k)
>
> instance (Monad m, MonadIO m) => MonadIO (ContT m) where
>     liftIO m = ContT $ \k -> liftIO m >>= k
>
> callCC :: (K m a -> ContT m a) -> ContT m a
> callCC f = ContT (\k -> unC (f k) k)

Given such ContT, the original goto expression would not type:

  goto :: (Monad m) => ContT m () -> ContT m a
  goto (ContT m) = ContT $ \_ -> m return

    Couldn't match expected type `()' against inferred type `Falsum'

If we drop the type annotation, the goto will type, but the argument
computation will be assigned the type ContT m Falsum. There can be no
non-divergent computation with that type.

That typing failure points to the problem with the definition: the
argument of goto was a ContT computation that expects a
continuation. We supplied `return' -- assuming that was the `initial,
or system' continuation. That is, we assumed that the corresponding
runContT indeed supplied `return' as the initial continuation. If
runContT supplied something else, we run into inconsistency. 

Thus the correct definition of goto, in the current approach, instead
of guessing the continuation to abort it, should ask the user. We
obtain the following definition

> goto :: Monad m => K m () -> ContT m () -> ContT m a
> goto k (ContT m) = ContT (\_ -> m k)

We need a way to obtain the continuation to pass to goto. That's where
callCC comes in handy:

> myComp :: ContT IO ()
> myComp = callCC $ \k0 -> do
>      input <- liftIO $ putStrLn "Print something (y/n)?" >> getLine
>      unless ("y" `isPrefixOf` input) $ goto k0 exit
>      liftIO $ putStrLn "Something."
>
>      input <- liftIO $ putStrLn "Print more (y/n)?" >> getLine
>      unless ("y" `isPrefixOf` input) $ goto k0 exit
>      liftIO $ putStrLn "More."
>
>      where
>        exit = liftIO $ putStrLn "Ok, I'm exiting."

A reader must have been wondering since five paragraphs ago about
running ContT computations. Ideally, there should be no runContT -- as
there is no runIO. Since we can't change the behavior of `main' or add a
similarly distinguished `mainCont', we have to find a continuation to
supply to our ContT computation -- the continuation from the present
state till the end of the universe. That seems
problematic. Fortunately, cheating is always an option:

> data FinalExit = FinalExit deriving (Show, Typeable)
> instance Exception FinalExit
>
> main :: IO ()
> main = do
>   handle (\FinalExit -> return ()) 
>          (unC myComp (\() -> putStrLn "At the end" >> throw FinalExit) >> 
>           error "unreachable")

The string "At the end" is printed at every end, caused by goto or the
normal termination.


Although the program type-checks and runs with the expected behavior,
it seems quite contrived. Our goto only skips a prefix of the current
continuation, from the current point to some definite point in
the program, marked by `handle' or runContT, etc. We don't make any 
essential use of undelimited continuations. In fact, I am yet to see
any practical use for undelimited continuations. Delimited
continuations are much more useful. The monad ContT of mtl or MonadLib
is the monad for simple delimited continuations; runContT is the
delimiter, and (\m -> lift $ runContT m return) is the reset.

Our example makes a special use of delimited continuations: we capture
the continuation from the current point till the main point, and throw
it away. That pattern is called abort, and it undelies exceptions. We
immediately obtain the following simplified implementation:

> data GoTo = GoTo deriving (Show, Typeable)
> instance Exception GoTo
>
> goto :: IO () -> IO a
> goto m = m >> throw GoTo
>
> myComp :: IO ()
> myComp = do
>      input <- putStrLn "Print something (y/n)?" >> getLine
>      unless ("y" `isPrefixOf` input) $ goto exit
>      putStrLn "Something."
>
>      input <- putStrLn "Print more (y/n)?" >> getLine
>      unless ("y" `isPrefixOf` input) $ goto exit
>      putStrLn "More."
>
>      where
>        exit = putStrLn "Ok, I'm exiting."
>
>
> main :: IO ()
> main = do
>   handle (\GoTo -> return ()) myComp 
>   putStrLn "At the end"
  
There is no longer any need in the ContT monad transformer: IO
supports exceptions natively.

The solution exhibits a well-known memory leak. Consider

	do
	x <- make_huge_value
	goto long_running_computation
	return x

While long_running_computation keeps running, the value x is being
referenced from the stack and cannot be garbage collected. There is a
well-known solution to the problem: trampolining. We abort first and
then run the goto computation. This leads us to the final solution:

{-# LANGUAGE DeriveDataTypeable #-}

module C2 where

import Data.List

import Control.Monad
import Control.Exception
import Data.Typeable

data GoToIt = GoToIt (IO ()) deriving (Typeable)
instance Show GoToIt where show _ = "Trampoline"
instance Exception GoToIt

goto :: IO () -> IO a
goto m = throw (GoToIt m)

myComp :: IO ()
myComp = do
     input <- putStrLn "Print something (y/n)?" >> getLine
     unless ("y" `isPrefixOf` input) $ goto exit
     putStrLn "Something."

     input <- putStrLn "Print more (y/n)?" >> getLine
     unless ("y" `isPrefixOf` input) $ goto exit
     putStrLn "More."

     where
       exit = putStrLn "Ok, I'm exiting."


main :: IO ()
main = do
       handle_it myComp
       putStrLn "At the end"
 where handle_it m = handle (\(GoToIt m) -> handle_it m) m