-- Slides for the Continuation Tutorial
-- September 23, 2011 -- Toukyou, Japan.
module ContTutorial where
-- * Continuations are effects, and so we have to use monads
-- * The familiar Cont monad from the Monad transformer library
-- It is actually the monad of delimited control, as we shall see
import Control.Monad
import Control.Applicative
-- Let's see for simple expressions
-- Our earlier example in OCaml:
-- * reset (3 + shift (\k -> 5*2)) - 1
-- we have to use monads, and have to write the
-- expression in the monadic style
-- * The translation is mechanical
t1 = liftM2 (-)
(reset
(liftM2 (+) (return 3)
(shift (\k -> liftM2 (*) (return 5) (return 2)))))
(return 1)
-- * it does look like scheme, doesn't it?
-- What is that return?
-- Lesson: the type can tell us a lot about the expression:
-- after all, a type is an approximation of the expression's
-- behavior, which tell us what an expression is without
-- running it. Can you guess what liftM2 does?
-- Now, what is the type of t1? What does it tell?
-- How to run:
t1r = runC t1
-- 9
-- * The expression t1 looks ugly, even to a Schemer.
-- We can write it better:
t1' = liftM2 (-)
(reset
(liftM2 (+) (return 3)
(shift (\k -> return (5*2)))))
(return 1)
t1'r = runC t1'
-- * What did I do? How to justify what I just did?
-- An instance of the so-called monad law.
-- We can do more simplifications, this time syntactic
infixl 6 -!,+!
infixl 7 *!
(-!),(+!),(*!) :: (Num a, Monad m) => m a -> m a -> m a
(-!) = liftM2 (-)
(+!) = liftM2 (+)
(*!) = liftM2 (*)
t12 = reset (return 3 +! shift (\k -> return (5*2))) -! return 1
t12r = runC t12
-- 9
-- We can even remove return and so make the code look
-- just like the OCaml code. Doing it is left as a homework.
-- We won't do that however.
-- * Explicitness in pursuit of insight is no vice.
-- More examples
-- * (3) fst (reset (fun () -> let x = [] in (x, x)))
-- We see that `let' corresponds to `do'
t13 = liftM fst (reset $ do
x <- shift (\k -> return ("hi","bye"))
return (x,x))
t13r = runC t13
-- (1) 5 * reset (fun () -> [] + 3 * 4)
-- (2) reset (fun () -> if [] then "hello" else "hi") ^ " world"
-- (3) fst (reset (fun () -> let x = [] in (x, x)))
-- (4) string_length (reset (fun () -> "x" ^ string_of_int []))
-- *//
-- * Rather than extracting a continuation as a function,
-- * and then applying to something, we apply it right away.
t2 = reset (return 3 +! shift (\k -> return (k (5*2)))) -! return 1
t2r = runC t2
-- 12
-- We can apply the captured continuation more than once within
-- the same expression:
t3 :: Cont Int Int
t3 = reset
(return 2 *! shift(\k -> return $ k (k 10))) +! return 1
t3r = runC t3
-- 41
-- * //
-- It is time now to introduce the continuation monad and
-- show how shift and reset are written in it.
newtype Cont w a = Cont{runCont :: (a -> w) -> w}
instance Monad (Cont w) where
return x = Cont (\k -> k x)
Cont m >>= f = Cont (\k -> m (\v -> runCont (f v) k))
instance Functor (Cont w) where
fmap f (Cont m) = Cont (\k -> m (k . f))
instance Applicative (Cont w) where
pure = return
m <*> a = m >>= \h -> fmap h a
runC :: Cont w w -> w
runC m = runCont m id
reset :: Cont a a -> Cont w a
reset = return . runC
shift :: ((a -> w) -> Cont w w) -> Cont w a
shift f = Cont (runC . f)
-- * //
-- * The big question: is this correct?
-- The results seem to be expected so far,
-- and in the agreement with OchaCaml. How to make sure they always
-- agree? To be certain, we need to say what is the specification
-- for shift/reset, and demonstrate that our implementation satisfies
-- the specification.
-- * Specification: so-called bubble-up semantics
-- which was the original semantics of delimited control (prompt/control)
-- introduced by Felleisen. That bubble-up semantics was re-discovered
-- for the so-called lambda-mu calculus, which is the calculus
-- for classical logic.
-- shift introduces a bubble
-- * shift body --> 泡 id body
-- The bubble propagates:
-- * (泡 k body) + e1 --> 泡 (\x -> (k x) + e1) body
-- * (泡 k body) e1 --> 泡 (\x -> (k x) e1) body
-- * f (泡 k body) --> 泡 (\x -> f (k x)) body
-- * if (泡 k body) then e1 else e2 -->
-- * 泡 (\x -> if (k x) then e1 else e2) body
-- reset pricks (eliminates) the bubble
-- * reset (泡 k body) --> reset (body (\x -> reset (k x)))
-- * reset value --> value
-- The bubble-up semantics helps in practice, too: see
-- the end of this file.
-- * eta-expand shift
-- to make the bubble representation explicit
shift' body = Cont (\k -> runC (body (\u -> runCont (return u) k)))
-- Here is the representation of the bubble:
泡 ctx body = Cont (\k -> runC (body (\u -> runCont (ctx u) k)))
-- * //
-- * Let us demonstrate that the propagation of the Cont bubble
-- * through the application matches the specification:
-- * (泡 k body) e1 --> 泡 (\x -> (k x) e1) body
proof1 body ctx e =
泡 ctx body <*> e
===
泡 ctx body >>= \h -> (fmap h e)
===
Cont (\ks -> runC (body (\u -> runCont (ctx u) ks))) >>=
\h -> (fmap h e)
===
Cont (\k ->
(\ks -> runC (body (\u -> runCont (ctx u) ks)))
(\v -> runCont ((\h -> (fmap h e)) v) k))
===
Cont (\k ->
(\ks -> runC (body (\u -> runCont (ctx u) ks)))
(\v -> runCont (fmap v e) k))
===
Cont (\k ->
runC (body (\u -> runCont (ctx u) (\v -> runCont (fmap v e) k)))
)
-- an inner expression is almost the same as
-- let g = (\v -> fmap v e) in
-- ctx u >>= g ===
-- Cont (\k1 -> runCont (ctx u) (\v -> runCont (g v) k1))
-- modulo the replacement of k1 with k
===
Cont (\k ->
runC (body (\u -> runCont (ctx u >>= \v -> fmap v e) k)))
===
let ctx' u = ctx u >>= \v -> fmap v e in
Cont (\k -> runC (body (\u -> runCont (ctx' u) k)))
===
let ctx' u = ctx u >>= \v -> fmap v e in
泡 (\u -> ctx u >>= \v -> fmap v e) body
===
泡 (\u -> ctx u <*> e) body
-- * To remind the specification rule:
-- * (泡 k body) e1 --> 泡 (\x -> (k x) e1) body
-- * The result matches the specification.
-- * The other bubble-propagation rules can be checked
-- * similarly.
-- * //
-- Our equational proof was written in Haskell!
-- It was not mechanically checked. But at least it is well-typed.
-- GHC (at present) cannot verify that
-- each step in the proof is valid; we need a real theorem prover for
-- that. However GHC does verify that the premise is well-typed
-- and each step in the proof is type preserving.
-- GHC thus already catches many silly errors during equational
-- re-writing: mis-substitutions tend to break type preservation.
infixl 0 ===
-- `Propositional equality'
-- It should really be proven than `computed'. Therefore,
-- the computation below is trivial
(===) :: a -> a -> a
(===) = const
-- * Let us check that the Cont bubble elimination matches
-- * the specification:
-- * reset (泡 ctx body) --> reset (body (\x -> reset (ctx x)))
proof2 body ctx =
reset (泡 ctx body)
===
reset (Cont (\k -> runC (body (\u -> runCont (ctx u) k))))
===
return (runC (Cont (\k -> runC (body (\u -> runCont (ctx u) k)))))
===
return ((\k -> runC (body (\u -> runCont (ctx u) k))) id)
===
return (runC (body (\u -> runCont (ctx u) id)))
===
reset (body (\u -> runCont (ctx u) id))
===
reset (body (\u -> runC (ctx u)))
-- * If the k were of the type a -> Cont w a, we would have
-- * added return, and noticed that return . runC === reset
-- The continuation captured by shift is a pure
-- function (that is, has no effects), we make this
-- fact explicit in its type.
-- We now demonstrate that the Cont monad reset when applied
-- to a value returns the value:
-- * reset value --> value
proof3 v =
reset (return v)
===
reset (Cont (\k -> k v))
===
return (runC (Cont (\k -> k v)))
===
return ((\k -> k v) id)
===
return v
-- If determining the result of t3 in your head was difficult,
-- let us show how the bubble-up semantics helps.
-- The bubble-up semantics makes determining the result of t3
-- a pure mechanical operation.
t3r' =
runC (reset
(return 2 *! shift(\k -> return $ k (k 10))) +! return 1)
-- shift introduces the bubble
===
runC (reset
(return 2 *! 泡 return (\k -> return $ k (k 10))) +! return 1)
-- the bubble propagates up and devours `return 2 *!'
===
runC (reset
(泡 (\x -> return 2 *! return x)
(\k -> return $ k (k 10))) +! return 1)
-- simplifying using the monad law
===
runC (reset
(泡 (\x -> return (2 * x))
(\k -> return $ k (k 10))) +! return 1)
-- reset pricks the bubble
===
runC (reset ((\k -> return $ k (k 10)) (\x -> runC (return (2 * x))))
+! return 1)
-- runC . return === id
===
runC (reset ((\k -> return $ k (k 10)) (\x -> 2 * x)) +! return 1)
-- beta-reduction
===
runC (reset (return 40) +! return 1)
-- reset of a value
===
runC (return 40 +! return 1)
-- monad law (addition of pure expressions)
===
runC (return 41)
===
41