name change
[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