edits
[lambda.git] / topics / week14_continuations.mdwn
1 <!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
2
3 [[!toc]]
4
5 # Continuations
6
7 Last week we saw how to turn a list zipper into a continuation-based
8 list processor.  The function computed something we called "the task",
9 which was a simplified langauge involving control operators.
10
11     abSdS ~~> ababdS ~~> ababdababd
12
13 The task is to process the list from left to right, and at each "S",
14 double the list so far.  Here, "S" is a kind of control operator, and
15 captures the entire previous computation.  We also considered a
16 variant in which '#' delimited the portion of the list to be copied:
17
18     ab#deSfg ~~> abededfg
19
20 In this variant, "S" and "#" correspond to `shift` and `reset`, which
21 provide access to delimited continuations.
22
23 The expository logic of starting with this simplified task is the
24 notion that as lists are to trees, so is this task to full-blown
25 continuations.  So to the extent that, say, list zippers are easier to
26 grasp than tree zippers, the task is easier to grasp than full
27 continuations.
28
29 We then presented CPS transforms, and demonstrated how they provide
30 an order-independent analysis of order of evaluation.
31
32 In order to continue to explore continuations, we will proceed in the
33 following fashion: we introduce the traditional continuation monad,
34 and show how it solves the task, then generalize the task to 
35 include doubling of both the left and the right context.
36
37 ## The continuation monad
38
39 In order to build a monad, we start with a Kleisli arrow.
40
41     Continuation monad: types: given some ρ, Mα => (α -> ρ) -> ρ
42                         ⇧ == \ak.ka : a -> Ma
43                         bind == \ufk. u(\x.fxk)
44
45 We'll first show that this monad solves the task, then we'll consider
46 the monad in more detail.
47
48 The unmonadized computation (without the shifty "S" operator) is
49
50     t1 = + a (+ b (+ c d)) ~~> abcd
51
52 where "+" is string concatenation and the symbol a is shorthand for
53 the string "a".
54
55 In order to use the continuation monad to solve the list task,
56 we choose α = ρ = [Char].  So "abcd" is a list of characters, and
57 a boxed list has type M[Char] == ([Char] -> [Char]) -> [Char].
58
59 Writing ¢ in between its arguments, t1 corresponds to the following
60 monadic computation:
61
62     mt1 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ ⇧c ¢ ⇧d))
63
64 We have to lift each functor (+) and each object (e.g., "b") into the
65 monad using mid (`⇧`), then combine them using monadic function
66 application, where
67
68     ¢ M N = \k -> M (\f -> N (\a -> k(f x)))
69
70 for the continuation monad.
71
72 The way in which we extract a value from a continuation box is by
73 applying it to a continuation; often, it is convenient to supply the
74 trivial continuation, the identity function \k.k = I.  So in fact, 
75
76     t1 = mt1 I
77
78 That is, the original computation is the monadic version applied to
79 the trivial continuation.
80
81 We can now add a shifty operator.  We would like to replace just the
82 one element, and we will do just that in a moment; but in order to
83 simulate the original task, we'll have to take a different strategy
84 initially.  We'll start by imagining a shift operator that combined
85 direction with the tail of the list, like this:
86
87     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
88
89 We can now define a shift operator to perform the work of "S":
90
91     shift u k = u(\s.k(ks))
92
93 Shift takes two arguments: a string continuation u of type M[Char],
94 and a string continuation k of type [Char] -> [Char].  Since u is the
95 the argument to shift, it represents the tail of the list after the
96 shift operator.  Then k is the continuation of the expression headed
97 by `shift`.  So in order to execute the task, shift needs to invoke k
98 twice.  The expression `\s.k(ks)` is just the composition of k with itself.
99
100     mt2 I == "ababd"
101
102 just as desired.
103
104 Let's just make sure that we have the left-to-right evaluation we were
105 hoping for by evaluating "abSdeSf":
106
107     mt3 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ (⇧+ ¢ ⇧d ¢ (⇧+ ¢ ⇧e ¢ (shift ⇧f)))))
108
109 Then
110
111     mt3 I = "ababdeababdef"   -- structure: (ababde)(ababde)f
112              
113
114 As expected.
115
116 For a reset operator #, we can have 
117
118     # u k = k(u(\k.k))   -- ex.: ab#deSf ~~> abdedef
119
120 The reset operator executes the remainder of the list separately, by
121 giving it the trivial continuation (\k.k), then feeds the result to
122 the continuation corresponding to the position of the reset.
123
124 So the continuation monad solves the list task using continuations in
125 a way that conforms to our by-now familiar strategy of lifting a
126 computation into a monad, and then writing a few key functions (shift,
127 reset) that exploit the power of the monad.
128
129 ## Generalizing to the tree doubling task
130
131 Now we should consider what happens when we write a shift operator
132 that takes the place of a single letter.
133
134     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
135     mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d))
136
137 Instead of mt2 (copied from above), we have mt4.  So now the type of a
138 leaf (a boxed string, type M[Char]) is the same as the type of the new
139 shift operator, shift'.
140
141     shift' = \k.k(k"")
142
143 This shift operator takes a continuation k of type [Char]->[Char], and
144 invokes it twice.  Since k requires an argument of type [Char], we
145 need to use the first invocation of k to construction a [Char]; we do
146 this by feeding it a string.  Since the task does not replace the
147 shift operator with any marker, we give the empty string "" as the
148 argument.
149
150 But now the new shift operator captures more than just the preceeding
151 part of the construction---it captures the entire context, including
152 the portion of the sequence that follows it.  That is,
153
154     mt4 I = "ababdd"
155
156 We have replaced "S" in "abSd" with "ab_d", where the underbar will be
157 replaced with the empty string supplied in the definition of shift'.
158 Crucially, not only is the prefix "ab" duplicated, so is the suffix
159 "d".
160
161 Things get interesting when we have more than one operator in the
162 initial list.  What should we expect if we start with "aScSe"?
163 If we assume that when we evaluate each S, all the other S's become
164 temporarily inert, we expect a reduction path like
165
166     aScSe ~~> aacSecSe
167
168 But note that the output has just as many S's as the input--if that is
169 what our reduction strategy delivers, then any initial string with
170 more than one S will never reach a normal form.
171
172 But that's not what the continuation operator shift' delivers.
173
174     mt5 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ (⇧+ ¢ ⇧c ¢ (⇧+ ¢ shift' ¢ "e")))
175
176     mt5 I = "aacaceecaacaceecee" -- structure: "aacaceecaacaceecee"
177
178 Huh?
179
180 This is considerably harder to understand than the original list task.
181 The key is figuring out in each case what function the argument k to
182 the shift operator gets bound to.
183
184 Let's go back to a simple one-shift example, "aSc".  Let's trace what
185 the shift' operator sees as its argument k by replacing ⇧ and ¢ with
186 their definitions:
187
188 <pre>
189       ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ ⇧c) I
190    = \k.⇧+(\f.⇧a(\x.k(fx))) ¢ (⇧+ ¢ shift' ¢ ⇧c) I
191    = \k.(\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.k(fx))) I
192    ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.I(fx))) 
193    ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(f)) 
194    ~~> ⇧+(\f.⇧a(\x.(\f.(⇧+ ¢ shift' ¢ ⇧c)(f))(fx)))) 
195    ~~> ⇧+(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx)))
196    = (\k.k+)(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx)))
197    ~~> ⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x))
198    = (\k.ka)(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x))
199    ~~> (⇧+ ¢ shift' ¢ ⇧c)(+a)
200    = (\k.⇧+(\f.shift(\x.k(fx)))) ¢ ⇧c (+a)
201    = (\k.(\k.⇧+(\f.shift(\x.k(fx))))(\f.⇧c(\x.k(fx))))(+a)
202    ~~> (\k.⇧+(\f.shift(\x.k(fx))))(\f'.⇧c(\x'.(+a)(f'x')))
203    ~~> ⇧+(\f.shift(\x.(\f'.⇧c(\x'.(+a)(f'x')))(fx)))
204    ~~> ⇧+(\f.shift(\x.⇧c(\x'.(+a)((fx)x'))))
205    = (\k.k+)(\f.shift(\x.⇧c(\x'.(+a)((fx)x'))))
206    ~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
207    = shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
208    ~~> shift(\x.(+a)((+x)c))
209 </pre>
210
211 So now we see what the argument of shift will be: a function k from
212 strings x to the string asc.  So shift k will be k(k "") = aacc.
213
214 Ok, this is ridiculous.  We need a way to get ahead of this deluge of
215 lambda conversion.  We'll see how to understand what is going on
216 when we talk about quantifier raising in the next lecture.
217
218 ## Viewing Montague's PTQ as CPS
219
220 Montague's conception of determiner phrases as generalized quantifiers
221 is a limited form of continuation-passing.  (See, e.g., chapter 4 of
222 Barker and Shan 2014.)  Start by assuming that ordinary DPs such as
223 proper names denote objects of type `e`.  Then verb phrases denote
224 functions from individuals to truth values, i.e., functions of type `e
225 -> t`.
226
227 The meaning of extraordinary DPs such as *every woman* or *no dog*
228 can't be expressed as a simple individual.  As Montague argued, it
229 works much better to view them as predicates on verb phrase meanings,
230 i.e., as having type `(e->t)->t`.  Then *no woman left* is true just
231 in case the property of leaving is true of no woman:
232
233     no woman:  \k.not \exists x . (woman x) & kx
234     left: \x.left x
235     (no woman) (left) = not \exists x . woman x & left x
236
237 Montague also proposed that all determiner phrases should have the
238 same type.  After all, we can coordinate proper names with
239 quantificational DPs, as in *John and no dog left*.  Then generalized
240 quantifier corresponding to the proper name *John* is the quantifier
241 `\k.kj`.
242
243 ## How continuations can simulate other monads
244
245 Because the continuation monad allows the result type ρ to be any
246 type, we can choose ρ in clever ways that allow us to simulate other
247 monads.
248
249     Reader: ρ = env -> α
250     State: ρ = s -> (α, s)
251     Maybe: ρ = Just α | Nothing
252
253 You see how this is going to go.  Let's see an example by adding an
254 abort operator to our task language, which represents what
255 we want to have happen if we divide by zero, where what we want to do
256 is return Nothing.
257
258     abort k = Nothing
259     mid a k = k a
260     map2 f u v k = u(\u' -> v (\v' -> k(f u' v'))) 
261     t13 = map2 (++) (mid "a")
262                    (map2 (++) (mid "b")
263                               (map2 (++) (mid "c")
264                                          (mid "d")))
265
266     t13 (\k->Just k) == Just "abcd"
267
268     t14 = map2 (++) (mid "a")
269                    (map2 (++) abort
270                               (map2 (++) (mid "c")
271                                          (mid "d")))
272
273
274     t14 (\k->Just k) == Nothing
275
276 Super cool.
277
278 ## Continuation Passing Style Transforms
279
280 Gaining control over order of evaluation
281 ----------------------------------------
282
283 We know that evaluation order matters.  We're beginning to learn how
284 to gain some control over order of evaluation (think of Jim's abort handler).
285 We continue to reason about order of evaluation.
286
287 A lucid discussion of evaluation order in the
288 context of the lambda calculus can be found here:
289 [Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
290 Sestoft also provides a lovely on-line lambda evaluator:
291 [Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
292 which allows you to select multiple evaluation strategies, 
293 and to see reductions happen step by step.
294
295 Evaluation order matters
296 ------------------------
297
298 We've seen this many times.  For instance, consider the following
299 reductions.  It will be convenient to use the abbreviation `w =
300 \x.xx`.  I'll
301 indicate which lambda is about to be reduced with a * underneath:
302
303 <pre>
304 (\x.y)(ww)
305  *
306 y
307 </pre>
308
309 Done!  We have a normal form.  But if we reduce using a different
310 strategy, things go wrong:
311
312 <pre>
313 (\x.y)(ww) =
314 (\x.y)((\x.xx)w) =
315         *
316 (\x.y)(ww) =
317 (\x.y)((\x.xx)w) =
318         *
319 (\x.y)(ww) 
320 </pre>
321
322 Etc.  
323
324 As a second reminder of when evaluation order matters, consider using
325 `Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:
326
327 <pre>
328 Y (\f n. blah) =
329 (\f.(\h.f(hh))(\h.f(hh))) (\f n. blah) 
330      *
331 (\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah) 
332        *
333 (\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah) 
334          *
335 (\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah) 
336 </pre>
337
338 And we never get the recursion off the ground.
339
340
341 Using a Continuation Passing Style transform to control order of evaluation
342 ---------------------------------------------------------------------------
343
344 We'll present a technique for controlling evaluation order by transforming a lambda term
345 using a Continuation Passing Style transform (CPS), then we'll explore
346 what the CPS is doing, and how.
347
348 In order for the CPS to work, we have to adopt a new restriction on
349 beta reduction: beta reduction does not occur underneath a lambda.
350 That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to
351 `\u.z`, because the `\u` protects the redex in the body from
352 reduction.  (In this context, a "redex" is a part of a term that matches
353 the pattern `...((\xM)N)...`, i.e., something that can potentially be
354 the target of beta reduction.)
355
356 Start with a simple form that has two different reduction paths:
357
358 reducing the leftmost lambda first: `(\x.y)((\x.z)u)  ~~> y`
359
360 reducing the rightmost lambda first: `(\x.y)((\x.z)u)  ~~> (\x.y)z ~~> y`
361
362 After using the following call-by-name CPS transform---and assuming
363 that we never evaluate redexes protected by a lambda---only the first
364 reduction path will be available: we will have gained control over the
365 order in which beta reductions are allowed to be performed.
366
367 Here's the CPS transform defined:
368
369     [x] = x
370     [\xM] = \k.k(\x[M])
371     [MN] = \k.[M](\m.m[N]k)
372
373 Here's the result of applying the transform to our simple example:
374
375     [(\x.y)((\x.z)u)] =
376     \k.[\x.y](\m.m[(\x.z)u]k) =
377     \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
378     \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)
379
380 Because the initial `\k` protects (i.e., takes scope over) the entire
381 transformed term, we can't perform any reductions.  In order to watch
382 the computation unfold, we have to apply the transformed term to a
383 trivial continuation, usually the identity function `I = \x.x`.
384
385     [(\x.y)((\x.z)u)] I =
386     (\k.[\x.y](\m.m[(\x.z)u]k)) I
387      *
388     [\x.y](\m.m[(\x.z)u] I) =
389     (\k.k(\x.y))(\m.m[(\x.z)u] I)
390      *           *
391     (\x.y)[(\x.z)u] I           --A--
392      *
393     y I
394
395 The application to `I` unlocks the leftmost functor.  Because that
396 functor (`\x.y`) throws away its argument (consider the reduction in the
397 line marked (A)), we never need to expand the
398 CPS transform of the argument.  This means that we never bother to
399 reduce redexes inside the argument.
400
401 Compare with a call-by-value xform:
402
403     {x} = \k.kx
404     {\aM} = \k.k(\a{M})
405     {MN} = \k.{M}(\m.{N}(\n.mnk))
406
407 This time the reduction unfolds in a different manner:
408
409     {(\x.y)((\x.z)u)} I =
410     (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
411      *
412     {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
413     (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
414      *             *
415     {(\x.z)u}(\n.(\x.{y})nI) =
416     (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI)
417      *
418     {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
419     (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI)))
420      *             *
421     {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
422     (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
423      *      *
424     (\x.{z})u(\n.(\x.{y})nI)       --A--
425      *
426     {z}(\n.(\x.{y})nI) =
427     (\k.kz)(\n.(\x.{y})nI)
428      *      *
429     (\x.{y})zI
430      *
431     {y}I =
432     (\k.ky)I
433      *
434     I y
435
436 In this case, the argument does get evaluated: consider the reduction
437 in the line marked (A).
438
439 Both xforms make the following guarantee: as long as redexes
440 underneath a lambda are never evaluated, there will be at most one
441 reduction available at any step in the evaluation.
442 That is, all choice is removed from the evaluation process.
443
444 Now let's verify that the CBN CPS avoids the infinite reduction path
445 discussed above (remember that `w = \x.xx`):
446
447     [(\x.y)(ww)] I =
448     (\k.[\x.y](\m.m[ww]k)) I
449      *
450     [\x.y](\m.m[ww]I) =
451     (\k.k(\x.y))(\m.m[ww]I)
452      *             *
453     (\x.y)[ww]I
454      *
455     y I
456
457
458 Questions and exercises:
459
460 1. Prove that {(\x.y)(ww)} does not terminate.
461
462 2. Why is the CBN xform for variables `[x] = x` instead of something
463 involving kappas (i.e., `k`'s)?  
464
465 3. Write an Ocaml function that takes a lambda term and returns a
466 CPS-xformed lambda term.  You can use the following data declaration:
467
468     type form = Var of char | Abs of char * form | App of form * form;;
469
470 4. The discussion above talks about the "leftmost" redex, or the
471 "rightmost".  But these words apply accurately only in a special set
472 of terms.  Characterize the order of evaluation for CBN (likewise, for
473 CBV) more completely and carefully.
474
475 5. What happens (in terms of evaluation order) when the application
476 rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
477
478 6. A term and its CPS xform are different lambda terms.  Yet in some
479 sense they "do" the same thing computationally.  Make this sense
480 precise.
481
482
483 Thinking through the types
484 --------------------------
485
486 This discussion is based on [Meyer and Wand 1985](http://citeseer.ist.psu.edu/viewdoc/download?doi=10.1.1.44.7943&rep=rep1&type=pdf).
487
488 Let's say we're working in the simply-typed lambda calculus.
489 Then if the original term is well-typed, the CPS xform will also be
490 well-typed.  But what will the type of the transformed term be?
491
492 The transformed terms all have the form `\k.blah`.  The rule for the
493 CBN xform of a variable appears to be an exception, but instead of
494 writing `[x] = x`, we can write `[x] = \k.xk`, which is
495 eta-equivalent.  The `k`'s are continuations: functions from something
496 to a result.  Let's use &sigma; as the result type.  The each `k` in
497 the transform will be a function of type &rho; --> &sigma; for some
498 choice of &rho;.
499
500 We'll need an ancilliary function ': for any ground type a, a' = a;
501 for functional types a->b, (a->b)' = ((a' -> &sigma;) -> &sigma;) -> (b' -> &sigma;) -> &sigma;.
502
503     Call by name transform
504
505     Terms                            Types
506
507     [x] = \k.xk                      [a] = (a'->o)->o
508     [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
509     [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o
510
511 Remember that types associate to the right.  Let's work through the
512 application xform and make sure the types are consistent.  We'll have
513 the following types:
514
515     M:a->b
516     N:a
517     MN:b 
518     k:b'->o
519     [N]:(a'->o)->o
520     m:((a'->o)->o)->(b'->o)->o
521     m[N]:(b'->o)->o
522     m[N]k:o 
523     [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
524     [M](\m.m[N]k):o
525     [MN]:(b'->o)->o
526
527 Be aware that even though the transform uses the same symbol for the
528 translation of a variable (i.e., `[x] = x`), in general the variable
529 in the transformed term will have a different type than in the source
530 term.
531
532 Excercise: what should the function ' be for the CBV xform?  Hint: 
533 see the Meyer and Wand abstract linked above for the answer.
534
535
536 Other CPS transforms
537 --------------------
538
539 It is easy to think that CBN and CBV are the only two CPS transforms.
540 (We've already seen a variant on call-by-value one of the excercises above.) 
541
542 In fact, the number of distinct transforms is unbounded.  For
543 instance, here is a variant of CBV that uses the same types as CBN:
544
545     <x> = x
546     <\xM> = \k.k(\x<M>)
547     <MN> = \k.<M>(\m.<N>(\n.m(\k.kn)k))
548
549 Try reducing `<(\x.x) ((\y.y) (\z.z))> I` to convince yourself that
550 this is a version of call-by-value.
551
552 Once we have two evaluation strategies that rely on the same types, we
553 can mix and match:
554
555     [x] = x
556     <x> = x
557     [\xM] = \k.k(\x<M>)
558     <\xM] = \k.k(\x[M])
559     [MN] = \k.<M>(\m.m<N>k)
560     <MN> = \k.[M](\m.[N](\n.m(\k.kn)k))
561
562 This xform interleaves call-by-name and call-by-value in layers,
563 according to the depth of embedding.
564 (Cf. page 4 of Reynold's 1974 paper ftp://ftp.cs.cmu.edu/user/jcr/reldircont.pdf (equation (4) and the
565 explanation in the paragraph below.)
566
567 CPS Transforms
568 ==============
569
570 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), 
571 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.
572
573 In our discussion of aborts, we showed how to rearrange code like this:
574
575
576         let foo x =
577         +---try begin----------------+
578         |       (if x = 1 then 10    |
579         |       else abort 20        |
580         |       ) + 100              |
581         +---end----------------------+
582         in (foo 2) + 1000;;
583
584 into a form like this:
585
586         let x = 2
587         in let snapshot = fun box ->
588             let foo_result = box
589             in (foo_result) + 1000
590         in let continue_normally = fun from_value ->
591             let value = from_value + 100
592             in snapshot value
593         in
594             if x = 1 then continue_normally 10
595             else snapshot 20;;
596
597 <!--
598 # #require "delimcc";;
599 # open Delimcc;;
600 # let reset body = let p = new_prompt () in push_prompt p (body p);;
601 # let test_cps x =
602       let snapshot = fun box ->
603           let foo_result = box
604           in (foo_result) + 1000
605       in let continue_normally = fun from_value ->
606           let value = from_value + 100
607           in snapshot value
608       in if x = 1 then continue_normally 10
609       else snapshot 20;;
610
611         let foo x =
612         +===try begin================+
613         |       (if x = 1 then 10    |
614         |       else abort 20        |
615         |       ) + 100              |
616         +===end======================+
617         in (foo 2) + 1000;;
618
619 # let test_shift x =
620     let foo x = reset(fun p () ->
621         (shift p (fun k ->
622             if x = 1 then k 10 else 20)
623         ) + 100)
624     in foo z + 1000;;
625
626 # test_cps 1;;
627 - : int = 1110
628 # test_shift 1;;
629 - : int = 1110
630 # test_cps 2;;
631 - : int = 1020
632 # test_shift 2;;
633 - : int = 1020
634 -->
635
636 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.
637
638 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.
639
640 In fact there are multiple ways to do a CPS transform. Here is one:
641
642         [x]     --> x
643         [\x. M] --> \k. k (\x. [M])
644         [M N]   --> \k. [M] (\m. m [N] k)
645
646 And here is another:
647
648         [x]     --> \k. k x
649         [\x. M] --> \k. k (\x. [M])
650         [M N]   --> \k. [M] (\m. [N] (\n. m n k))
651
652 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.
653
654 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).)
655
656 Here's another interesting fact about these transforms. Compare the translations for variables and applications in the call-by-value transform:
657
658         [x]     --> \k. k x
659         [M N]   --> \k. [M] (\m. [N] (\n. m n k))
660
661 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:
662
663         let cont_unit x = fun k -> k x
664         let cont_bind N M = fun k -> N (fun n -> M n k)
665
666 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 -->
667
668 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:
669
670         let var = \x (\k. k x) in
671         let lam = \x_body (\k. k (\x. x_body x)) in
672         let app = \m n. (\k. m (\m. n (\n. m n k))) in
673         ...
674
675 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.
676
677 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:
678
679         [succ x]
680                   = \k. [succ] (\m. [x] (\n. m n k))
681                 ~~> ...
682                 ~~> \k. k (succ x)
683
684 Or, using the lambda evaluator, that is:
685
686         ...
687         let op1 = \op. \u. u (\a k. k (op a)) in
688         app (op1 succ) (var x)
689         ~~> \k. k (succ x)
690
691 Some other handy tools: 
692
693         let app2 = \a b c. app (app a b) c in
694         let app3 = \a b c d. app (app (app a b) c) d in
695         let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
696         let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
697         ...
698
699 Then, for instance, [plus x y] would be rendered in the lambda evaluator as:
700
701         app2 (op2 plus) (var x) (var y)
702         ~~> \k. k (plus x y)
703
704 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.
705
706 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.
707
708 Callcc
709 ======
710
711 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.
712
713 I won't give the CPS transform for `callcc` itself, but instead for the complex form:
714
715         [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
716
717 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.
718
719 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.
720
721 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.
722
723 So too will examples. We'll give some examples, and show you how to try them out in a variety of formats:
724
725 1.      using the lambda evaluator to check how the CPS transforms reduce
726
727         To do this, you can use the following helper function:
728
729                 let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
730                 ...
731
732         Used like this: [callcc (\k. body)] = `callcc (\k. BODY)`, where `BODY` is [body].
733
734 2.      using a `callcc` operation on our Continuation monad
735
736         This is implemented like this:
737
738                 let callcc body = fun outk -> body (fun v localk -> outk v) outk
739
740         <!-- GOTCHAS?? -->
741
742 -- cutting for control operators --
743
744 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:
745
746                 (call/cc (lambda (k) ...))
747
748         I prefer instead to use the lighter, and equivalent, shorthand:
749
750                 (let/cc k ...)
751
752
753 Callcc/letcc examples
754 ---------------------
755
756 First, here are two examples in Scheme:
757
758         (+ 100 (let/cc k (+ 10 1)))
759                |-----------------|
760
761 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`.
762
763 What if we do instead:
764
765         (+ 100 (let/cc k (+ 10 (k 1))))
766                |---------------------|
767
768 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`.
769
770 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:
771
772         (let ([p (let/cc k (cons 1 k))])
773           (cons (car p) ((cdr p) (cons 2 (lambda (x) x)))))
774         ; evaluates to '(2 2 . #<procedure>)
775
776 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:
777
778         '(2 2 . #<procedure>)
779
780 -- end of cut --
781
782 Ok, so now let's see how to perform these same computations via CPS.
783
784 In the lambda evaluator:
785
786         let var = \x (\k. k x) in
787         let lam = \x_body (\k. k (\x. x_body x)) in
788         let app = \m n. (\k. m (\m. n (\n. m n k))) in
789         let app2 = \a b c. app (app a b) c in
790         let app3 = \a b c d. app (app (app a b) c) d in
791         let op1 = \op. \u. u (\a k. k (op a)) in
792         let op2 = \op. \u. u (\a v. v (\b k. k (op a b))) in
793         let op3 = \op. \u. u (\a v. v (\b w. w (\c k. k (op a b c)))) in
794         let callcc = \k_body. \outk. (\k. (k_body k) outk) (\v localk. outk v) in
795
796         ; (+ 100 (let/cc k (+ 10 1))) ~~> 111
797         app2 (op2 plus) (var hundred) (callcc (\k. app2 (op2 plus) (var ten) (var one)))
798         ; evaluates to \k. k (plus hundred (plus ten one))
799
800 Next:
801
802         ; (+ 100 (let/cc k (+ 10 (k 1)))) ~~> 101
803         app2 (op2 plus) (var hundred) (callcc (\k. app2 (op2 plus) (var ten) (app (var k) (var one))))
804         ; evaluates to \k. k (plus hundred one)
805
806 We won't try to do the third example in this framework.
807
808 Finally, using the Continuation monad from our OCaml monad library. We begin:
809
810         # #use "path/to/monads.ml"
811         # module C = Continuation_monad;;
812
813 Now what we want to do is something like this:
814
815         # C.(run0 (100 + callcc (fun k -> 10 + 1)));;
816
817 `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:
818
819         # C.(run0 (callcc (fun k -> 10 + 1) >>= fun i -> 100 + i));;
820
821 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:
822
823         # C.(run0 (callcc (fun k -> unit (10 + 1)) >>= fun i -> unit (100 + i)));;
824         - : int = 111
825
826 This works and as you can see, delivers the same answer `111` that we got by the other methods.
827
828 Next we try:
829
830         # C.(run0 (callcc (fun k -> unit (10 + (k 1))) >>= fun i -> unit (100 + i)));;
831
832 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:
833
834         # C.(run0 (callcc (fun k -> k 1 >>= fun j -> unit (10 + j)) >>= fun i -> unit (100 + i)));;
835         - : int = 101
836
837 This also works and as you can see, delivers the expected answer `101`.
838
839 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:
840
841         # C.(run0 (callcc (fun k -> unit (1,`Box k)) >>= fun (p1,`Box p2) -> p2 (2,`Box unit) >>= fun p2' -> unit (p1,p2')));;
842         - : int * (int * [ `Box of 'b -> ('a, 'b) C.m ] as 'b) as 'a =
843         (2, (2, `Box <fun>))
844
845 <!-- FIXME -->
846
847 -- cutting following section for control operators --
848
849 Some callcc/letcc exercises
850 ---------------------------
851
852 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.
853
854 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.
855
856 Most of the examples assume the following preface:
857
858         #lang racket
859
860         (define (atom? x)
861           (and (not (pair? x)) (not (null? x))))
862
863 Now try to figure out what this function does:
864
865         (define alpha
866           (lambda (a lst)
867             (let/cc k ; now what will happen when k is called?
868               (letrec ([aux (lambda (l)
869                               (cond
870                                 [(null? l) '()]
871                                 [(eq? (car l) a) (k (aux (cdr l)))]
872                                 [else (cons (car l) (aux (cdr l)))]))])
873                 (aux lst)))))
874         
875 Here is [the answer](/hints/cps_hint_1), but try to figure it out for yourself.
876
877 Next, try to figure out what this function does:
878
879         (define beta
880           (lambda (lst)
881             (let/cc k ; now what will happen when k is called?
882               (letrec ([aux (lambda (l)
883                               (cond
884                                 [(null? l) '()]
885                                 [(atom? (car l)) (k (car l))]
886                                 [else (begin
887                                         ; what will the value of the next line be? why is it ignored?
888                                         (aux (car l))
889                                         (aux (cdr l)))]))])
890                 (aux lst)))))
891
892 Here is [the answer](/hints/cps_hint_2), but try to figure it out for yourself.
893
894 Next, try to figure out what this function does:
895
896         (define gamma
897           (lambda (a lst)
898             (letrec ([aux (lambda (l k)
899                             (cond
900                               [(null? l) (k 'notfound)]
901                               [(eq? (car l) a) (cdr l)]
902                               [(atom? (car l)) (cons (car l) (aux (cdr l) k))]
903                               [else
904                                ; what happens when (car l) exists but isn't an atom?
905                                (let ([car2 (let/cc k2 ; now what will happen when k2 is called?
906                                              (aux (car l) k2))])
907                                  (cond
908                                    ; when will the following condition be met? what happens then?
909                                    [(eq? car2 'notfound) (cons (car l) (aux (cdr l) k))]
910                                    [else (cons car2 (cdr l))]))]))]
911                      [lst2 (let/cc k1 ; now what will happen when k1 is called?
912                              (aux lst k1))])
913               (cond
914                 ; when will the following condition be met?
915                 [(eq? lst2 'notfound) lst]
916                 [else lst2]))))
917
918 Here is [the answer](/hints/cps_hint_3), but try to figure it out for yourself.
919
920 Here is the hardest example. Try to figure out what this function does:
921
922         (define delta
923           (letrec ([yield (lambda (x) x)]
924                    [resume (lambda (x) x)]
925                    [walk (lambda (l)
926                            (cond
927                              ; is this the only case where walk returns a non-atom?
928                              [(null? l) '()]
929                              [(atom? (car l)) (begin
930                                                 (let/cc k2 (begin
931                                                   (set! resume k2) ; now what will happen when resume is called?
932                                                   ; when the next line is executed, what will yield be bound to?
933                                                   (yield (car l))))
934                                                 ; when will the next line be executed?
935                                                 (walk (cdr l)))]
936                              [else (begin
937                                      ; what will the value of the next line be? why is it ignored?
938                                      (walk (car l))
939                                      (walk (cdr l)))]))]
940                    [next (lambda () ; next is a thunk
941                            (let/cc k3 (begin
942                              (set! yield k3) ; now what will happen when yield is called?
943                              ; when the next line is executed, what will resume be bound to?
944                              (resume 'blah))))]
945                    [check (lambda (prev)
946                             (let ([n (next)])
947                               (cond
948                                 [(eq? n prev) #t]
949                                 [(atom? n) (check n)]
950                                 ; when will n fail to be an atom?
951                                 [else #f])))])
952             (lambda (lst)
953               (let ([fst (let/cc k1 (begin
954                            (set! yield k1) ; now what will happen when yield is called?
955                            (walk lst)
956                            ; when will the next line be executed?
957                            (yield '())))])
958                 (cond
959                   [(atom? fst) (check fst)]
960                   ; when will fst fail to be an atom?
961                   [else #f])
962                 ))))
963
964 Here is [the answer](/hints/cps_hint_4), but again, first try to figure it out for yourself.
965
966
967 Delimited control operators
968 ===========================
969
970 Here again is the CPS transform for `callcc`:
971
972         [callcc (\k. body)] = \outk. (\k. [body] outk) (\v localk. outk v)
973
974 `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.
975
976 (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.)
977
978 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.
979
980 It works like this:
981
982         (1) outer code
983         ------- reset -------
984         | (2)               |
985         | +----shift k ---+ |
986         | | (3)           | |
987         | |               | |
988         | |               | |
989         | +---------------+ |
990         | (4)               |
991         +-------------------+
992         (5) more outer code
993
994 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.
995
996 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).
997
998 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).
999
1000 For instance, in Scheme this:
1001
1002         (require racket/control)
1003         
1004         (reset
1005          (let ([x 1])
1006            (+ 10 (shift k x))))
1007
1008 will return 1. The `(let ([x 1]) ...` part is evaluated, but the `(+ 10 ...` part is not.
1009
1010 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.
1011
1012 This pattern should look somewhat familiar. Recall from our discussion of aborts, and repeated at the top of this page:
1013
1014         let foo x =
1015         +---try begin----------------+
1016         |       (if x = 1 then 10    |
1017         |       else abort 20        |
1018         |       ) + 100              |
1019         +---end----------------------+
1020         in (foo 2) + 1000;;
1021
1022 The box is working like a reset. The `abort` is implemented with a `shift`. Earlier, we refactored our code into a more CPS form:
1023
1024         let x = 2
1025         in let snapshot = fun box ->
1026             let foo_result = box
1027             in (foo_result) + 1000
1028         in let continue_normally = fun from_value ->
1029             let value = from_value + 100
1030             in snapshot value
1031         in
1032             if x = 1 then continue_normally 10
1033             else snapshot 20;;
1034
1035 `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.
1036
1037
1038 -- end of cut --
1039
1040
1041 Using `shift` and `reset` operators in OCaml, this would look like this:
1042
1043         #require "delimcc";;
1044         let p = Delimcc.new_prompt ();;
1045         let reset = Delimcc.push_prompt p;;
1046         let shift = Delimcc.shift p;;
1047         let abort = Delimcc.abort p;;
1048         
1049         let foo x =
1050           reset(fun () ->
1051             shift(fun continue ->
1052                 if x = 1 then continue 10
1053                 else 20
1054             ) + 100
1055           )
1056         in foo 2 + 1000;;
1057         - : int = 1020
1058
1059 If instead at the end we did `... foo 1 + 1000`, we'd get the result `1110`.
1060
1061 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.
1062
1063 You can make the lambda evaluator perform the required CPS transforms with these helper functions:
1064
1065         let reset = \body. \outk. outk (body (\i i)) in
1066         let shift = \k_body. \midk. (\k. (k_body k) (\i i)) (\a localk. localk (midk a)) in
1067         let abort = \body. \midk. body (\i i) in
1068         ...
1069
1070 You use these like so:
1071
1072 *       [reset body] is `reset BODY` where `BODY` is [body]
1073 *       [shift k body] is `shift (\k. BODY)` where `BODY` is [body]
1074 *       and [abort value] is `abort VALUE` where `VALUE` is [value]
1075         
1076 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.
1077
1078
1079 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.
1080
1081 (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).)
1082
1083
1084 Ken Shan has done terrific work exploring the relations of `shift` and `control` and other control operators to each other.
1085
1086 In collecting these CPS transforms and implementing the monadic versions, we've been helped by Ken and by Oleg and by these papers:
1087
1088 *       Danvy and Filinski, "Representing control: a study of the CPS transformation" (1992)
1089 *       Sabry, "Note on axiomatizing the semantics of control operators" (1996)
1090
1091
1092 -- cutting some of the following for control operators --
1093
1094 Examples of shift/reset/abort
1095 -----------------------------
1096
1097 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.)
1098
1099
1100 Example 1:
1101
1102         ; (+ 1000 (+ 100 (abort 11))) ~~> 11
1103         
1104         app2 (op2 plus) (var thousand)
1105           (app2 (op2 plus) (var hundred) (abort (var eleven)))
1106         
1107         # Continuation_monad.(run0(
1108             abort 11 >>= fun i ->
1109             unit (100+i) >>= fun j ->
1110             unit (1000+j)));;
1111         - : int = 11
1112
1113 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:
1114
1115         # Continuation_monad.(run0(
1116             reset (
1117               abort 11 >>= fun i ->
1118               unit (100+i) >>= fun j ->
1119               unit (1000+j))));;
1120         - : int = 11
1121
1122
1123 Example 2:
1124         
1125         ; (+ 1000 (reset (+ 100 (abort 11)))) ~~> 1011
1126         
1127         app2 (op2 plus) (var thousand)
1128           (reset (app2 (op2 plus) (var hundred) (abort (var eleven))))
1129         
1130         # Continuation_monad.(run0(
1131             reset (
1132               abort 11 >>= fun i ->
1133               unit (100+i)
1134             ) >>= fun j ->
1135             unit (1000+j)));;
1136         - : int = 1011
1137
1138 Example 3:
1139
1140         ; (+ 1000 (reset (+ 100 (shift k (+ 10 1))))) ~~> 1011
1141
1142         app2 (op2 plus) (var thousand)
1143           (reset (app2 (op2 plus) (var hundred)
1144             (shift (\k. ((op2 plus) (var ten) (var one))))))
1145
1146         Continuation_monad.(
1147           let v = reset (
1148             let u = shift (fun k -> unit (10 + 1))
1149             in u >>= fun x -> unit (100 + x)
1150           ) in let w = v >>= fun x -> unit (1000 + x)
1151           in run0 w);;
1152         - : int = 1011
1153
1154 Example 4:
1155
1156         ; (+ 1000 (reset (+ 100 (shift k (k (+ 10 1)))))) ~~> 1111
1157         
1158         app2 (op2 plus) (var thousand)
1159           (reset (app2 (op2 plus) (var hundred)
1160             (shift (\k. (app (var k) ((op2 plus) (var ten) (var one)))))))
1161         
1162         Continuation_monad.(
1163           let v = reset (
1164             let u = shift (fun k -> k (10 :: [1]))
1165             in u >>= fun x -> unit (100 :: x)
1166           ) in let w = v >>= fun x -> unit (1000 :: x)
1167           in run0 w);;
1168         - : int list = [1000; 100; 10; 1]
1169
1170 To demonstrate the different adding order between Examples 4 and 5, we use `::` in the OCaml version instead of `+`. Here is Example 5:
1171
1172         ; (+ 1000 (reset (+ 100 (shift k (+ 10 (k 1)))))) ~~> 1111 but added differently
1173
1174         app2 (op2 plus) (var thousand)
1175           (reset (app2 (op2 plus) (var hundred)
1176             (shift (\k. ((op2 plus) (var ten) (app (var k) (var one)))))))
1177         
1178         Continuation_monad.(let v = reset (
1179             let u = shift (fun k -> k [1] >>= fun x -> unit (10 :: x))
1180             in u >>= fun x -> unit (100 :: x)
1181           ) in let w = v >>= fun x -> unit (1000 :: x)
1182           in run0  w);;
1183         - : int list = [1000; 10; 100; 1]
1184
1185
1186 Example 6:
1187
1188         ; (+ 100 ((reset (+ 10 (shift k k))) 1)) ~~> 111
1189         
1190         app2 (op2 plus) (var hundred)
1191           (app (reset (app2 (op2 plus) (var ten)
1192             (shift (\k. (var k))))) (var one))
1193         
1194         (* not sure if this example can be typed as-is in OCaml... this is the best I an do at the moment... *)
1195
1196         # type 'x either = Left of (int -> ('x,'x either) Continuation_monad.m) | Right of int;;
1197         # Continuation_monad.(let v = reset (
1198             shift (fun k -> unit (Left k)) >>= fun i -> unit (Right (10+i))
1199           ) in let w = v >>= fun (Left k) ->
1200               k 1 >>= fun (Right i) ->
1201               unit (100+i)
1202           in run0 w);;
1203         - : int = 111
1204
1205 <!--
1206 # type either = Left of (int -> either) | Right of int;;
1207 # let getleft e = match e with Left lft -> lft | Right _ -> failwith "not a Left";;
1208 # let getright e = match e with Right rt -> rt | Left _ -> failwith "not a Right";;
1209 # 100 + getright (let v = reset (fun p () -> Right (10 + shift p (fun k -> Left k))) in getleft v 1);;
1210 -->
1211
1212 Example 7:
1213
1214         ; (+ 100 (reset (+ 10 (shift k (k (k 1)))))) ~~> 121
1215         
1216         app2 (op2 plus) (var hundred)
1217           (reset (app2 (op2 plus) (var ten)
1218             (shift (\k. app (var k) (app (var k) (var one))))))
1219         
1220         Continuation_monad.(let v = reset (
1221             let u = shift (fun k -> k 1 >>= fun x -> k x)
1222             in u >>= fun x -> unit (10 + x)
1223           ) in let w = v >>= fun x -> unit (100 + x)
1224           in run0 w)
1225         - : int = 121
1226
1227 <!--
1228
1229         print_endline "=== pa_monad's Continuation Tests ============";;
1230
1231         (1, 5 = C.(run0 (unit 1 >>= fun x -> unit (x+4))) );;
1232         (2, 9 = C.(run0 (reset (unit 5 >>= fun x -> unit (x+4)))) );;
1233         (3, 9 = C.(run0 (reset (abort 5 >>= fun y -> unit (y+6)) >>= fun x -> unit (x+4))) );;
1234         (4, 9 = C.(run0 (reset (reset (abort 5 >>= fun y -> unit (y+6))) >>= fun x -> unit (x+4))) );;
1235         (5, 27 = C.(run0 (
1236                                   let c = reset(abort 5 >>= fun y -> unit (y+6))
1237                                   in reset(c >>= fun v1 -> abort 7 >>= fun v2 -> unit (v2+10) ) >>= fun x -> unit (x+20))) );;
1238
1239         (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))) );;
1240
1241         (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))) );;
1242
1243         (12, ["a"] = C.(run0 (reset (shift (fun f -> f [] >>= fun t -> unit ("a"::t)  ) >>= fun xv -> shift (fun _ -> unit xv)))) );;
1244
1245
1246         (0, 15 = C.(run0 (let f k = k 10 >>= fun v-> unit (v+100) in reset (callcc f >>= fun v -> unit (v+5)))) );;
1247
1248 -->