rename topics/_coroutines_and_aborts.mdwn to topics/week13_coroutines_exceptions_and_...
[lambda.git] / topics / _cps.mdwn
1 Gaining control over order of evaluation
2 ----------------------------------------
3
4 We know that evaluation order matters.  We're beginning to learn how
5 to gain some control over order of evaluation (think of Jim's abort handler).
6 We continue to reason about order of evaluation.
7
8 A lucid discussion of evaluation order in the
9 context of the lambda calculus can be found here:
10 [Sestoft: Demonstrating Lambda Calculus Reduction](http://www.itu.dk/~sestoft/papers/mfps2001-sestoft.pdf).
11 Sestoft also provides a lovely on-line lambda evaluator:
12 [Sestoft: Lambda calculus reduction workbench](http://www.itu.dk/~sestoft/lamreduce/index.html),
13 which allows you to select multiple evaluation strategies, 
14 and to see reductions happen step by step.
15
16 Evaluation order matters
17 ------------------------
18
19 We've seen this many times.  For instance, consider the following
20 reductions.  It will be convenient to use the abbreviation `w =
21 \x.xx`.  I'll
22 indicate which lambda is about to be reduced with a * underneath:
23
24 <pre>
25 (\x.y)(ww)
26  *
27 y
28 </pre>
29
30 Done!  We have a normal form.  But if we reduce using a different
31 strategy, things go wrong:
32
33 <pre>
34 (\x.y)(ww) =
35 (\x.y)((\x.xx)w) =
36         *
37 (\x.y)(ww) =
38 (\x.y)((\x.xx)w) =
39         *
40 (\x.y)(ww) 
41 </pre>
42
43 Etc.  
44
45 As a second reminder of when evaluation order matters, consider using
46 `Y = \f.(\h.f(hh))(\h.f(hh))` as a fixed point combinator to define a recursive function:
47
48 <pre>
49 Y (\f n. blah) =
50 (\f.(\h.f(hh))(\h.f(hh))) (\f n. blah) 
51      *
52 (\f.f((\h.f(hh))(\h.f(hh)))) (\f n. blah) 
53        *
54 (\f.f(f((\h.f(hh))(\h.f(hh))))) (\f n. blah) 
55          *
56 (\f.f(f(f((\h.f(hh))(\h.f(hh)))))) (\f n. blah) 
57 </pre>
58
59 And we never get the recursion off the ground.
60
61
62 Using a Continuation Passing Style transform to control order of evaluation
63 ---------------------------------------------------------------------------
64
65 We'll present a technique for controlling evaluation order by transforming a lambda term
66 using a Continuation Passing Style transform (CPS), then we'll explore
67 what the CPS is doing, and how.
68
69 In order for the CPS to work, we have to adopt a new restriction on
70 beta reduction: beta reduction does not occur underneath a lambda.
71 That is, `(\x.y)z` reduces to `z`, but `\u.(\x.y)z` does not reduce to
72 `\u.z`, because the `\u` protects the redex in the body from
73 reduction.  (In this context, a "redex" is a part of a term that matches
74 the pattern `...((\xM)N)...`, i.e., something that can potentially be
75 the target of beta reduction.)
76
77 Start with a simple form that has two different reduction paths:
78
79 reducing the leftmost lambda first: `(\x.y)((\x.z)u)  ~~> y`
80
81 reducing the rightmost lambda first: `(\x.y)((\x.z)u)  ~~> (\x.y)z ~~> y`
82
83 After using the following call-by-name CPS transform---and assuming
84 that we never evaluate redexes protected by a lambda---only the first
85 reduction path will be available: we will have gained control over the
86 order in which beta reductions are allowed to be performed.
87
88 Here's the CPS transform defined:
89
90     [x] = x
91     [\xM] = \k.k(\x[M])
92     [MN] = \k.[M](\m.m[N]k)
93
94 Here's the result of applying the transform to our simple example:
95
96     [(\x.y)((\x.z)u)] =
97     \k.[\x.y](\m.m[(\x.z)u]k) =
98     \k.(\k.k(\x.[y]))(\m.m(\k.[\x.z](\m.m[u]k))k) =
99     \k.(\k.k(\x.y))(\m.m(\k.(\k.k(\x.z))(\m.muk))k)
100
101 Because the initial `\k` protects (i.e., takes scope over) the entire
102 transformed term, we can't perform any reductions.  In order to watch
103 the computation unfold, we have to apply the transformed term to a
104 trivial continuation, usually the identity function `I = \x.x`.
105
106     [(\x.y)((\x.z)u)] I =
107     (\k.[\x.y](\m.m[(\x.z)u]k)) I
108      *
109     [\x.y](\m.m[(\x.z)u] I) =
110     (\k.k(\x.y))(\m.m[(\x.z)u] I)
111      *           *
112     (\x.y)[(\x.z)u] I           --A--
113      *
114     y I
115
116 The application to `I` unlocks the leftmost functor.  Because that
117 functor (`\x.y`) throws away its argument (consider the reduction in the
118 line marked (A)), we never need to expand the
119 CPS transform of the argument.  This means that we never bother to
120 reduce redexes inside the argument.
121
122 Compare with a call-by-value xform:
123
124     {x} = \k.kx
125     {\aM} = \k.k(\a{M})
126     {MN} = \k.{M}(\m.{N}(\n.mnk))
127
128 This time the reduction unfolds in a different manner:
129
130     {(\x.y)((\x.z)u)} I =
131     (\k.{\x.y}(\m.{(\x.z)u}(\n.mnk))) I
132      *
133     {\x.y}(\m.{(\x.z)u}(\n.mnI)) =
134     (\k.k(\x.{y}))(\m.{(\x.z)u}(\n.mnI))
135      *             *
136     {(\x.z)u}(\n.(\x.{y})nI) =
137     (\k.{\x.z}(\m.{u}(\n.mnk)))(\n.(\x.{y})nI)
138      *
139     {\x.z}(\m.{u}(\n.mn(\n.(\x.{y})nI))) =
140     (\k.k(\x.{z}))(\m.{u}(\n.mn(\n.(\x.{y})nI)))
141      *             *
142     {u}(\n.(\x.{z})n(\n.(\x.{y})nI)) =
143     (\k.ku)(\n.(\x.{z})n(\n.(\x.{y})nI))
144      *      *
145     (\x.{z})u(\n.(\x.{y})nI)       --A--
146      *
147     {z}(\n.(\x.{y})nI) =
148     (\k.kz)(\n.(\x.{y})nI)
149      *      *
150     (\x.{y})zI
151      *
152     {y}I =
153     (\k.ky)I
154      *
155     I y
156
157 In this case, the argument does get evaluated: consider the reduction
158 in the line marked (A).
159
160 Both xforms make the following guarantee: as long as redexes
161 underneath a lambda are never evaluated, there will be at most one
162 reduction available at any step in the evaluation.
163 That is, all choice is removed from the evaluation process.
164
165 Now let's verify that the CBN CPS avoids the infinite reduction path
166 discussed above (remember that `w = \x.xx`):
167
168     [(\x.y)(ww)] I =
169     (\k.[\x.y](\m.m[ww]k)) I
170      *
171     [\x.y](\m.m[ww]I) =
172     (\k.k(\x.y))(\m.m[ww]I)
173      *             *
174     (\x.y)[ww]I
175      *
176     y I
177
178
179 Questions and exercises:
180
181 1. Prove that {(\x.y)(ww)} does not terminate.
182
183 2. Why is the CBN xform for variables `[x] = x` instead of something
184 involving kappas (i.e., `k`'s)?  
185
186 3. Write an Ocaml function that takes a lambda term and returns a
187 CPS-xformed lambda term.  You can use the following data declaration:
188
189     type form = Var of char | Abs of char * form | App of form * form;;
190
191 4. The discussion above talks about the "leftmost" redex, or the
192 "rightmost".  But these words apply accurately only in a special set
193 of terms.  Characterize the order of evaluation for CBN (likewise, for
194 CBV) more completely and carefully.
195
196 5. What happens (in terms of evaluation order) when the application
197 rule for CBV CPS is changed to `{MN} = \k.{N}(\n.{M}(\m.mnk))`?
198
199 6. A term and its CPS xform are different lambda terms.  Yet in some
200 sense they "do" the same thing computationally.  Make this sense
201 precise.
202
203
204 Thinking through the types
205 --------------------------
206
207 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).
208
209 Let's say we're working in the simply-typed lambda calculus.
210 Then if the original term is well-typed, the CPS xform will also be
211 well-typed.  But what will the type of the transformed term be?
212
213 The transformed terms all have the form `\k.blah`.  The rule for the
214 CBN xform of a variable appears to be an exception, but instead of
215 writing `[x] = x`, we can write `[x] = \k.xk`, which is
216 eta-equivalent.  The `k`'s are continuations: functions from something
217 to a result.  Let's use &sigma; as the result type.  The each `k` in
218 the transform will be a function of type &rho; --> &sigma; for some
219 choice of &rho;.
220
221 We'll need an ancilliary function ': for any ground type a, a' = a;
222 for functional types a->b, (a->b)' = ((a' -> &sigma;) -> &sigma;) -> (b' -> &sigma;) -> &sigma;.
223
224     Call by name transform
225
226     Terms                            Types
227
228     [x] = \k.xk                      [a] = (a'->o)->o
229     [\xM] = \k.k(\x[M])              [a->b] = ((a->b)'->o)->o
230     [MN] = \k.[M](\m.m[N]k)          [b] = (b'->o)->o
231
232 Remember that types associate to the right.  Let's work through the
233 application xform and make sure the types are consistent.  We'll have
234 the following types:
235
236     M:a->b
237     N:a
238     MN:b 
239     k:b'->o
240     [N]:(a'->o)->o
241     m:((a'->o)->o)->(b'->o)->o
242     m[N]:(b'->o)->o
243     m[N]k:o 
244     [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
245     [M](\m.m[N]k):o
246     [MN]:(b'->o)->o
247
248 Be aware that even though the transform uses the same symbol for the
249 translation of a variable (i.e., `[x] = x`), in general the variable
250 in the transformed term will have a different type than in the source
251 term.
252
253 Excercise: what should the function ' be for the CBV xform?  Hint: 
254 see the Meyer and Wand abstract linked above for the answer.
255
256
257 Other CPS transforms
258 --------------------
259
260 It is easy to think that CBN and CBV are the only two CPS transforms.
261 (We've already seen a variant on call-by-value one of the excercises above.) 
262
263 In fact, the number of distinct transforms is unbounded.  For
264 instance, here is a variant of CBV that uses the same types as CBN:
265
266     <x> = x
267     <\xM> = \k.k(\x<M>)
268     <MN> = \k.<M>(\m.<N>(\n.m(\k.kn)k))
269
270 Try reducing `<(\x.x) ((\y.y) (\z.z))> I` to convince yourself that
271 this is a version of call-by-value.
272
273 Once we have two evaluation strategies that rely on the same types, we
274 can mix and match:
275
276     [x] = x
277     <x> = x
278     [\xM] = \k.k(\x<M>)
279     <\xM] = \k.k(\x[M])
280     [MN] = \k.<M>(\m.m<N>k)
281     <MN> = \k.[M](\m.[N](\n.m(\k.kn)k))
282
283 This xform interleaves call-by-name and call-by-value in layers,
284 according to the depth of embedding.
285 (Cf. page 4 of Reynold's 1974 paper ftp://ftp.cs.cmu.edu/user/jcr/reldircont.pdf (equation (4) and the
286 explanation in the paragraph below.)