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