1 <!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
3 [[!toc]]
5 # Continuations
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.
11     abSdS ~~> ababdS ~~> ababdababd
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:
18     ab#deSfg ~~> abededfg
20 In this variant, "S" and "#" correspond to `shift` and `reset`, which
21 provide access to delimited continuations.
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.
29 We then presented CPS transforms, and demonstrated how they provide
30 an order-independent analysis of order of evaluation.
32 In order to continue to explore continuations, we will proceed in the
34 and show how it solves the task, then generalize the task to
35 include doubling of both the left and the right context.
39 In order to build a monad, we start with a Kleisli arrow.
41     Continuation monad: types: given some ρ, Mα => (α -> ρ) -> ρ
42                         ⇧ == \ak.ka : a -> Ma
43                         bind == \ufk. u(\x.fxk)
45 We'll first show that this monad solves the task, then we'll consider
46 the monad in more detail.
48 The unmonadized computation (without the shifty "S" operator) is
50     t1 = + a (+ b (+ c d)) ~~> abcd
52 where "+" is string concatenation and the symbol a is shorthand for
53 the string "a".
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].
59 Writing ¢ in between its arguments, t1 corresponds to the following
62     mt1 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ ⇧c ¢ ⇧d))
64 We have to lift each functor (+) and each object (e.g., "b") into the
66 application, where
68     ¢ M N = \k -> M (\f -> N (\a -> k(f x)))
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,
76     t1 = mt1 I
78 That is, the original computation is the monadic version applied to
79 the trivial continuation.
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:
87     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
89 We can now define a shift operator to perform the work of "S":
91     shift u k = u(\s.k(ks))
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.
100     mt2 I == "ababd"
102 just as desired.
104 Let's just make sure that we have the left-to-right evaluation we were
105 hoping for by evaluating "abSdeSf":
107     mt3 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ (⇧+ ¢ ⇧d ¢ (⇧+ ¢ ⇧e ¢ (shift ⇧f)))))
109 Then
111     mt3 I = "ababdeababdef"   -- structure: (ababde)(ababde)f
114 As expected.
116 For a reset operator #, we can have
118     # u k = k(u(\k.k))   -- ex.: ab#deSf ~~> abdedef
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.
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.
129 ## Generalizing to the tree doubling task
131 Now we should consider what happens when we write a shift operator
132 that takes the place of a single letter.
134     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
135     mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d))
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'.
141     shift' = \k.k(k"")
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.
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,
154     mt4 I = "ababdd"
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".
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
166     aScSe ~~> aacSecSe
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.
172 But that's not what the continuation operator shift' delivers.
174     mt5 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ (⇧+ ¢ ⇧c ¢ (⇧+ ¢ shift' ¢ "e")))
176     mt5 I = "aacaceecaacaceecee" -- structure: "aacaceecaacaceecee"
178 Huh?
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.
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:
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>
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.
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.
218 ## Viewing Montague's PTQ as CPS
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`.
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:
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
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`.
243 ## How continuations can simulate other monads
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
249     Reader: ρ = env -> α
250     State: ρ = s -> (α, s)
251     Maybe: ρ = Just α | Nothing
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.
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")))
266     t13 (\k->Just k) == Just "abcd"
268     t14 = map2 (++) (mid "a")
269                    (map2 (++) abort
270                               (map2 (++) (mid "c")
271                                          (mid "d")))
274     t14 (\k->Just k) == Nothing
276 Super cool.