1 <!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
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:
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
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
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.
37 ## The continuation monad
39 In order to build a monad, we start with a Kleisli arrow.
41 Continuation monad: types: given some ρ, Mα => (α -> ρ) -> ρ
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
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
65 monad using mid (`⇧`), then combine them using monadic function
68 ¢ M N = \k -> M (\f -> N (\a -> k(f x)))
70 for the continuation monad.
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,
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.
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)))))
111 mt3 I = "ababdeababdef" -- structure: (ababde)(ababde)f
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'.
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
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,
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
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
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"
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
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))
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
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
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
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
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
260 map2 f u v k = u(\u' -> v (\v' -> k(f u' v')))
261 t13 = map2 (++) (mid "a")
266 t13 (\k->Just k) == Just "abcd"
268 t14 = map2 (++) (mid "a")
274 t14 (\k->Just k) == Nothing