author Chris Wed, 13 May 2015 17:27:44 +0000 (13:27 -0400) committer Chris Wed, 13 May 2015 17:27:44 +0000 (13:27 -0400)

index 3873215..125bc3a 100644 (file)
@@ -1,289 +1,3 @@
**Note to Chris**: [[don't forget this material to be merged in somehow|/topics/_cps_and_continuation_operators]]. I marked where I cut some material to put into week13_control_operators, but that page is still a work in progress in my browser...

-Gaining control over order of evaluation
-----------------------------------------
-
-We know that evaluation order matters.  We're beginning to learn how
-to gain some control over order of evaluation (think of Jim's abort handler).
-We continue to reason about order of evaluation.
-
-A lucid discussion of evaluation order in the
-context of the lambda calculus can be found here:
-[Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
-Sestoft also provides a lovely on-line lambda evaluator:
-[Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
-which allows you to select multiple evaluation strategies,
-and to see reductions happen step by step.
-
-Evaluation order matters
-------------------------
-
-We've seen this many times.  For instance, consider the following
-reductions.  It will be convenient to use the abbreviation `w =
-\x.xx`.  I'll
-indicate which lambda is about to be reduced with a * underneath:
-
-<pre>
-(\x.y)(ww)
- *
-y
-</pre>
-
-Done!  We have a normal form.  But if we reduce using a different
-strategy, things go wrong:
-
-<pre>
-(\x.y)(ww) =
-(\x.y)((\x.xx)w) =
-        *
-(\x.y)(ww) =
-(\x.y)((\x.xx)w) =
-        *
-(\x.y)(ww)
-</pre>
-
-Etc.
-
-As a second reminder of when evaluation order matters, consider using
-`Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:
-
-<pre>
-Y (\f n. blah) =
-(\f.(\h.f(hh))(\h.f(hh))) (\f n. blah)
-     *
-(\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah)
-       *
-(\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah)
-         *
-(\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah)
-</pre>
-
-And we never get the recursion off the ground.
-
-
-Using a Continuation Passing Style transform to control order of evaluation
----------------------------------------------------------------------------
-
-We'll present a technique for controlling evaluation order by transforming a lambda term
-using a Continuation Passing Style transform (CPS), then we'll explore
-what the CPS is doing, and how.
-
-In order for the CPS to work, we have to adopt a new restriction on
-beta reduction: beta reduction does not occur underneath a lambda.
-That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to
-`\u.z`, because the `\u` protects the redex in the body from
-reduction.  (In this context, a "redex" is a part of a term that matches
-the pattern `...((\xM)N)...`, i.e., something that can potentially be
-the target of beta reduction.)
-
-Start with a simple form that has two different reduction paths:
-
-reducing the leftmost lambda first: `(\x.y)((\x.z)u)  ~~> y`
-
-reducing the rightmost lambda first: `(\x.y)((\x.z)u)  ~~> (\x.y)z ~~> y`
-
-After using the following call-by-name CPS transform---and assuming
-that we never evaluate redexes protected by a lambda---only the first
-reduction path will be available: we will have gained control over the
-order in which beta reductions are allowed to be performed.
-
-Here's the CPS transform defined:
-
-    [x] = x
-    [\xM] = \k.k(\x[M])
-    [MN] = \k.[M](\m.m[N]k)
-
-Here's the result of applying the transform to our simple example:
-
-    [(\x.y)((\x.z)u)] =
-    \k.[\x.y](\m.m[(\x.z)u]k) =
-    \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
-    \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)
-
-Because the initial `\k` protects (i.e., takes scope over) the entire
-transformed term, we can't perform any reductions.  In order to watch
-the computation unfold, we have to apply the transformed term to a
-trivial continuation, usually the identity function `I = \x.x`.
-
-    [(\x.y)((\x.z)u)] I =
-    (\k.[\x.y](\m.m[(\x.z)u]k)) I
-     *
-    [\x.y](\m.m[(\x.z)u] I) =
-    (\k.k(\x.y))(\m.m[(\x.z)u] I)
-     *           *
-    (\x.y)[(\x.z)u] I           --A--
-     *
-    y I
-
-The application to `I` unlocks the leftmost functor.  Because that
-functor (`\x.y`) throws away its argument (consider the reduction in the
-line marked (A)), we never need to expand the
-CPS transform of the argument.  This means that we never bother to
-reduce redexes inside the argument.
-
-Compare with a call-by-value xform:
-
-    {x} = \k.kx
-    {\aM} = \k.k(\a{M})
-    {MN} = \k.{M}(\m.{N}(\n.mnk))
-
-This time the reduction unfolds in a different manner:
-
-    {(\x.y)((\x.z)u)} I =
-    (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
-     *
-    {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
-    (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
-     *             *
-    {(\x.z)u}(\n.(\x.{y})nI) =
-    (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI)
-     *
-    {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
-    (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI)))
-     *             *
-    {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
-    (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
-     *      *
-    (\x.{z})u(\n.(\x.{y})nI)       --A--
-     *
-    {z}(\n.(\x.{y})nI) =
-    (\k.kz)(\n.(\x.{y})nI)
-     *      *
-    (\x.{y})zI
-     *
-    {y}I =
-    (\k.ky)I
-     *
-    I y
-
-In this case, the argument does get evaluated: consider the reduction
-in the line marked (A).
-
-Both xforms make the following guarantee: as long as redexes
-underneath a lambda are never evaluated, there will be at most one
-reduction available at any step in the evaluation.
-That is, all choice is removed from the evaluation process.
-
-Now let's verify that the CBN CPS avoids the infinite reduction path
-discussed above (remember that `w = \x.xx`):
-
-    [(\x.y)(ww)] I =
-    (\k.[\x.y](\m.m[ww]k)) I
-     *
-    [\x.y](\m.m[ww]I) =
-    (\k.k(\x.y))(\m.m[ww]I)
-     *             *
-    (\x.y)[ww]I
-     *
-    y I
-
-
-Questions and exercises:
-
-1. Prove that {(\x.y)(ww)} does not terminate.
-
-2. Why is the CBN xform for variables `[x] = x` instead of something
-involving kappas (i.e., `k`'s)?
-
-3. Write an Ocaml function that takes a lambda term and returns a
-CPS-xformed lambda term.  You can use the following data declaration:
-
-    type form = Var of char | Abs of char * form | App of form * form;;
-
-4. The discussion above talks about the "leftmost" redex, or the
-"rightmost".  But these words apply accurately only in a special set
-of terms.  Characterize the order of evaluation for CBN (likewise, for
-CBV) more completely and carefully.
-
-5. What happens (in terms of evaluation order) when the application
-rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
-
-6. A term and its CPS xform are different lambda terms.  Yet in some
-sense they "do" the same thing computationally.  Make this sense
-precise.
-
-
-Thinking through the types
---------------------------
-
-
-Let's say we're working in the simply-typed lambda calculus.
-Then if the original term is well-typed, the CPS xform will also be
-well-typed.  But what will the type of the transformed term be?
-
-The transformed terms all have the form `\k.blah`.  The rule for the
-CBN xform of a variable appears to be an exception, but instead of
-writing `[x] = x`, we can write `[x] = \k.xk`, which is
-eta-equivalent.  The `k`'s are continuations: functions from something
-to a result.  Let's use &sigma; as the result type.  The each `k` in
-the transform will be a function of type &rho; --> &sigma; for some
-choice of &rho;.
-
-We'll need an ancilliary function ': for any ground type a, a' = a;
-for functional types a->b, (a->b)' = ((a' -> &sigma;) -> &sigma;) -> (b' -> &sigma;) -> &sigma;.
-
-    Call by name transform
-
-    Terms                            Types
-
-    [x] = \k.xk                      [a] = (a'->o)->o
-    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
-    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o
-
-Remember that types associate to the right.  Let's work through the
-application xform and make sure the types are consistent.  We'll have
-the following types:
-
-    M:a->b
-    N:a
-    MN:b
-    k:b'->o
-    [N]:(a'->o)->o
-    m:((a'->o)->o)->(b'->o)->o
-    m[N]:(b'->o)->o
-    m[N]k:o
-    [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
-    [M](\m.m[N]k):o
-    [MN]:(b'->o)->o
-
-Be aware that even though the transform uses the same symbol for the
-translation of a variable (i.e., `[x] = x`), in general the variable
-in the transformed term will have a different type than in the source
-term.
-
-Excercise: what should the function ' be for the CBV xform?  Hint:
-
-
-Other CPS transforms
---------------------
-
-It is easy to think that CBN and CBV are the only two CPS transforms.
-(We've already seen a variant on call-by-value one of the excercises above.)
-
-In fact, the number of distinct transforms is unbounded.  For
-instance, here is a variant of CBV that uses the same types as CBN:
-
-    <x> = x
-    <\xM> = \k.k(\x<M>)
-    <MN> = \k.<M>(\m.<N>(\n.m(\k.kn)k))
-
-Try reducing `<(\x.x) ((\y.y) (\z.z))> I` to convince yourself that
-this is a version of call-by-value.
-
-Once we have two evaluation strategies that rely on the same types, we
-can mix and match:
-
-    [x] = x
-    <x> = x
-    [\xM] = \k.k(\x<M>)
-    <\xM] = \k.k(\x[M])
-    [MN] = \k.<M>(\m.m<N>k)
-    <MN> = \k.[M](\m.[N](\n.m(\k.kn)k))
-
-This xform interleaves call-by-name and call-by-value in layers,
-according to the depth of embedding.
-(Cf. page 4 of Reynold's 1974 paper ftp://ftp.cs.cmu.edu/user/jcr/reldircont.pdf (equation (4) and the
-explanation in the paragraph below.)
index 679f0fb..f09f336 100644 (file)
@@ -1,684 +1,2 @@
[[!toc]]

-CPS Transforms
-==============
-
-We've already approached some tasks now by programming in **continuation-passing style.** We first did that with tuples at the start of term, and then with the v5 lists in [[week4]], and now more recently and self-consciously when discussing [aborts](/couroutines_and_aborts),
-and [the "abSd" task](/from_list_zippers_to_continuations). and the use of `tree_monadize` specialized to the Continuation monad, which required us to supply an initial continuation.
-
-In our discussion of aborts, we showed how to rearrange code like this:
-
-
-       let foo x =
-       +---try begin----------------+
-       |       (if x = 1 then 10    |
-       |       else abort 20        |
-       |       ) + 100              |
-       +---end----------------------+
-       in (foo 2) + 1000;;
-
-into a form like this:
-
-       let x = 2
-       in let snapshot = fun box ->
-           let foo_result = box
-           in (foo_result) + 1000
-       in let continue_normally = fun from_value ->
-           let value = from_value + 100
-           in snapshot value
-       in
-           if x = 1 then continue_normally 10
-           else snapshot 20;;
-
-<!--
-# #require "delimcc";;
-# open Delimcc;;
-# let reset body = let p = new_prompt () in push_prompt p (body p);;
-# let test_cps x =
-      let snapshot = fun box ->
-          let foo_result = box
-          in (foo_result) + 1000
-      in let continue_normally = fun from_value ->
-          let value = from_value + 100
-          in snapshot value
-      in if x = 1 then continue_normally 10
-      else snapshot 20;;
-
-       let foo x =
-       +===try begin================+
-       |       (if x = 1 then 10    |
-       |       else abort 20        |
-       |       ) + 100              |
-       +===end======================+
-       in (foo 2) + 1000;;
-
-# let test_shift x =
-    let foo x = reset(fun p () ->
-        (shift p (fun k ->
-            if x = 1 then k 10 else 20)
-        ) + 100)
-    in foo z + 1000;;
-
-# test_cps 1;;
-- : int = 1110
-# test_shift 1;;
-- : int = 1110
-# test_cps 2;;
-- : int = 1020
-# test_shift 2;;
-- : int = 1020
--->
-
-How did we figure out how to rearrange that code? There are algorithms that can do this for us mechanically. These algorithms are known as **CPS transforms**, because they transform code that might not yet be in CPS form into that form.
-
-We won't attempt to give a full CPS transform for OCaml; instead we'll just focus on the lambda calculus and a few extras, to be introduced as we proceed.
-
-In fact there are multiple ways to do a CPS transform. Here is one:
-
-       [x]     --> x
-       [\x. M] --> \k. k (\x. [M])
-       [M N]   --> \k. [M] (\m. m [N] k)
-
-And here is another:
-
-       [x]     --> \k. k x
-       [\x. M] --> \k. k (\x. [M])
-       [M N]   --> \k. [M] (\m. [N] (\n. m n k))
-
-These transforms have some interesting properties. One is that---assuming we never reduce inside a lambda term, but only when redexes are present in the outermost level---the formulas generated by these transforms will always only have a single candidate redex to be reduced at any stage. In other words, the generated expressions dictate in what order the components from the original expressions will be evaluated. As it happens, the first transform above forces a *call-by-name* reduction order: assuming `M N` to be a redex, redexes inside `N` will be evaluated only after `N` has been substituted into `M`. And the second transform forces a *call-by-value* reduction order. These reduction orders will be forced no matter what the native reduction order of the interpreter is, just so long as we're only allowed to reduce redexes not underneath lambdas.
-
-Plotkin did important early work with CPS transforms, and they are now a staple of academic computer science. (See the end of his 1975 paper [Call-by-name, call-by-value, and the lambda-calculus](http://homepages.inf.ed.ac.uk/gdp/publications/cbn_cbv_lambda.pdf).)
-
-Here's another interesting fact about these transforms. Compare the translations for variables and applications in the call-by-value transform:
-
-       [x]     --> \k. k x
-       [M N]   --> \k. [M] (\m. [N] (\n. m n k))
-
-to the implementations we proposed for `unit` and `bind` when developing a Continuation monads, for example [here](/list_monad_as_continuation_monad). I'll relabel some of the variable names to help the comparison:
-
-       let cont_unit x = fun k -> k x
-       let cont_bind N M = fun k -> N (fun n -> M n k)
-
-The transform for `x` is just `cont_unit x`! And the transform for `M N` is, though not here exactly the same as `cont_bind N M`, quite reminiscent of it. (I don't yet know whether there's an easy and satisfying explanation of why these two are related as they are.) <!-- FIXME -->
-
-Doing CPS transforms by hand is very cumbersome. (Try it.) But you can leverage our lambda evaluator to help you out. Here's how to do it. From here on out, we'll be working with and extending the call-by-value CPS transform set out above:
-
-       let var = \x (\k. k x) in
-       let lam = \x_body (\k. k (\x. x_body x)) in
-       let app = \m n. (\k. m (\m. n (\n. m n k))) in
-       ...
-
-Then if you want to use [x], you'd write `var x`. If you want to use [\x. body], you'd write `lam (\x. BODY)`, where `BODY` is whatever [body] amounts to. If you want to use [m n], you'd write `app M N`, where M and N are whatever [m] and [n] amount to.
-
-To play around with this, you'll also want to help yourself to some primitives already in CPS form. (You won't want to rebuild everything again from scratch.) For a unary function like `succ`, you can take its primitive CPS analogue [succ] to be `\u. u (\a k. k (succ a))` (where `succ` in this expansion is the familiar non-CPS form of `succ`). Then for example:
-
-       [succ x]
-                 = \k. [succ] (\m. [x] (\n. m n k))
-               ~~> ...
-               ~~> \k. k (succ x)
-
-Or, using the lambda evaluator, that is:
-
-       ...
-       let op1 = \op. \u. u (\a k. k (op a)) in
-       app (op1 succ) (var x)
-       ~~> \k. k (succ x)
-
-Some other handy tools:
-
-       let app2 = \a b c. app (app a b) c in
-       let app3 = \a b c d. app (app (app a b) c) d in
-       let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
-       let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
-       ...
-
-Then, for instance, [plus x y] would be rendered in the lambda evaluator as:
-
-       app2 (op2 plus) (var x) (var y)
-       ~~> \k. k (plus x y)
-
-To finish off a CPS computation, you have to supply it with an "initial" or "outermost" continuation. (This is somewhat like "running" a monadic computation.) Usually you'll give the identity function, representing that nothing further happens to the continuation-expecting value.
-
-If the program you're working with is already in CPS form, then some elegant and powerful computational patterns become available, as we've been seeing. But it's tedious to convert to and work in fully-explicit CPS form. Usually you'll just want to be using the power of continuations at some few points in your program. It'd be nice if we had some way to make use of those patterns without having to convert our code explicitly into CPS form.
-
-Callcc
-======
-
-Well, we can. Consider the space of lambda formulas. Consider their image under a CPS transform. There will be many well-formed lambda expressions not in that image---that is, expressions that aren't anybody's CPS transform. Some of these will be useful levers in the CPS patterns we want to make use of. We can think of them as being the CPS transforms of some new syntax in the original language. For example, the expression `callcc` is explained as a new bit of syntax having some of that otherwise unclaimed CPS real-estate. The meaning of the new syntax can be understood in terms of how the CPS transform we specify for it behaves, when the whole language is in CPS form.
-
-I won't give the CPS transform for `callcc` itself, but instead for the complex form:
-
-       [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
-
-The behavior of `callcc` is this. The whole expression `callcc (\k. body)`, call it C, is being evaluated in a context, call it E[\_]. When we convert to CPS form, the continuation of this occurrence of C will be bound to the variable `outk`. What happens then is that we bind the expression `\v localk. outk v` to the variable `k` and evaluate [body], passing through to it the existing continuation `outk`. Now if `body` is just, for example, `x`, then its CPS transform [x] will be `\j. j x` and this will accept the continuation `outk` and feed it `x`, and we'll continue on with nothing unusual occurring. If on the other hand `body` makes use of the variable `k`, what happens then? For example, suppose `body` includes `foo (k v)`. In the reduction of the CPS transform `[foo (k v)]`, `v` will be passed to `k` which as we said is now `\v localk. outk v`. The continuation of that application---what is scheduled to happen to `k v` after it's evaluated and `foo` gets access to it---will be bound next to `localk`. But notice that this `localk` is discarded. The computation goes on without it. Instead, it just continues evaluating `outk v`, where as we said `outk` is the outside continuation E[\_] of the whole `callcc (\k. body)` invocation.
-
-So in other words, since the continuation in which `foo` was to be applied to the value of `k v` was discarded, that application never gets evaluated. We escape from that whole block of code.
-
-It's important to understand that `callcc` binds `k` to a pipe into the continuation as still then installed. Not just to a function that performs the same computation as the context E[\_] does---that has the same normal form and extension. But rather, a pipe into E[\_] *in its continuation-playing role*. This is manifested by the fact that when `k v` finishes evaluating, that value is not delivered to `foo` for the computation to proceed. Instead, when `k v` finishes evaluating, the program will then be done. Not because of some "stop here" block attached to `k`, but rather because of what it is that `k` represents. Walking through the explanation above several times may help you understand this better.
-
-So too will examples. We'll give some examples, and show you how to try them out in a variety of formats:
-
-1.     using the lambda evaluator to check how the CPS transforms reduce
-
-       To do this, you can use the following helper function:
-
-               let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
-               ...
-
-       Used like this: [callcc (\k. body)] = `callcc (\k. BODY)`, where `BODY` is [body].
-
-2.     using a `callcc` operation on our Continuation monad
-
-       This is implemented like this:
-
-               let callcc body = fun outk -> body (fun v localk -> outk v) outk
-
-       <!-- GOTCHAS?? -->
-
--- cutting for control operators --
-
-3.     `callcc` was originally introduced in Scheme. There it's written `call/cc` and is an abbreviation of `call-with-current-continuation`. Instead of the somewhat bulky form:
-
-               (call/cc (lambda (k) ...))
-
-       I prefer instead to use the lighter, and equivalent, shorthand:
-
-               (let/cc k ...)
-
-
-Callcc/letcc examples
----------------------
-
-First, here are two examples in Scheme:
-
-       (+ 100 (let/cc k (+ 10 1)))
-              |-----------------|
-
-This binds the continuation `outk` of the underlined expression to `k`, then computes `(+ 10 1)` and delivers that to `outk` in the normal way (not through `k`). No unusual behavior. It evaluates to `111`.
-
-
-       (+ 100 (let/cc k (+ 10 (k 1))))
-              |---------------------|
-
-This time, during the evaluation of `(+ 10 (k 1))`, we supply `1` to `k`. So then the local continuation, which delivers the value up to `(+ 10 [_])` and so on, is discarded. Instead `1` gets supplied to the outer continuation in place when `let/cc` was invoked. That will be `(+ 100 [_])`. When `(+ 100 1)` is evaluated, there's no more of the computation left to evaluate. So the answer here is `101`.
-
-You are not restricted to calling a bound continuation only once, nor are you restricted to calling it only inside of the `call/cc` (or `let/cc`) block. For example, you can do this:
-
-       (let ([p (let/cc k (cons 1 k))])
-         (cons (car p) ((cdr p) (cons 2 (lambda (x) x)))))
-       ; evaluates to '(2 2 . #<procedure>)
-
-What happens here? First, we capture the continuation where `p` is about to be assigned a value. Inside the `let/cc` block, we create a pair consisting of `1` and the captured continuation. This pair is bound to p. We then proceed to extract the components of the pair. The head (`car`) goes into the start of a tuple we're building up. To get the next piece of the tuple, we extract the second component of `p` (this is the bound continuation `k`) and we apply it to a pair consisting of `2` and the identity function. Supplying arguments to `k` takes us back to the point where `p` is about to be assigned a value. The tuple we had formerly been building, starting with `1`, will no longer be accessible because we didn't bring along with us any way to refer to it, and we'll never get back to the context where we supplied an argument to `k`. Now `p` gets assigned not the result of `(let/cc k (cons 1 k))` again, but instead, the new pair that we provided: `'(2 . #<identity procedure>)`. Again we proceed to build up a tuple: we take the first element `2`, then we take the second element (now the identity function), and feed it a pair `'(2 . #<identity procedure>)`, and since it's an argument to the identity procedure that's also the result. So our final result is a nested pair, whose first element is `2` and whose second element is the pair `'(2 . #<identity procedure>)`. Racket displays this nested pair like this:
-
-       '(2 2 . #<procedure>)
-
--- end of cut --
-
-Ok, so now let's see how to perform these same computations via CPS.
-
-In the lambda evaluator:
-
-       let var = \x (\k. k x) in
-       let lam = \x_body (\k. k (\x. x_body x)) in
-       let app = \m n. (\k. m (\m. n (\n. m n k))) in
-       let app2 = \a b c. app (app a b) c in
-       let app3 = \a b c d. app (app (app a b) c) d in
-       let op1 = \op. \u. u (\a k. k (op a)) in
-       let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
-       let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
-       let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
-
-       ; (+ 100 (let/cc k (+ 10 1))) ~~> 111
-       app2 (op2 plus) (var hundred) (callcc (\k. app2 (op2 plus) (var ten) (var one)))
-       ; evaluates to \k. k (plus hundred (plus ten one))
-
-Next:
-
-       ; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101
-       app2 (op2 plus) (var hundred) (callcc (\k. app2 (op2 plus) (var ten) (app (var k) (var one))))
-       ; evaluates to \k. k (plus hundred one)
-
-We won't try to do the third example in this framework.
-
-Finally, using the Continuation monad from our OCaml monad library. We begin:
-
-       # module C = Continuation_monad;;
-
-Now what we want to do is something like this:
-
-       # C.(run0 (100 + callcc (fun k -> 10 + 1)));;
-
-`run0` is a special function in the Continuation monad that runs a value of that monad using the identity function as its initial continuation. The above expression won't type-check, for several reasons. First, we're trying to add 100 to `callcc (...)` but the latter is a `Continuation.m` value, not an `int`. So we have to do this instead:
-
-       # C.(run0 (callcc (fun k -> 10 + 1) >>= fun i -> 100 + i));;
-
-Except that's still no good, because `10 + 1` and `100 + i` are of type `int`, but their context demands Continuation monadic values. So we have to throw in some `unit`s:
-
-       # C.(run0 (callcc (fun k -> unit (10 + 1)) >>= fun i -> unit (100 + i)));;
-       - : int = 111
-
-This works and as you can see, delivers the same answer `111` that we got by the other methods.
-
-Next we try:
-
-       # C.(run0 (callcc (fun k -> unit (10 + (k 1))) >>= fun i -> unit (100 + i)));;
-
-That won't work because `k 1` doesn't have type `int`, but we're trying to add it to `10`. So we have to do instead:
-
-       # C.(run0 (callcc (fun k -> k 1 >>= fun j -> unit (10 + j)) >>= fun i -> unit (100 + i)));;
-       - : int = 101
-
-This also works and as you can see, delivers the expected answer `101`.
-
-The third example is more difficult to make work with the monadic library, because its types are tricky. I was able to get this to work, which uses OCaml's "polymorphic variants." These are generally more relaxed about typing. There may be a version that works with regular OCaml types, but I haven't yet been able to identify it. Here's what does work:
-
-       # C.(run0 (callcc (fun k -> unit (1,`Box k)) >>= fun (p1,`Box p2) -> p2 (2,`Box unit) >>= fun p2' -> unit (p1,p2')));;
-       - : int * (int * [ `Box of 'b -> ('a, 'b) C.m ] as 'b) as 'a =
-       (2, (2, `Box <fun>))
-
-<!-- FIXME -->
-
--- cutting following section for control operators --
-
-Some callcc/letcc exercises
----------------------------
-
-Here are a series of examples from *The Seasoned Schemer*, which we recommended at the start of term. It's not necessary to have the book to follow the exercises, though if you do have it, its walkthroughs will give you useful assistance.
-
-For reminders about Scheme syntax, see [here](/assignment8/) and [here](/week1/) and [here](/translating_between_ocaml_scheme_and_haskell). Other resources are on our [[Learning Scheme]] page.
-
-Most of the examples assume the following preface:
-
-       #lang racket
-
-       (define (atom? x)
-         (and (not (pair? x)) (not (null? x))))
-
-Now try to figure out what this function does:
-
-       (define alpha
-         (lambda (a lst)
-           (let/cc k ; now what will happen when k is called?
-             (letrec ([aux (lambda (l)
-                             (cond
-                               [(null? l) '()]
-                               [(eq? (car l) a) (k (aux (cdr l)))]
-                               [else (cons (car l) (aux (cdr l)))]))])
-               (aux lst)))))
-
-Here is [the answer](/hints/cps_hint_1), but try to figure it out for yourself.
-
-Next, try to figure out what this function does:
-
-       (define beta
-         (lambda (lst)
-           (let/cc k ; now what will happen when k is called?
-             (letrec ([aux (lambda (l)
-                             (cond
-                               [(null? l) '()]
-                               [(atom? (car l)) (k (car l))]
-                               [else (begin
-                                       ; what will the value of the next line be? why is it ignored?
-                                       (aux (car l))
-                                       (aux (cdr l)))]))])
-               (aux lst)))))
-
-Here is [the answer](/hints/cps_hint_2), but try to figure it out for yourself.
-
-Next, try to figure out what this function does:
-
-       (define gamma
-         (lambda (a lst)
-           (letrec ([aux (lambda (l k)
-                           (cond
-                             [(null? l) (k 'notfound)]
-                             [(eq? (car l) a) (cdr l)]
-                             [(atom? (car l)) (cons (car l) (aux (cdr l) k))]
-                             [else
-                              ; what happens when (car l) exists but isn't an atom?
-                              (let ([car2 (let/cc k2 ; now what will happen when k2 is called?
-                                            (aux (car l) k2))])
-                                (cond
-                                  ; when will the following condition be met? what happens then?
-                                  [(eq? car2 'notfound) (cons (car l) (aux (cdr l) k))]
-                                  [else (cons car2 (cdr l))]))]))]
-                    [lst2 (let/cc k1 ; now what will happen when k1 is called?
-                            (aux lst k1))])
-             (cond
-               ; when will the following condition be met?
-               [(eq? lst2 'notfound) lst]
-               [else lst2]))))
-
-Here is [the answer](/hints/cps_hint_3), but try to figure it out for yourself.
-
-Here is the hardest example. Try to figure out what this function does:
-
-       (define delta
-         (letrec ([yield (lambda (x) x)]
-                  [resume (lambda (x) x)]
-                  [walk (lambda (l)
-                          (cond
-                            ; is this the only case where walk returns a non-atom?
-                            [(null? l) '()]
-                            [(atom? (car l)) (begin
-                                               (let/cc k2 (begin
-                                                 (set! resume k2) ; now what will happen when resume is called?
-                                                 ; when the next line is executed, what will yield be bound to?
-                                                 (yield (car l))))
-                                               ; when will the next line be executed?
-                                               (walk (cdr l)))]
-                            [else (begin
-                                    ; what will the value of the next line be? why is it ignored?
-                                    (walk (car l))
-                                    (walk (cdr l)))]))]
-                  [next (lambda () ; next is a thunk
-                          (let/cc k3 (begin
-                            (set! yield k3) ; now what will happen when yield is called?
-                            ; when the next line is executed, what will resume be bound to?
-                            (resume 'blah))))]
-                  [check (lambda (prev)
-                           (let ([n (next)])
-                             (cond
-                               [(eq? n prev) #t]
-                               [(atom? n) (check n)]
-                               ; when will n fail to be an atom?
-                               [else #f])))])
-           (lambda (lst)
-             (let ([fst (let/cc k1 (begin
-                          (set! yield k1) ; now what will happen when yield is called?
-                          (walk lst)
-                          ; when will the next line be executed?
-                          (yield '())))])
-               (cond
-                 [(atom? fst) (check fst)]
-                 ; when will fst fail to be an atom?
-                 [else #f])
-               ))))
-
-Here is [the answer](/hints/cps_hint_4), but again, first try to figure it out for yourself.
-
-
-Delimited control operators
-===========================
-
-Here again is the CPS transform for `callcc`:
-
-       [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
-
-`callcc` is what's known as an *undelimited control operator*. That is, the continuations `outk` that get bound into our `k`s include all the code from the `call/cc ...` out to *and including* the end of the program. Calling such a continuation will never return any value to the call site.
-
-(See the technique employed in the `delta` example above, with the `(begin (let/cc k2 ...) ...)`, for a work-around. Also. if you've got a copy of *The Seasoned Schemer*, see the comparison of let/cc vs. "collector-using" (that is, partly CPS) functions at pp. 155-164.)
-
-Often times it's more useful to use a different pattern, where we instead capture only the code from the invocation of our control operator out to a certain boundary, not including the end of the program. These are called *delimited control operators*. A variety of these have been formulated. The most well-behaved from where we're coming from is the pair `reset` and `shift`. `reset` sets the boundary, and `shift` binds the continuation from the position where it's invoked out to that boundary.
-
-It works like this:
-
-       (1) outer code
-       ------- reset -------
-       | (2)               |
-       | +----shift k ---+ |
-       | | (3)           | |
-       | |               | |
-       | |               | |
-       | +---------------+ |
-       | (4)               |
-       +-------------------+
-       (5) more outer code
-
-First, the code in position (1) runs. Ignore position (2) for the moment. When we hit the `shift k`, the continuation between the `shift` and the `reset` will be captured and bound to `k`. Then the code in position (3) will run, with `k` so bound. The code in position (4) will never run, unless it's invoked through `k`. If the code in position (3) just ends with a regular value, and doesn't apply `k`, then the value returned by (3) is passed to (5) and the computation continues.
-
-So it's as though the middle box---the (2) and (4) region---is by default not evaluated. This code is instead bound to `k`, and it's up to other code whether and when to apply `k` to any argument. If `k` is applied to an argument, then what happens? Well it will be as if that were the argument supplied by (3) only now that argument does go to the code (4) syntactically enclosing (3). When (4) is finished, that value also goes to (5) (just as (3)'s value did when it ended with a regular value). `k` can be applied repeatedly, and every time the computation will traverse that same path from (4) into (5).
-
-I set (2) aside a moment ago. The story we just told is a bit too simple because the code in (2) needs to be evaluated because some of it may be relied on in (3).
-
-For instance, in Scheme this:
-
-       (require racket/control)
-
-       (reset
-        (let ([x 1])
-          (+ 10 (shift k x))))
-
-will return 1. The `(let ([x 1]) ...` part is evaluated, but the `(+ 10 ...` part is not.
-
-Notice we had to preface the Scheme code with `(require racket/control)`. You don't have to do anything special to use `call/cc` or `let/cc`; but to use the other control operators we'll discuss you do have to include that preface in Racket.
-
-This pattern should look somewhat familiar. Recall from our discussion of aborts, and repeated at the top of this page:
-
-       let foo x =
-       +---try begin----------------+
-       |       (if x = 1 then 10    |
-       |       else abort 20        |
-       |       ) + 100              |
-       +---end----------------------+
-       in (foo 2) + 1000;;
-
-The box is working like a reset. The `abort` is implemented with a `shift`. Earlier, we refactored our code into a more CPS form:
-
-       let x = 2
-       in let snapshot = fun box ->
-           let foo_result = box
-           in (foo_result) + 1000
-       in let continue_normally = fun from_value ->
-           let value = from_value + 100
-           in snapshot value
-       in
-           if x = 1 then continue_normally 10
-           else snapshot 20;;
-
-`snapshot` here corresponds to the code outside the `reset`. `continue_normally` is the middle block of code, between the `shift` and its surrounding `reset`. This is what gets bound to the `k` in our `shift`. The `if...` statement is inside a `shift`. Notice there that we invoke the bound continuation to "continue normally". We just invoke the outer continuation, saved in `snapshot` when we placed the `reset`, to skip the "continue normally" code and immediately abort to outside the box.
-
-
--- end of cut --
-
-
-Using `shift` and `reset` operators in OCaml, this would look like this:
-
-       #require "delimcc";;
-       let p = Delimcc.new_prompt ();;
-       let reset = Delimcc.push_prompt p;;
-       let shift = Delimcc.shift p;;
-       let abort = Delimcc.abort p;;
-
-       let foo x =
-         reset(fun () ->
-           shift(fun continue ->
-               if x = 1 then continue 10
-               else 20
-           ) + 100
-         )
-       in foo 2 + 1000;;
-       - : int = 1020
-
-If instead at the end we did `... foo 1 + 1000`, we'd get the result `1110`.
-
-The above OCaml code won't work out of the box; you have to compile and install a special library that Oleg wrote. We discuss it on our [translation page](/translating_between_ocaml_scheme_and_haskell). If you can't get it working, then you can play around with `shift` and `reset` in Scheme instead. Or in the Continuation monad. Or using CPS transforms of your code, with the help of the lambda evaluator.
-
-You can make the lambda evaluator perform the required CPS transforms with these helper functions:
-
-       let reset = \body. \outk. outk (body (\i i)) in
-       let shift = \k_body. \midk. (\k. (k_body k) (\i i)) (\a localk. localk (midk a)) in
-       let abort = \body. \midk. body (\i i) in
-       ...
-
-You use these like so:
-
-*      [reset body] is `reset BODY` where `BODY` is [body]
-*      [shift k body] is `shift (\k. BODY)` where `BODY` is [body]
-*      and [abort value] is `abort VALUE` where `VALUE` is [value]
-
-There are also `reset` and `shift` and `abort` operations in the Continuation monad in our OCaml [[monad library]]. You can check the code for details.
-
-
-As we said, there are many varieties of delimited continuations. Another common pair is `prompt` and `control`. There's no difference in meaning between `prompt` and `reset`; it's just that people tend to say `reset` when talking about `shift`, and `prompt` when talking about `control`. `control` acts subtly differently from `shift`. In the uses you're likely to make as you're just learning about continuations, you won't see any difference. If you'll do more research in this vicinity, you'll soon enough learn about the differences.
-
-(You can start by reading [the Racket docs](http://docs.racket-lang.org/reference/cont.html?q=shift&q=do#%28part._.Classical_.Control_.Operators%29).)
-
-
-Ken Shan has done terrific work exploring the relations of `shift` and `control` and other control operators to each other.
-
-In collecting these CPS transforms and implementing the monadic versions, we've been helped by Ken and by Oleg and by these papers:
-
-*      Danvy and Filinski, "Representing control: a study of the CPS transformation" (1992)
-*      Sabry, "Note on axiomatizing the semantics of control operators" (1996)
-
-
--- cutting some of the following for control operators --
-
-Examples of shift/reset/abort
------------------------------
-
-Here are some more examples of using delimited control operators. We present each example three ways: first a Scheme formulation; then we compute the same result using CPS and the lambda evaluator; then we do the same using the Continuation monad in OCaml. (We don't demonstrate the use of Oleg's delimcc library.)
-
-
-Example 1:
-
-       ; (+ 1000 (+ 100 (abort 11))) ~~> 11
-
-       app2 (op2 plus) (var thousand)
-         (app2 (op2 plus) (var hundred) (abort (var eleven)))
-
-           abort 11 >>= fun i ->
-           unit (100+i) >>= fun j ->
-           unit (1000+j)));;
-       - : int = 11
-
-When no `reset` is specified, there's understood to be an implicit one surrounding the entire computation (but unlike in the case of `callcc`, you still can't capture up to *and including* the end of the computation). So it makes no difference if we say instead:
-
-           reset (
-             abort 11 >>= fun i ->
-             unit (100+i) >>= fun j ->
-             unit (1000+j))));;
-       - : int = 11
-
-
-Example 2:
-
-       ; (+ 1000 (reset (+ 100 (abort 11)))) ~~> 1011
-
-       app2 (op2 plus) (var thousand)
-         (reset (app2 (op2 plus) (var hundred) (abort (var eleven))))
-
-           reset (
-             abort 11 >>= fun i ->
-             unit (100+i)
-           ) >>= fun j ->
-           unit (1000+j)));;
-       - : int = 1011
-
-Example 3:
-
-       ; (+ 1000 (reset (+ 100 (shift k (+ 10 1))))) ~~> 1011
-
-       app2 (op2 plus) (var thousand)
-         (reset (app2 (op2 plus) (var hundred)
-           (shift (\k. ((op2 plus) (var ten) (var one))))))
-
-         let v = reset (
-           let u = shift (fun k -> unit (10 + 1))
-           in u >>= fun x -> unit (100 + x)
-         ) in let w = v >>= fun x -> unit (1000 + x)
-         in run0 w);;
-       - : int = 1011
-
-Example 4:
-
-       ; (+ 1000 (reset (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111
-
-       app2 (op2 plus) (var thousand)
-         (reset (app2 (op2 plus) (var hundred)
-           (shift (\k. (app (var k) ((op2 plus) (var ten) (var one)))))))
-
-         let v = reset (
-           let u = shift (fun k -> k (10 :: ))
-           in u >>= fun x -> unit (100 :: x)
-         ) in let w = v >>= fun x -> unit (1000 :: x)
-         in run0 w);;
-       - : int list = [1000; 100; 10; 1]
-
-To demonstrate the different adding order between Examples 4 and 5, we use `::` in the OCaml version instead of `+`. Here is Example 5:
-
-       ; (+ 1000 (reset (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently
-
-       app2 (op2 plus) (var thousand)
-         (reset (app2 (op2 plus) (var hundred)
-           (shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
-
-       Continuation_monad.(let v = reset (
-           let u = shift (fun k -> k  >>= fun x -> unit (10 :: x))
-           in u >>= fun x -> unit (100 :: x)
-         ) in let w = v >>= fun x -> unit (1000 :: x)
-         in run0  w);;
-       - : int list = [1000; 10; 100; 1]
-
-
-Example 6:
-
-       ; (+ 100 ((reset (+ 10 (shift k k))) 1)) ~~> 111
-
-       app2 (op2 plus) (var hundred)
-         (app (reset (app2 (op2 plus) (var ten)
-           (shift (\k. (var k))))) (var one))
-
-       (* not sure if this example can be typed as-is in OCaml... this is the best I an do at the moment... *)
-
-       # type 'x either = Left of (int -> ('x,'x either) Continuation_monad.m) | Right of int;;
-       # Continuation_monad.(let v = reset (
-           shift (fun k -> unit (Left k)) >>= fun i -> unit (Right (10+i))
-         ) in let w = v >>= fun (Left k) ->
-             k 1 >>= fun (Right i) ->
-             unit (100+i)
-         in run0 w);;
-       - : int = 111
-
-<!--
-# type either = Left of (int -> either) | Right of int;;
-# let getleft e = match e with Left lft -> lft | Right _ -> failwith "not a Left";;
-# let getright e = match e with Right rt -> rt | Left _ -> failwith "not a Right";;
-# 100 + getright (let v = reset (fun p () -> Right (10 + shift p (fun k -> Left k))) in getleft v 1);;
--->
-
-Example 7:
-
-       ; (+ 100 (reset (+ 10 (shift k (k (k 1)))))) ~~> 121
-
-       app2 (op2 plus) (var hundred)
-         (reset (app2 (op2 plus) (var ten)
-           (shift (\k. app (var k) (app (var k) (var one))))))
-
-       Continuation_monad.(let v = reset (
-           let u = shift (fun k -> k 1 >>= fun x -> k x)
-           in u >>= fun x -> unit (10 + x)
-         ) in let w = v >>= fun x -> unit (100 + x)
-         in run0 w)
-       - : int = 121
-
-<!--
-
-       print_endline "=== pa_monad's Continuation Tests ============";;
-
-       (1, 5 = C.(run0 (unit 1 >>= fun x -> unit (x+4))) );;
-       (2, 9 = C.(run0 (reset (unit 5 >>= fun x -> unit (x+4)))) );;
-       (3, 9 = C.(run0 (reset (abort 5 >>= fun y -> unit (y+6)) >>= fun x -> unit (x+4))) );;
-       (4, 9 = C.(run0 (reset (reset (abort 5 >>= fun y -> unit (y+6))) >>= fun x -> unit (x+4))) );;
-       (5, 27 = C.(run0 (
-                                 let c = reset(abort 5 >>= fun y -> unit (y+6))
-                                 in reset(c >>= fun v1 -> abort 7 >>= fun v2 -> unit (v2+10) ) >>= fun x -> unit (x+20))) );;
-
-       (7, 117 = C.(run0 (reset (shift (fun sk -> sk 3 >>= sk >>= fun v3 -> unit (v3+100) ) >>= fun v1 -> unit (v1+2)) >>= fun x -> unit (x+10))) );;
-
-       (8, 115 = C.(run0 (reset (shift (fun sk -> sk 3 >>= fun v3 -> unit (v3+100)) >>= fun v1 -> unit (v1+2)) >>= fun x -> unit (x+10))) );;
-
-       (12, ["a"] = C.(run0 (reset (shift (fun f -> f [] >>= fun t -> unit ("a"::t)  ) >>= fun xv -> shift (fun _ -> unit xv)))) );;
-
-
-       (0, 15 = C.(run0 (let f k = k 10 >>= fun v-> unit (v+100) in reset (callcc f >>= fun v -> unit (v+5)))) );;
-
--->
index 42f2c11..7788af9 100644 (file)
@@ -275,3 +275,974 @@ is return Nothing.

Super cool.

+## Continuation Passing Style Transforms
+
+Gaining control over order of evaluation
+----------------------------------------
+
+We know that evaluation order matters.  We're beginning to learn how
+to gain some control over order of evaluation (think of Jim's abort handler).
+We continue to reason about order of evaluation.
+
+A lucid discussion of evaluation order in the
+context of the lambda calculus can be found here:
+[Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
+Sestoft also provides a lovely on-line lambda evaluator:
+[Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
+which allows you to select multiple evaluation strategies,
+and to see reductions happen step by step.
+
+Evaluation order matters
+------------------------
+
+We've seen this many times.  For instance, consider the following
+reductions.  It will be convenient to use the abbreviation `w =
+\x.xx`.  I'll
+indicate which lambda is about to be reduced with a * underneath:
+
+<pre>
+(\x.y)(ww)
+ *
+y
+</pre>
+
+Done!  We have a normal form.  But if we reduce using a different
+strategy, things go wrong:
+
+<pre>
+(\x.y)(ww) =
+(\x.y)((\x.xx)w) =
+        *
+(\x.y)(ww) =
+(\x.y)((\x.xx)w) =
+        *
+(\x.y)(ww)
+</pre>
+
+Etc.
+
+As a second reminder of when evaluation order matters, consider using
+`Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:
+
+<pre>
+Y (\f n. blah) =
+(\f.(\h.f(hh))(\h.f(hh))) (\f n. blah)
+     *
+(\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah)
+       *
+(\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah)
+         *
+(\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah)
+</pre>
+
+And we never get the recursion off the ground.
+
+
+Using a Continuation Passing Style transform to control order of evaluation
+---------------------------------------------------------------------------
+
+We'll present a technique for controlling evaluation order by transforming a lambda term
+using a Continuation Passing Style transform (CPS), then we'll explore
+what the CPS is doing, and how.
+
+In order for the CPS to work, we have to adopt a new restriction on
+beta reduction: beta reduction does not occur underneath a lambda.
+That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to
+`\u.z`, because the `\u` protects the redex in the body from
+reduction.  (In this context, a "redex" is a part of a term that matches
+the pattern `...((\xM)N)...`, i.e., something that can potentially be
+the target of beta reduction.)
+
+Start with a simple form that has two different reduction paths:
+
+reducing the leftmost lambda first: `(\x.y)((\x.z)u)  ~~> y`
+
+reducing the rightmost lambda first: `(\x.y)((\x.z)u)  ~~> (\x.y)z ~~> y`
+
+After using the following call-by-name CPS transform---and assuming
+that we never evaluate redexes protected by a lambda---only the first
+reduction path will be available: we will have gained control over the
+order in which beta reductions are allowed to be performed.
+
+Here's the CPS transform defined:
+
+    [x] = x
+    [\xM] = \k.k(\x[M])
+    [MN] = \k.[M](\m.m[N]k)
+
+Here's the result of applying the transform to our simple example:
+
+    [(\x.y)((\x.z)u)] =
+    \k.[\x.y](\m.m[(\x.z)u]k) =
+    \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
+    \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)
+
+Because the initial `\k` protects (i.e., takes scope over) the entire
+transformed term, we can't perform any reductions.  In order to watch
+the computation unfold, we have to apply the transformed term to a
+trivial continuation, usually the identity function `I = \x.x`.
+
+    [(\x.y)((\x.z)u)] I =
+    (\k.[\x.y](\m.m[(\x.z)u]k)) I
+     *
+    [\x.y](\m.m[(\x.z)u] I) =
+    (\k.k(\x.y))(\m.m[(\x.z)u] I)
+     *           *
+    (\x.y)[(\x.z)u] I           --A--
+     *
+    y I
+
+The application to `I` unlocks the leftmost functor.  Because that
+functor (`\x.y`) throws away its argument (consider the reduction in the
+line marked (A)), we never need to expand the
+CPS transform of the argument.  This means that we never bother to
+reduce redexes inside the argument.
+
+Compare with a call-by-value xform:
+
+    {x} = \k.kx
+    {\aM} = \k.k(\a{M})
+    {MN} = \k.{M}(\m.{N}(\n.mnk))
+
+This time the reduction unfolds in a different manner:
+
+    {(\x.y)((\x.z)u)} I =
+    (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
+     *
+    {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
+    (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
+     *             *
+    {(\x.z)u}(\n.(\x.{y})nI) =
+    (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI)
+     *
+    {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
+    (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI)))
+     *             *
+    {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
+    (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
+     *      *
+    (\x.{z})u(\n.(\x.{y})nI)       --A--
+     *
+    {z}(\n.(\x.{y})nI) =
+    (\k.kz)(\n.(\x.{y})nI)
+     *      *
+    (\x.{y})zI
+     *
+    {y}I =
+    (\k.ky)I
+     *
+    I y
+
+In this case, the argument does get evaluated: consider the reduction
+in the line marked (A).
+
+Both xforms make the following guarantee: as long as redexes
+underneath a lambda are never evaluated, there will be at most one
+reduction available at any step in the evaluation.
+That is, all choice is removed from the evaluation process.
+
+Now let's verify that the CBN CPS avoids the infinite reduction path
+discussed above (remember that `w = \x.xx`):
+
+    [(\x.y)(ww)] I =
+    (\k.[\x.y](\m.m[ww]k)) I
+     *
+    [\x.y](\m.m[ww]I) =
+    (\k.k(\x.y))(\m.m[ww]I)
+     *             *
+    (\x.y)[ww]I
+     *
+    y I
+
+
+Questions and exercises:
+
+1. Prove that {(\x.y)(ww)} does not terminate.
+
+2. Why is the CBN xform for variables `[x] = x` instead of something
+involving kappas (i.e., `k`'s)?
+
+3. Write an Ocaml function that takes a lambda term and returns a
+CPS-xformed lambda term.  You can use the following data declaration:
+
+    type form = Var of char | Abs of char * form | App of form * form;;
+
+4. The discussion above talks about the "leftmost" redex, or the
+"rightmost".  But these words apply accurately only in a special set
+of terms.  Characterize the order of evaluation for CBN (likewise, for
+CBV) more completely and carefully.
+
+5. What happens (in terms of evaluation order) when the application
+rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
+
+6. A term and its CPS xform are different lambda terms.  Yet in some
+sense they "do" the same thing computationally.  Make this sense
+precise.
+
+
+Thinking through the types
+--------------------------
+
+
+Let's say we're working in the simply-typed lambda calculus.
+Then if the original term is well-typed, the CPS xform will also be
+well-typed.  But what will the type of the transformed term be?
+
+The transformed terms all have the form `\k.blah`.  The rule for the
+CBN xform of a variable appears to be an exception, but instead of
+writing `[x] = x`, we can write `[x] = \k.xk`, which is
+eta-equivalent.  The `k`'s are continuations: functions from something
+to a result.  Let's use &sigma; as the result type.  The each `k` in
+the transform will be a function of type &rho; --> &sigma; for some
+choice of &rho;.
+
+We'll need an ancilliary function ': for any ground type a, a' = a;
+for functional types a->b, (a->b)' = ((a' -> &sigma;) -> &sigma;) -> (b' -> &sigma;) -> &sigma;.
+
+    Call by name transform
+
+    Terms                            Types
+
+    [x] = \k.xk                      [a] = (a'->o)->o
+    [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
+    [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o
+
+Remember that types associate to the right.  Let's work through the
+application xform and make sure the types are consistent.  We'll have
+the following types:
+
+    M:a->b
+    N:a
+    MN:b
+    k:b'->o
+    [N]:(a'->o)->o
+    m:((a'->o)->o)->(b'->o)->o
+    m[N]:(b'->o)->o
+    m[N]k:o
+    [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
+    [M](\m.m[N]k):o
+    [MN]:(b'->o)->o
+
+Be aware that even though the transform uses the same symbol for the
+translation of a variable (i.e., `[x] = x`), in general the variable
+in the transformed term will have a different type than in the source
+term.
+
+Excercise: what should the function ' be for the CBV xform?  Hint:
+
+
+Other CPS transforms
+--------------------
+
+It is easy to think that CBN and CBV are the only two CPS transforms.
+(We've already seen a variant on call-by-value one of the excercises above.)
+
+In fact, the number of distinct transforms is unbounded.  For
+instance, here is a variant of CBV that uses the same types as CBN:
+
+    <x> = x
+    <\xM> = \k.k(\x<M>)
+    <MN> = \k.<M>(\m.<N>(\n.m(\k.kn)k))
+
+Try reducing `<(\x.x) ((\y.y) (\z.z))> I` to convince yourself that
+this is a version of call-by-value.
+
+Once we have two evaluation strategies that rely on the same types, we
+can mix and match:
+
+    [x] = x
+    <x> = x
+    [\xM] = \k.k(\x<M>)
+    <\xM] = \k.k(\x[M])
+    [MN] = \k.<M>(\m.m<N>k)
+    <MN> = \k.[M](\m.[N](\n.m(\k.kn)k))
+
+This xform interleaves call-by-name and call-by-value in layers,
+according to the depth of embedding.
+(Cf. page 4 of Reynold's 1974 paper ftp://ftp.cs.cmu.edu/user/jcr/reldircont.pdf (equation (4) and the
+explanation in the paragraph below.)
+
+CPS Transforms
+==============
+
+We've already approached some tasks now by programming in **continuation-passing style.** We first did that with tuples at the start of term, and then with the v5 lists in [[week4]], and now more recently and self-consciously when discussing [aborts](/couroutines_and_aborts),
+and [the "abSd" task](/from_list_zippers_to_continuations). and the use of `tree_monadize` specialized to the Continuation monad, which required us to supply an initial continuation.
+
+In our discussion of aborts, we showed how to rearrange code like this:
+
+
+       let foo x =
+       +---try begin----------------+
+       |       (if x = 1 then 10    |
+       |       else abort 20        |
+       |       ) + 100              |
+       +---end----------------------+
+       in (foo 2) + 1000;;
+
+into a form like this:
+
+       let x = 2
+       in let snapshot = fun box ->
+           let foo_result = box
+           in (foo_result) + 1000
+       in let continue_normally = fun from_value ->
+           let value = from_value + 100
+           in snapshot value
+       in
+           if x = 1 then continue_normally 10
+           else snapshot 20;;
+
+<!--
+# #require "delimcc";;
+# open Delimcc;;
+# let reset body = let p = new_prompt () in push_prompt p (body p);;
+# let test_cps x =
+      let snapshot = fun box ->
+          let foo_result = box
+          in (foo_result) + 1000
+      in let continue_normally = fun from_value ->
+          let value = from_value + 100
+          in snapshot value
+      in if x = 1 then continue_normally 10
+      else snapshot 20;;
+
+       let foo x =
+       +===try begin================+
+       |       (if x = 1 then 10    |
+       |       else abort 20        |
+       |       ) + 100              |
+       +===end======================+
+       in (foo 2) + 1000;;
+
+# let test_shift x =
+    let foo x = reset(fun p () ->
+        (shift p (fun k ->
+            if x = 1 then k 10 else 20)
+        ) + 100)
+    in foo z + 1000;;
+
+# test_cps 1;;
+- : int = 1110
+# test_shift 1;;
+- : int = 1110
+# test_cps 2;;
+- : int = 1020
+# test_shift 2;;
+- : int = 1020
+-->
+
+How did we figure out how to rearrange that code? There are algorithms that can do this for us mechanically. These algorithms are known as **CPS transforms**, because they transform code that might not yet be in CPS form into that form.
+
+We won't attempt to give a full CPS transform for OCaml; instead we'll just focus on the lambda calculus and a few extras, to be introduced as we proceed.
+
+In fact there are multiple ways to do a CPS transform. Here is one:
+
+       [x]     --> x
+       [\x. M] --> \k. k (\x. [M])
+       [M N]   --> \k. [M] (\m. m [N] k)
+
+And here is another:
+
+       [x]     --> \k. k x
+       [\x. M] --> \k. k (\x. [M])
+       [M N]   --> \k. [M] (\m. [N] (\n. m n k))
+
+These transforms have some interesting properties. One is that---assuming we never reduce inside a lambda term, but only when redexes are present in the outermost level---the formulas generated by these transforms will always only have a single candidate redex to be reduced at any stage. In other words, the generated expressions dictate in what order the components from the original expressions will be evaluated. As it happens, the first transform above forces a *call-by-name* reduction order: assuming `M N` to be a redex, redexes inside `N` will be evaluated only after `N` has been substituted into `M`. And the second transform forces a *call-by-value* reduction order. These reduction orders will be forced no matter what the native reduction order of the interpreter is, just so long as we're only allowed to reduce redexes not underneath lambdas.
+
+Plotkin did important early work with CPS transforms, and they are now a staple of academic computer science. (See the end of his 1975 paper [Call-by-name, call-by-value, and the lambda-calculus](http://homepages.inf.ed.ac.uk/gdp/publications/cbn_cbv_lambda.pdf).)
+
+Here's another interesting fact about these transforms. Compare the translations for variables and applications in the call-by-value transform:
+
+       [x]     --> \k. k x
+       [M N]   --> \k. [M] (\m. [N] (\n. m n k))
+
+to the implementations we proposed for `unit` and `bind` when developing a Continuation monads, for example [here](/list_monad_as_continuation_monad). I'll relabel some of the variable names to help the comparison:
+
+       let cont_unit x = fun k -> k x
+       let cont_bind N M = fun k -> N (fun n -> M n k)
+
+The transform for `x` is just `cont_unit x`! And the transform for `M N` is, though not here exactly the same as `cont_bind N M`, quite reminiscent of it. (I don't yet know whether there's an easy and satisfying explanation of why these two are related as they are.) <!-- FIXME -->
+
+Doing CPS transforms by hand is very cumbersome. (Try it.) But you can leverage our lambda evaluator to help you out. Here's how to do it. From here on out, we'll be working with and extending the call-by-value CPS transform set out above:
+
+       let var = \x (\k. k x) in
+       let lam = \x_body (\k. k (\x. x_body x)) in
+       let app = \m n. (\k. m (\m. n (\n. m n k))) in
+       ...
+
+Then if you want to use [x], you'd write `var x`. If you want to use [\x. body], you'd write `lam (\x. BODY)`, where `BODY` is whatever [body] amounts to. If you want to use [m n], you'd write `app M N`, where M and N are whatever [m] and [n] amount to.
+
+To play around with this, you'll also want to help yourself to some primitives already in CPS form. (You won't want to rebuild everything again from scratch.) For a unary function like `succ`, you can take its primitive CPS analogue [succ] to be `\u. u (\a k. k (succ a))` (where `succ` in this expansion is the familiar non-CPS form of `succ`). Then for example:
+
+       [succ x]
+                 = \k. [succ] (\m. [x] (\n. m n k))
+               ~~> ...
+               ~~> \k. k (succ x)
+
+Or, using the lambda evaluator, that is:
+
+       ...
+       let op1 = \op. \u. u (\a k. k (op a)) in
+       app (op1 succ) (var x)
+       ~~> \k. k (succ x)
+
+Some other handy tools:
+
+       let app2 = \a b c. app (app a b) c in
+       let app3 = \a b c d. app (app (app a b) c) d in
+       let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
+       let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
+       ...
+
+Then, for instance, [plus x y] would be rendered in the lambda evaluator as:
+
+       app2 (op2 plus) (var x) (var y)
+       ~~> \k. k (plus x y)
+
+To finish off a CPS computation, you have to supply it with an "initial" or "outermost" continuation. (This is somewhat like "running" a monadic computation.) Usually you'll give the identity function, representing that nothing further happens to the continuation-expecting value.
+
+If the program you're working with is already in CPS form, then some elegant and powerful computational patterns become available, as we've been seeing. But it's tedious to convert to and work in fully-explicit CPS form. Usually you'll just want to be using the power of continuations at some few points in your program. It'd be nice if we had some way to make use of those patterns without having to convert our code explicitly into CPS form.
+
+Callcc
+======
+
+Well, we can. Consider the space of lambda formulas. Consider their image under a CPS transform. There will be many well-formed lambda expressions not in that image---that is, expressions that aren't anybody's CPS transform. Some of these will be useful levers in the CPS patterns we want to make use of. We can think of them as being the CPS transforms of some new syntax in the original language. For example, the expression `callcc` is explained as a new bit of syntax having some of that otherwise unclaimed CPS real-estate. The meaning of the new syntax can be understood in terms of how the CPS transform we specify for it behaves, when the whole language is in CPS form.
+
+I won't give the CPS transform for `callcc` itself, but instead for the complex form:
+
+       [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
+
+The behavior of `callcc` is this. The whole expression `callcc (\k. body)`, call it C, is being evaluated in a context, call it E[\_]. When we convert to CPS form, the continuation of this occurrence of C will be bound to the variable `outk`. What happens then is that we bind the expression `\v localk. outk v` to the variable `k` and evaluate [body], passing through to it the existing continuation `outk`. Now if `body` is just, for example, `x`, then its CPS transform [x] will be `\j. j x` and this will accept the continuation `outk` and feed it `x`, and we'll continue on with nothing unusual occurring. If on the other hand `body` makes use of the variable `k`, what happens then? For example, suppose `body` includes `foo (k v)`. In the reduction of the CPS transform `[foo (k v)]`, `v` will be passed to `k` which as we said is now `\v localk. outk v`. The continuation of that application---what is scheduled to happen to `k v` after it's evaluated and `foo` gets access to it---will be bound next to `localk`. But notice that this `localk` is discarded. The computation goes on without it. Instead, it just continues evaluating `outk v`, where as we said `outk` is the outside continuation E[\_] of the whole `callcc (\k. body)` invocation.
+
+So in other words, since the continuation in which `foo` was to be applied to the value of `k v` was discarded, that application never gets evaluated. We escape from that whole block of code.
+
+It's important to understand that `callcc` binds `k` to a pipe into the continuation as still then installed. Not just to a function that performs the same computation as the context E[\_] does---that has the same normal form and extension. But rather, a pipe into E[\_] *in its continuation-playing role*. This is manifested by the fact that when `k v` finishes evaluating, that value is not delivered to `foo` for the computation to proceed. Instead, when `k v` finishes evaluating, the program will then be done. Not because of some "stop here" block attached to `k`, but rather because of what it is that `k` represents. Walking through the explanation above several times may help you understand this better.
+
+So too will examples. We'll give some examples, and show you how to try them out in a variety of formats:
+
+1.     using the lambda evaluator to check how the CPS transforms reduce
+
+       To do this, you can use the following helper function:
+
+               let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
+               ...
+
+       Used like this: [callcc (\k. body)] = `callcc (\k. BODY)`, where `BODY` is [body].
+
+2.     using a `callcc` operation on our Continuation monad
+
+       This is implemented like this:
+
+               let callcc body = fun outk -> body (fun v localk -> outk v) outk
+
+       <!-- GOTCHAS?? -->
+
+-- cutting for control operators --
+
+3.     `callcc` was originally introduced in Scheme. There it's written `call/cc` and is an abbreviation of `call-with-current-continuation`. Instead of the somewhat bulky form:
+
+               (call/cc (lambda (k) ...))
+
+       I prefer instead to use the lighter, and equivalent, shorthand:
+
+               (let/cc k ...)
+
+
+Callcc/letcc examples
+---------------------
+
+First, here are two examples in Scheme:
+
+       (+ 100 (let/cc k (+ 10 1)))
+              |-----------------|
+
+This binds the continuation `outk` of the underlined expression to `k`, then computes `(+ 10 1)` and delivers that to `outk` in the normal way (not through `k`). No unusual behavior. It evaluates to `111`.
+
+
+       (+ 100 (let/cc k (+ 10 (k 1))))
+              |---------------------|
+
+This time, during the evaluation of `(+ 10 (k 1))`, we supply `1` to `k`. So then the local continuation, which delivers the value up to `(+ 10 [_])` and so on, is discarded. Instead `1` gets supplied to the outer continuation in place when `let/cc` was invoked. That will be `(+ 100 [_])`. When `(+ 100 1)` is evaluated, there's no more of the computation left to evaluate. So the answer here is `101`.
+
+You are not restricted to calling a bound continuation only once, nor are you restricted to calling it only inside of the `call/cc` (or `let/cc`) block. For example, you can do this:
+
+       (let ([p (let/cc k (cons 1 k))])
+         (cons (car p) ((cdr p) (cons 2 (lambda (x) x)))))
+       ; evaluates to '(2 2 . #<procedure>)
+
+What happens here? First, we capture the continuation where `p` is about to be assigned a value. Inside the `let/cc` block, we create a pair consisting of `1` and the captured continuation. This pair is bound to p. We then proceed to extract the components of the pair. The head (`car`) goes into the start of a tuple we're building up. To get the next piece of the tuple, we extract the second component of `p` (this is the bound continuation `k`) and we apply it to a pair consisting of `2` and the identity function. Supplying arguments to `k` takes us back to the point where `p` is about to be assigned a value. The tuple we had formerly been building, starting with `1`, will no longer be accessible because we didn't bring along with us any way to refer to it, and we'll never get back to the context where we supplied an argument to `k`. Now `p` gets assigned not the result of `(let/cc k (cons 1 k))` again, but instead, the new pair that we provided: `'(2 . #<identity procedure>)`. Again we proceed to build up a tuple: we take the first element `2`, then we take the second element (now the identity function), and feed it a pair `'(2 . #<identity procedure>)`, and since it's an argument to the identity procedure that's also the result. So our final result is a nested pair, whose first element is `2` and whose second element is the pair `'(2 . #<identity procedure>)`. Racket displays this nested pair like this:
+
+       '(2 2 . #<procedure>)
+
+-- end of cut --
+
+Ok, so now let's see how to perform these same computations via CPS.
+
+In the lambda evaluator:
+
+       let var = \x (\k. k x) in
+       let lam = \x_body (\k. k (\x. x_body x)) in
+       let app = \m n. (\k. m (\m. n (\n. m n k))) in
+       let app2 = \a b c. app (app a b) c in
+       let app3 = \a b c d. app (app (app a b) c) d in
+       let op1 = \op. \u. u (\a k. k (op a)) in
+       let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
+       let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
+       let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
+
+       ; (+ 100 (let/cc k (+ 10 1))) ~~> 111
+       app2 (op2 plus) (var hundred) (callcc (\k. app2 (op2 plus) (var ten) (var one)))
+       ; evaluates to \k. k (plus hundred (plus ten one))
+
+Next:
+
+       ; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101
+       app2 (op2 plus) (var hundred) (callcc (\k. app2 (op2 plus) (var ten) (app (var k) (var one))))
+       ; evaluates to \k. k (plus hundred one)
+
+We won't try to do the third example in this framework.
+
+Finally, using the Continuation monad from our OCaml monad library. We begin:
+
+       # module C = Continuation_monad;;
+
+Now what we want to do is something like this:
+
+       # C.(run0 (100 + callcc (fun k -> 10 + 1)));;
+
+`run0` is a special function in the Continuation monad that runs a value of that monad using the identity function as its initial continuation. The above expression won't type-check, for several reasons. First, we're trying to add 100 to `callcc (...)` but the latter is a `Continuation.m` value, not an `int`. So we have to do this instead:
+
+       # C.(run0 (callcc (fun k -> 10 + 1) >>= fun i -> 100 + i));;
+
+Except that's still no good, because `10 + 1` and `100 + i` are of type `int`, but their context demands Continuation monadic values. So we have to throw in some `unit`s:
+
+       # C.(run0 (callcc (fun k -> unit (10 + 1)) >>= fun i -> unit (100 + i)));;
+       - : int = 111
+
+This works and as you can see, delivers the same answer `111` that we got by the other methods.
+
+Next we try:
+
+       # C.(run0 (callcc (fun k -> unit (10 + (k 1))) >>= fun i -> unit (100 + i)));;
+
+That won't work because `k 1` doesn't have type `int`, but we're trying to add it to `10`. So we have to do instead:
+
+       # C.(run0 (callcc (fun k -> k 1 >>= fun j -> unit (10 + j)) >>= fun i -> unit (100 + i)));;
+       - : int = 101
+
+This also works and as you can see, delivers the expected answer `101`.
+
+The third example is more difficult to make work with the monadic library, because its types are tricky. I was able to get this to work, which uses OCaml's "polymorphic variants." These are generally more relaxed about typing. There may be a version that works with regular OCaml types, but I haven't yet been able to identify it. Here's what does work:
+
+       # C.(run0 (callcc (fun k -> unit (1,`Box k)) >>= fun (p1,`Box p2) -> p2 (2,`Box unit) >>= fun p2' -> unit (p1,p2')));;
+       - : int * (int * [ `Box of 'b -> ('a, 'b) C.m ] as 'b) as 'a =
+       (2, (2, `Box <fun>))
+
+<!-- FIXME -->
+
+-- cutting following section for control operators --
+
+Some callcc/letcc exercises
+---------------------------
+
+Here are a series of examples from *The Seasoned Schemer*, which we recommended at the start of term. It's not necessary to have the book to follow the exercises, though if you do have it, its walkthroughs will give you useful assistance.
+
+For reminders about Scheme syntax, see [here](/assignment8/) and [here](/week1/) and [here](/translating_between_ocaml_scheme_and_haskell). Other resources are on our [[Learning Scheme]] page.
+
+Most of the examples assume the following preface:
+
+       #lang racket
+
+       (define (atom? x)
+         (and (not (pair? x)) (not (null? x))))
+
+Now try to figure out what this function does:
+
+       (define alpha
+         (lambda (a lst)
+           (let/cc k ; now what will happen when k is called?
+             (letrec ([aux (lambda (l)
+                             (cond
+                               [(null? l) '()]
+                               [(eq? (car l) a) (k (aux (cdr l)))]
+                               [else (cons (car l) (aux (cdr l)))]))])
+               (aux lst)))))
+
+Here is [the answer](/hints/cps_hint_1), but try to figure it out for yourself.
+
+Next, try to figure out what this function does:
+
+       (define beta
+         (lambda (lst)
+           (let/cc k ; now what will happen when k is called?
+             (letrec ([aux (lambda (l)
+                             (cond
+                               [(null? l) '()]
+                               [(atom? (car l)) (k (car l))]
+                               [else (begin
+                                       ; what will the value of the next line be? why is it ignored?
+                                       (aux (car l))
+                                       (aux (cdr l)))]))])
+               (aux lst)))))
+
+Here is [the answer](/hints/cps_hint_2), but try to figure it out for yourself.
+
+Next, try to figure out what this function does:
+
+       (define gamma
+         (lambda (a lst)
+           (letrec ([aux (lambda (l k)
+                           (cond
+                             [(null? l) (k 'notfound)]
+                             [(eq? (car l) a) (cdr l)]
+                             [(atom? (car l)) (cons (car l) (aux (cdr l) k))]
+                             [else
+                              ; what happens when (car l) exists but isn't an atom?
+                              (let ([car2 (let/cc k2 ; now what will happen when k2 is called?
+                                            (aux (car l) k2))])
+                                (cond
+                                  ; when will the following condition be met? what happens then?
+                                  [(eq? car2 'notfound) (cons (car l) (aux (cdr l) k))]
+                                  [else (cons car2 (cdr l))]))]))]
+                    [lst2 (let/cc k1 ; now what will happen when k1 is called?
+                            (aux lst k1))])
+             (cond
+               ; when will the following condition be met?
+               [(eq? lst2 'notfound) lst]
+               [else lst2]))))
+
+Here is [the answer](/hints/cps_hint_3), but try to figure it out for yourself.
+
+Here is the hardest example. Try to figure out what this function does:
+
+       (define delta
+         (letrec ([yield (lambda (x) x)]
+                  [resume (lambda (x) x)]
+                  [walk (lambda (l)
+                          (cond
+                            ; is this the only case where walk returns a non-atom?
+                            [(null? l) '()]
+                            [(atom? (car l)) (begin
+                                               (let/cc k2 (begin
+                                                 (set! resume k2) ; now what will happen when resume is called?
+                                                 ; when the next line is executed, what will yield be bound to?
+                                                 (yield (car l))))
+                                               ; when will the next line be executed?
+                                               (walk (cdr l)))]
+                            [else (begin
+                                    ; what will the value of the next line be? why is it ignored?
+                                    (walk (car l))
+                                    (walk (cdr l)))]))]
+                  [next (lambda () ; next is a thunk
+                          (let/cc k3 (begin
+                            (set! yield k3) ; now what will happen when yield is called?
+                            ; when the next line is executed, what will resume be bound to?
+                            (resume 'blah))))]
+                  [check (lambda (prev)
+                           (let ([n (next)])
+                             (cond
+                               [(eq? n prev) #t]
+                               [(atom? n) (check n)]
+                               ; when will n fail to be an atom?
+                               [else #f])))])
+           (lambda (lst)
+             (let ([fst (let/cc k1 (begin
+                          (set! yield k1) ; now what will happen when yield is called?
+                          (walk lst)
+                          ; when will the next line be executed?
+                          (yield '())))])
+               (cond
+                 [(atom? fst) (check fst)]
+                 ; when will fst fail to be an atom?
+                 [else #f])
+               ))))
+
+Here is [the answer](/hints/cps_hint_4), but again, first try to figure it out for yourself.
+
+
+Delimited control operators
+===========================
+
+Here again is the CPS transform for `callcc`:
+
+       [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
+
+`callcc` is what's known as an *undelimited control operator*. That is, the continuations `outk` that get bound into our `k`s include all the code from the `call/cc ...` out to *and including* the end of the program. Calling such a continuation will never return any value to the call site.
+
+(See the technique employed in the `delta` example above, with the `(begin (let/cc k2 ...) ...)`, for a work-around. Also. if you've got a copy of *The Seasoned Schemer*, see the comparison of let/cc vs. "collector-using" (that is, partly CPS) functions at pp. 155-164.)
+
+Often times it's more useful to use a different pattern, where we instead capture only the code from the invocation of our control operator out to a certain boundary, not including the end of the program. These are called *delimited control operators*. A variety of these have been formulated. The most well-behaved from where we're coming from is the pair `reset` and `shift`. `reset` sets the boundary, and `shift` binds the continuation from the position where it's invoked out to that boundary.
+
+It works like this:
+
+       (1) outer code
+       ------- reset -------
+       | (2)               |
+       | +----shift k ---+ |
+       | | (3)           | |
+       | |               | |
+       | |               | |
+       | +---------------+ |
+       | (4)               |
+       +-------------------+
+       (5) more outer code
+
+First, the code in position (1) runs. Ignore position (2) for the moment. When we hit the `shift k`, the continuation between the `shift` and the `reset` will be captured and bound to `k`. Then the code in position (3) will run, with `k` so bound. The code in position (4) will never run, unless it's invoked through `k`. If the code in position (3) just ends with a regular value, and doesn't apply `k`, then the value returned by (3) is passed to (5) and the computation continues.
+
+So it's as though the middle box---the (2) and (4) region---is by default not evaluated. This code is instead bound to `k`, and it's up to other code whether and when to apply `k` to any argument. If `k` is applied to an argument, then what happens? Well it will be as if that were the argument supplied by (3) only now that argument does go to the code (4) syntactically enclosing (3). When (4) is finished, that value also goes to (5) (just as (3)'s value did when it ended with a regular value). `k` can be applied repeatedly, and every time the computation will traverse that same path from (4) into (5).
+
+I set (2) aside a moment ago. The story we just told is a bit too simple because the code in (2) needs to be evaluated because some of it may be relied on in (3).
+
+For instance, in Scheme this:
+
+       (require racket/control)
+
+       (reset
+        (let ([x 1])
+          (+ 10 (shift k x))))
+
+will return 1. The `(let ([x 1]) ...` part is evaluated, but the `(+ 10 ...` part is not.
+
+Notice we had to preface the Scheme code with `(require racket/control)`. You don't have to do anything special to use `call/cc` or `let/cc`; but to use the other control operators we'll discuss you do have to include that preface in Racket.
+
+This pattern should look somewhat familiar. Recall from our discussion of aborts, and repeated at the top of this page:
+
+       let foo x =
+       +---try begin----------------+
+       |       (if x = 1 then 10    |
+       |       else abort 20        |
+       |       ) + 100              |
+       +---end----------------------+
+       in (foo 2) + 1000;;
+
+The box is working like a reset. The `abort` is implemented with a `shift`. Earlier, we refactored our code into a more CPS form:
+
+       let x = 2
+       in let snapshot = fun box ->
+           let foo_result = box
+           in (foo_result) + 1000
+       in let continue_normally = fun from_value ->
+           let value = from_value + 100
+           in snapshot value
+       in
+           if x = 1 then continue_normally 10
+           else snapshot 20;;
+
+`snapshot` here corresponds to the code outside the `reset`. `continue_normally` is the middle block of code, between the `shift` and its surrounding `reset`. This is what gets bound to the `k` in our `shift`. The `if...` statement is inside a `shift`. Notice there that we invoke the bound continuation to "continue normally". We just invoke the outer continuation, saved in `snapshot` when we placed the `reset`, to skip the "continue normally" code and immediately abort to outside the box.
+
+
+-- end of cut --
+
+
+Using `shift` and `reset` operators in OCaml, this would look like this:
+
+       #require "delimcc";;
+       let p = Delimcc.new_prompt ();;
+       let reset = Delimcc.push_prompt p;;
+       let shift = Delimcc.shift p;;
+       let abort = Delimcc.abort p;;
+
+       let foo x =
+         reset(fun () ->
+           shift(fun continue ->
+               if x = 1 then continue 10
+               else 20
+           ) + 100
+         )
+       in foo 2 + 1000;;
+       - : int = 1020
+
+If instead at the end we did `... foo 1 + 1000`, we'd get the result `1110`.
+
+The above OCaml code won't work out of the box; you have to compile and install a special library that Oleg wrote. We discuss it on our [translation page](/translating_between_ocaml_scheme_and_haskell). If you can't get it working, then you can play around with `shift` and `reset` in Scheme instead. Or in the Continuation monad. Or using CPS transforms of your code, with the help of the lambda evaluator.
+
+You can make the lambda evaluator perform the required CPS transforms with these helper functions:
+
+       let reset = \body. \outk. outk (body (\i i)) in
+       let shift = \k_body. \midk. (\k. (k_body k) (\i i)) (\a localk. localk (midk a)) in
+       let abort = \body. \midk. body (\i i) in
+       ...
+
+You use these like so:
+
+*      [reset body] is `reset BODY` where `BODY` is [body]
+*      [shift k body] is `shift (\k. BODY)` where `BODY` is [body]
+*      and [abort value] is `abort VALUE` where `VALUE` is [value]
+
+There are also `reset` and `shift` and `abort` operations in the Continuation monad in our OCaml [[monad library]]. You can check the code for details.
+
+
+As we said, there are many varieties of delimited continuations. Another common pair is `prompt` and `control`. There's no difference in meaning between `prompt` and `reset`; it's just that people tend to say `reset` when talking about `shift`, and `prompt` when talking about `control`. `control` acts subtly differently from `shift`. In the uses you're likely to make as you're just learning about continuations, you won't see any difference. If you'll do more research in this vicinity, you'll soon enough learn about the differences.
+
+(You can start by reading [the Racket docs](http://docs.racket-lang.org/reference/cont.html?q=shift&q=do#%28part._.Classical_.Control_.Operators%29).)
+
+
+Ken Shan has done terrific work exploring the relations of `shift` and `control` and other control operators to each other.
+
+In collecting these CPS transforms and implementing the monadic versions, we've been helped by Ken and by Oleg and by these papers:
+
+*      Danvy and Filinski, "Representing control: a study of the CPS transformation" (1992)
+*      Sabry, "Note on axiomatizing the semantics of control operators" (1996)
+
+
+-- cutting some of the following for control operators --
+
+Examples of shift/reset/abort
+-----------------------------
+
+Here are some more examples of using delimited control operators. We present each example three ways: first a Scheme formulation; then we compute the same result using CPS and the lambda evaluator; then we do the same using the Continuation monad in OCaml. (We don't demonstrate the use of Oleg's delimcc library.)
+
+
+Example 1:
+
+       ; (+ 1000 (+ 100 (abort 11))) ~~> 11
+
+       app2 (op2 plus) (var thousand)
+         (app2 (op2 plus) (var hundred) (abort (var eleven)))
+
+           abort 11 >>= fun i ->
+           unit (100+i) >>= fun j ->
+           unit (1000+j)));;
+       - : int = 11
+
+When no `reset` is specified, there's understood to be an implicit one surrounding the entire computation (but unlike in the case of `callcc`, you still can't capture up to *and including* the end of the computation). So it makes no difference if we say instead:
+
+           reset (
+             abort 11 >>= fun i ->
+             unit (100+i) >>= fun j ->
+             unit (1000+j))));;
+       - : int = 11
+
+
+Example 2:
+
+       ; (+ 1000 (reset (+ 100 (abort 11)))) ~~> 1011
+
+       app2 (op2 plus) (var thousand)
+         (reset (app2 (op2 plus) (var hundred) (abort (var eleven))))
+
+           reset (
+             abort 11 >>= fun i ->
+             unit (100+i)
+           ) >>= fun j ->
+           unit (1000+j)));;
+       - : int = 1011
+
+Example 3:
+
+       ; (+ 1000 (reset (+ 100 (shift k (+ 10 1))))) ~~> 1011
+
+       app2 (op2 plus) (var thousand)
+         (reset (app2 (op2 plus) (var hundred)
+           (shift (\k. ((op2 plus) (var ten) (var one))))))
+
+         let v = reset (
+           let u = shift (fun k -> unit (10 + 1))
+           in u >>= fun x -> unit (100 + x)
+         ) in let w = v >>= fun x -> unit (1000 + x)
+         in run0 w);;
+       - : int = 1011
+
+Example 4:
+
+       ; (+ 1000 (reset (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111
+
+       app2 (op2 plus) (var thousand)
+         (reset (app2 (op2 plus) (var hundred)
+           (shift (\k. (app (var k) ((op2 plus) (var ten) (var one)))))))
+
+         let v = reset (
+           let u = shift (fun k -> k (10 :: ))
+           in u >>= fun x -> unit (100 :: x)
+         ) in let w = v >>= fun x -> unit (1000 :: x)
+         in run0 w);;
+       - : int list = [1000; 100; 10; 1]
+
+To demonstrate the different adding order between Examples 4 and 5, we use `::` in the OCaml version instead of `+`. Here is Example 5:
+
+       ; (+ 1000 (reset (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently
+
+       app2 (op2 plus) (var thousand)
+         (reset (app2 (op2 plus) (var hundred)
+           (shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
+
+       Continuation_monad.(let v = reset (
+           let u = shift (fun k -> k  >>= fun x -> unit (10 :: x))
+           in u >>= fun x -> unit (100 :: x)
+         ) in let w = v >>= fun x -> unit (1000 :: x)
+         in run0  w);;
+       - : int list = [1000; 10; 100; 1]
+
+
+Example 6:
+
+       ; (+ 100 ((reset (+ 10 (shift k k))) 1)) ~~> 111
+
+       app2 (op2 plus) (var hundred)
+         (app (reset (app2 (op2 plus) (var ten)
+           (shift (\k. (var k))))) (var one))
+
+       (* not sure if this example can be typed as-is in OCaml... this is the best I an do at the moment... *)
+
+       # type 'x either = Left of (int -> ('x,'x either) Continuation_monad.m) | Right of int;;
+       # Continuation_monad.(let v = reset (
+           shift (fun k -> unit (Left k)) >>= fun i -> unit (Right (10+i))
+         ) in let w = v >>= fun (Left k) ->
+             k 1 >>= fun (Right i) ->
+             unit (100+i)
+         in run0 w);;
+       - : int = 111
+
+<!--
+# type either = Left of (int -> either) | Right of int;;
+# let getleft e = match e with Left lft -> lft | Right _ -> failwith "not a Left";;
+# let getright e = match e with Right rt -> rt | Left _ -> failwith "not a Right";;
+# 100 + getright (let v = reset (fun p () -> Right (10 + shift p (fun k -> Left k))) in getleft v 1);;
+-->
+
+Example 7:
+
+       ; (+ 100 (reset (+ 10 (shift k (k (k 1)))))) ~~> 121
+
+       app2 (op2 plus) (var hundred)
+         (reset (app2 (op2 plus) (var ten)
+           (shift (\k. app (var k) (app (var k) (var one))))))
+
+       Continuation_monad.(let v = reset (
+           let u = shift (fun k -> k 1 >>= fun x -> k x)
+           in u >>= fun x -> unit (10 + x)
+         ) in let w = v >>= fun x -> unit (100 + x)
+         in run0 w)
+       - : int = 121
+
+<!--
+
+       print_endline "=== pa_monad's Continuation Tests ============";;
+
+       (1, 5 = C.(run0 (unit 1 >>= fun x -> unit (x+4))) );;
+       (2, 9 = C.(run0 (reset (unit 5 >>= fun x -> unit (x+4)))) );;
+       (3, 9 = C.(run0 (reset (abort 5 >>= fun y -> unit (y+6)) >>= fun x -> unit (x+4))) );;
+       (4, 9 = C.(run0 (reset (reset (abort 5 >>= fun y -> unit (y+6))) >>= fun x -> unit (x+4))) );;
+       (5, 27 = C.(run0 (
+                                 let c = reset(abort 5 >>= fun y -> unit (y+6))
+                                 in reset(c >>= fun v1 -> abort 7 >>= fun v2 -> unit (v2+10) ) >>= fun x -> unit (x+20))) );;
+
+       (7, 117 = C.(run0 (reset (shift (fun sk -> sk 3 >>= sk >>= fun v3 -> unit (v3+100) ) >>= fun v1 -> unit (v1+2)) >>= fun x -> unit (x+10))) );;
+
+       (8, 115 = C.(run0 (reset (shift (fun sk -> sk 3 >>= fun v3 -> unit (v3+100)) >>= fun v1 -> unit (v1+2)) >>= fun x -> unit (x+10))) );;
+
+       (12, ["a"] = C.(run0 (reset (shift (fun f -> f [] >>= fun t -> unit ("a"::t)  ) >>= fun xv -> shift (fun _ -> unit xv)))) );;
+
+
+       (0, 15 = C.(run0 (let f k = k 10 >>= fun v-> unit (v+100) in reset (callcc f >>= fun v -> unit (v+5)))) );;
+
+-->