cps continue
[lambda.git] / cps_and_continuation_operators.mdwn
1 [[!toc]]
2
3 CPS Transforms
4 ==============
5
6 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.
7
8 In our discussion of aborts, we showed how to rearrange code like this:
9
10
11         let foo x =
12         +---try begin----------------+
13         |       (if x = 1 then 10    |
14         |       else abort 20        |
15         |       ) + 100              |
16         +---end----------------------+
17         in (foo 2) + 1000;;
18
19 into a form like this:
20
21         let x = 2
22         in let snapshot = fun box ->
23             let foo_result = box
24             in (foo_result) + 1000
25         in let continue_normally = fun from_value ->
26             let value = from_value + 100
27             in snapshot value
28         in
29             if x = 1 then continue_normally 10
30             else snapshot 20;;
31
32 <!--
33 # #require "delimcc";;
34 # open Delimcc;;
35 # let reset body = let p = new_prompt () in push_prompt p (body p);;
36 # let test_cps x =
37       let snapshot = fun box ->
38           let foo_result = box
39           in (foo_result) + 1000
40       in let continue_normally = fun from_value ->
41           let value = from_value + 100
42           in snapshot value
43       in if x = 1 then continue_normally 10
44       else snapshot 20;;
45
46         let foo x =
47         +===try begin================+
48         |       (if x = 1 then 10    |
49         |       else abort 20        |
50         |       ) + 100              |
51         +===end======================+
52         in (foo 2) + 1000;;
53
54 # let test_shift x =
55     let foo x = reset(fun p () ->
56         (shift p (fun k ->
57             if x = 1 then k 10 else 20)
58         ) + 100)
59     in foo z + 1000;;
60
61 # test_cps 1;;
62 - : int = 1110
63 # test_shift 1;;
64 - : int = 1110
65 # test_cps 2;;
66 - : int = 1020
67 # test_shift 2;;
68 - : int = 1020
69 -->
70
71 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.
72
73 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.
74
75 In fact there are multiple ways to do a CPS transform. Here is one:
76
77         [x]     --> x
78         [\x. M] --> \k. k (\x. [M])
79         [M N]   --> \k. [M] (\m. m [N] k)
80
81 And here is another:
82
83         [x]     --> \k. k x
84         [\x. M] --> \k. k (\x. [M])
85         [M N]   --> \k. [M] (\m. [N] (\n. m n k))
86
87 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.
88
89 Plotkin did important early work with CPS transforms (around 1975), and they are now a staple of academic computer science.
90
91 Here's another interesting fact about these transforms. Compare the translations for variables and applications in the call-by-value transform:
92
93         [x]     --> \k. k x
94         [M N]   --> \k. [M] (\m. [N] (\n. m n k))
95
96 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:
97
98         let cont_unit x = fun k -> k x
99         let cont_bind M N = fun k -> M (fun m -> N m k)
100
101 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 M N`, quite reminiscent of it. (I don't yet know whether there's an easy and satisfying explanation of why these two diverge as they do.) <!-- FIXME -->
102
103 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:
104
105         let var = \x (\k. k x) in
106         let lam = \x_body (\k. k (\x. x_body x)) in
107         let app = \m n. (\k. m (\m. n (\n. m n k))) in
108         ...
109
110 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.
111
112 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:
113
114         [succ x]
115                   = \k. [succ] (\m. [x] (\n. m n k))
116                 ~~> ...
117                 ~~> \k. k (succ x)
118
119 Or, using the lambda evaluator, that is:
120
121         ...
122         let op1 = \op. \u. u (\a k. k (op a)) in
123         app (op1 succ) (var x)
124         ~~> \k. k (succ x)
125
126 Some other handy tools: 
127         let app3 = \a b c. app (app a b) c in
128         let app4 = \a b c d. app (app (app a b) c) d in
129         let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
130         let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
131         ...
132
133 Then, for instance, [plus x y] would be rendered in the lambda evaluator as:
134
135         app3 (op2 plus) (var x) (var y)
136         ~~> \k. k (plus x y)
137
138 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.
139
140 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.
141
142 Callcc
143 ======
144
145 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.
146
147 I won't give the CPS transform for `callcc` itself, but instead for the complex form:
148
149         [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
150
151 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 happens 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.
152
153 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.
154
155 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.
156
157 So too will examples. We'll give some examples, and show you how to try them out in a variety of formats:
158
159 (i)     using the lambda evaluator to check how the CPS transforms reduce
160
161         To do this, you can use the following helper function:
162
163                 let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
164                 ...
165
166         Used like this: [callcc (\k. body)] = `callcc (\k. BODY)`, where `BODY` is [body].
167
168 (ii) using a `callcc` operation on our Continuation monad
169
170         This is implemented like this:
171
172                 let callcc body = fun outk -> body (fun v localk -> outk v) outk
173
174         GOTCHAS??
175
176 (iii)   `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:
177
178         (call/cc (lambda (k) ...))
179
180 I prefer instead to use the lighter, and equivalent, shorthand:
181
182         (let/cc k ...)
183
184
185 Callcc examples
186 ---------------
187
188 First, here are two examples in Scheme:
189
190         (+ 100 (let/cc k (+ 10 1)))
191                |-----------------|
192
193 This binds the continuation `outk` of the underlined expression to `k`, the computes `(+ 10 1) and delivers that to `outk` in the normal way (not through `k`). No unusual behavior. It evaluates to `111.
194
195 Now if we do instead:
196
197         (+ 100 (let/cc k (+ 10 (k 1))))
198                |---------------------|
199
200 Now, 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`.
201
202 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:
203
204         (let ([p (let/cc k (cons 1 k))])
205           (cons (car p) ((cdr p) (cons 2 (lambda (x) x)))))
206         ; evaluates to '(2 2 . #<procedure>)
207
208 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 nest pair, whose first element is `2` and whose second element is the pair `'(2 . #<identity procedure>)`. Racket displays this nested pair like this:
209
210         '(2 2 . #<procedure>)
211
212 Ok, so now let's see how to perform these same computations via CPS.
213
214 In the lambda evaluator:
215
216         let var = \x (\k. k x) in
217         let lam = \x_body (\k. k (\x. x_body x)) in
218         let app = \m n. (\k. m (\m. n (\n. m n k))) in
219         let app3 = \a b c. app (app a b) c in
220         let app4 = \a b c d. app (app (app a b) c) d in
221         let op1 = \op. \u. u (\a k. k (op a)) in
222         let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
223         let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
224         let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
225
226         ; (+ 100 (let/cc k (+ 10 1))) ~~> 111
227         app3 (op2 plus) (var hundred) (callcc (\k. app3 (op2 plus) (var ten) (var one)))
228         ; evaluates to \k. k (plus hundred (plus ten one))
229
230 Next:
231
232         ; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101
233         app3 (op2 plus) (var hundred) (callcc (\k. app3 (op2 plus) (var ten) (app (var k) (var one))))
234         ; evaluates to \k. k (plus hundred one)
235
236 We won't try to do the third example in this framework.
237
238 Finally, using the Continuation monad from our OCaml monad library. We begin:
239
240         # #use "path/to/monads.ml"
241         # module C = Continuation_monad;;
242
243 Now what we want to do is something like this:
244
245         # C.(run0 (100 + callcc (fun k -> 10 + 1)));;
246
247 `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 typee-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:
248
249         # C.(run0 (callcc (fun k -> 10 + 1) >>= fun i -> 100 + i));;
250
251 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:
252
253         # C.(run0 (callcc (fun k -> unit (10 + 1)) >>= fun i -> unit (100 + i)));;
254         - : int = 111
255
256 This works and as you can see, delivers the same answer `111` that we got by the other methods.
257
258 Next we try:
259
260         # C.(run0 (callcc (fun k -> unit (10 + (k 1))) >>= fun i -> unit (100 + i)));;
261
262 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:
263
264         # C.(run0 (callcc (fun k -> k 1 >>= fun j -> unit (10 + j)) >>= fun i -> unit (100 + i)));;
265         - : int = 101
266
267 This also works and as you can see, delivers the expected answer `101`.
268
269 At the moment, I'm not able to get the third example working with the monadic library. I thought that this should do it, but it doesn't type-check:
270
271         # C.(run0 (callcc (fun k -> unit (1,k)) >>= fun (p1,p2) -> p2 (2,unit) >>= fun p2' -> unit (p1,p2')));;
272
273 If we figure this out later (or anyone else does), we'll come back and report. <!-- FIXME -->
274
275
276
277 Delimited control operators
278 ===========================
279
280 `callcc` is what's known as an *undelimited control operator*. That is, the continuations `outk` that get bound inside our `k`s behave as though they include all the code from the `call/cc ...` out to *and including* the end of the program.
281
282 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 the latter have been formulated.
283
284 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.
285
286 It works like this:
287
288         (1) outer code
289         ------- reset -------
290         | (2)               |
291         | +----shift k ---+ |
292         | | (3)           | |
293         | |               | |
294         | |               | |
295         | +---------------+ |
296         | (4)               |
297         +-------------------+
298         (5) more outer code
299
300 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.
301
302 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).
303
304 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).
305
306 For instance, in Scheme this:
307
308         (require racket/control)
309
310         (reset
311          (let ([x 1])
312            (+ 10 (shift k x))))
313
314 will return 1. The `(let ([x 1]) ...` part is evaluated, but the `(+ 10 ...` part is not.
315
316 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.
317
318 This pattern should look somewhat familiar. Recall from our discussion of aborts, and repeated at the top of this page:
319
320         let foo x =
321         +---try begin----------------+
322         |       (if x = 1 then 10    |
323         |       else abort 20        |
324         |       ) + 100              |
325         +---end----------------------+
326         in (foo 2) + 1000;;
327
328 The box is working like a reset. The `abort` is implemented with a `shift`. Earlier, we refactored our code into a more CPS form:
329
330         let x = 2
331         in let snapshot = fun box ->
332             let foo_result = box
333             in (foo_result) + 1000
334         in let continue_normally = fun from_value ->
335             let value = from_value + 100
336             in snapshot value
337         in
338             if x = 1 then continue_normally 10
339             else snapshot 20;;
340
341 `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.
342
343 Using `shift` and `reset` operators in OCaml, this would look like this:
344
345         #require "delimcc";;
346         let p = Delimcc.new_prompt ();;
347         let reset = Delimcc.push_prompt p;;
348         let shift = Delimcc.shift p;;
349         let abort = Delimcc.abort p;;
350
351         let foo x =
352           reset(fun () ->
353                 shift(fun continue ->
354                         if x = 1 then continue 10
355                         else 20
356                 ) + 100
357           )
358         in foo 2 + 1000;;
359         - : int = 1020
360
361 If instead at the end we did `in foo 1 + 1000`, we'd get the result `1110`.
362
363 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.
364
365 The relevant CPS transforms will be performed by these helper functions:
366
367         let reset = \body. \outk. outk (body (\i i)) in
368         let shift = \k_body. \midk. (\k. (k_body k) (\i i)) (\a localk. localk (midk a)) in
369         let abort = \body. \midk. body (\i i) in
370         ...
371
372 You use these like so:
373
374 *       [prompt m] is `prompt M` where `M` is [m]
375 *       [shift k M] is `shift (\k. M)` where `M` is [m]
376 *       and [abort M] is `abort M` where `M` is [m]
377         
378 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.
379
380
381 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.
382
383 (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).)
384
385
386 Ken Shan has done terrific work exploring the relations of `shift` and `control` and other control operators to each other.
387
388 In collecting these CPS transforms and implementing the monadic versions, we've been helped by Ken and by Oleg and by these papers:
389
390 *       Danvy and Filinski, "Representing control: a study of the CPS transformation" (1992)
391 *       Sabry, "Note on axiomatizing the semantics of control operators" (1996)
392
393
394 Examples of shift/reset/abort
395 -----------------------------
396
397 Here are some more examples of using delimited control operators. We present first a Scheme formulation; then we compute the same result using CPS and the lambda evaluator.
398
399
400         ; (+ 100 (+ 10 (abort 1))) ~~> 1
401         app3 (op2 plus) (var hundred)
402           (app3 (op2 plus) (var ten) (abort (var one)))
403
404         ; (+ 100 (prompt (+ 10 (abort 1)))) ~~> 101
405         app3 (op2 plus) (var hundred)
406           (prompt (app3 (op2 plus) (var ten) (abort (var one))))
407
408         ; (+ 1000 (prompt (+ 100 (shift k (+ 10 1))))) ~~> 1011
409         app3 (op2 plus) (var thousand)
410           (prompt (app3 (op2 plus) (var hundred)
411                 (shift (\k. ((op2 plus) (var ten) (var one))))))
412
413         ; (+ 1000 (prompt (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111
414         app3 (op2 plus) (var thousand)
415           (prompt (app3 (op2 plus) (var hundred)
416                 (shift (\k. (app (var k) ((op2 plus) (var ten) (var one)))))))
417
418         ; (+ 1000 (prompt (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently
419         app3 (op2 plus) (var thousand)
420           (prompt (app3 (op2 plus) (var hundred)
421                 (shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
422
423         ; (+ 100 ((prompt (+ 10 (shift k k))) 1)) ~~> 111
424         app3 (op2 plus) (var hundred)
425           (app (prompt (app3 (op2 plus) (var ten)
426                 (shift (\k. (var k))))) (var one))
427
428         ; (+ 100 (prompt (+ 10 (shift k (k (k 1)))))) ~~> 121
429         app3 (op2 plus) (var hundred)
430           (prompt (app3 (op2 plus) (var ten)
431                 (shift (\k. app (var k) (app (var k) (var one))))))
432
433
434 More:
435
436         (* (+ 1000 (prompt (+ 100 (shift k (+ 10 1))))) ~~> 1011 *)
437         let example1 () : int =
438           Continuation_monad.(let v = reset (
439                   let u = shift (fun k -> unit (10 + 1))
440                   in u >>= fun x -> unit (100 + x)
441                 ) in let w = v >>= fun x -> unit (1000 + x)
442                 in run w)
443
444         (* (+ 1000 (prompt (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111 *)
445         let example2 () =
446           Continuation_monad.(let v = reset (
447                   let u = shift (fun k -> k (10 :: [1]))
448                   in u >>= fun x -> unit (100 :: x)
449                 ) in let w = v >>= fun x -> unit (1000 :: x)
450                 in run w)
451
452         (* (+ 1000 (prompt (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently *)
453         let example3 () =
454           Continuation_monad.(let v = reset (
455                   let u = shift (fun k -> k [1] >>= fun x -> unit (10 :: x))
456                   in u >>= fun x -> unit (100 :: x)
457                 ) in let w = v >>= fun x -> unit (1000 :: x)
458                 in run w)
459
460         (* (+ 100 ((prompt (+ 10 (shift k k))) 1)) ~~> 111 *)
461         (* not sure if this example can be typed without a sum-type *)
462
463         (* (+ 100 (prompt (+ 10 (shift k (k (k 1)))))) ~~> 121 *)
464         let example5 () : int =
465           Continuation_monad.(let v = reset (
466                   let u = shift (fun k -> k 1 >>= fun x -> k x)
467                   in u >>= fun x -> unit (10 + x)
468                 ) in let w = v >>= fun x -> unit (100 + x)
469                 in run w)
470
471 More:
472
473         module C = Continuation_monad;;
474
475
476         print_endline "=== test TreeT(Continuation).distribute ==================";;
477
478         let id : 'z. 'z -> 'z = fun x -> x
479
480         let example n : (int * int) =
481           Continuation_monad.(let u = callcc (fun k ->
482                   (if n < 0 then k 0 else unit [n + 100])
483                   (* all of the following is skipped by k 0; the end type int is k's input type *)
484                   >>= fun [x] -> unit (x + 1)
485           )
486           (* k 0 starts again here, outside the callcc (...); the end type int * int is k's output type *)
487           >>= fun x -> unit (x, 0)
488           in run0 u)
489
490
491         (* (+ 1000 (prompt (+ 100 (shift k (+ 10 1))))) ~~> 1011 *)
492         let example1 () : int =
493           Continuation_monad.(let v = reset (
494                   let u = shift (fun k -> unit (10 + 1))
495                   in u >>= fun x -> unit (100 + x)
496                 ) in let w = v >>= fun x -> unit (1000 + x)
497                 in run0 w)
498
499         (* (+ 1000 (prompt (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111 *)
500         let example2 () =
501           Continuation_monad.(let v = reset (
502                   let u = shift (fun k -> k (10 :: [1]))
503                   in u >>= fun x -> unit (100 :: x)
504                 ) in let w = v >>= fun x -> unit (1000 :: x)
505                 in run0 w)
506
507         (* (+ 1000 (prompt (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently *)
508         let example3 () =
509           Continuation_monad.(let v = reset (
510                   let u = shift (fun k -> k [1] >>= fun x -> unit (10 :: x))
511                   in u >>= fun x -> unit (100 :: x)
512                 ) in let w = v >>= fun x -> unit (1000 :: x)
513                 in run0 w)
514
515         (* (+ 100 ((prompt (+ 10 (shift k k))) 1)) ~~> 111 *)
516         (* not sure if this example can be typed without a sum-type *)
517
518         (* (+ 100 (prompt (+ 10 (shift k (k (k 1)))))) ~~> 121 *)
519         let example5 () : int =
520           Continuation_monad.(let v = reset (
521                   let u = shift (fun k -> k 1 >>= k)
522                   in u >>= fun x -> unit (10 + x)
523                 ) in let w = v >>= fun x -> unit (100 + x)
524                 in run0 w)
525
526         ;;
527
528 More:
529
530         print_endline "=== test bare Continuation ============";;
531
532         (1011, 1111, 1111, 121);;
533         (example1(), example2(), example3(), example5());;
534         ((111,0), (0,0));;
535         (example ~+10, example ~-10);;
536
537
538         print_endline "=== pa_monad's Continuation Tests ============";;
539
540         (1, 5 = C.(run0 (unit 1 >>= fun x -> unit (x+4))) );;
541         (2, 9 = C.(run0 (reset (unit 5 >>= fun x -> unit (x+4)))) );;
542         (3, 9 = C.(run0 (reset (abort 5 >>= fun y -> unit (y+6)) >>= fun x -> unit (x+4))) );;
543         (4, 9 = C.(run0 (reset (reset (abort 5 >>= fun y -> unit (y+6))) >>= fun x -> unit (x+4))) );;
544         (5, 27 = C.(run0 (
545                                   let c = reset(abort 5 >>= fun y -> unit (y+6))
546                                   in reset(c >>= fun v1 -> abort 7 >>= fun v2 -> unit (v2+10) ) >>= fun x -> unit (x+20))) );;
547
548         (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))) );;
549
550         (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))) );;
551
552         (12, ["a"] = C.(run0 (reset (shift (fun f -> f [] >>= fun t -> unit ("a"::t)  ) >>= fun xv -> shift (fun _ -> unit xv)))) );;
553
554
555         (0, 15 = C.(run0 (let f k = k 10 >>= fun v-> unit (v+100) in reset (callcc f >>= fun v -> unit (v+5)))) );;
556