bb6826039b61c6aef113d9e88676ab3d6498b760
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
33 followin fashion.
37 Let's take a look at some of our favorite monads from the point of
38 view of types.  Here, `==>` is the Kleisli arrow.
41                   ⇧: \ae.a : α -> Mα
42                   compose: \fghe.f(ghe)e : (Q->MR)->(P->MQ)->(P->MR)
43                   gloss: copy environment and distribute it to f and g
45     State monad: types: α ==> β -> (α x β)
46                  ⇧: \ae.(a,e) : α -> Mα
47                  compose: \fghe.let (x,s) = ghe in fxs
48                  thread the state through g, then through f
50     List monad: types: α ==> [α]
51                 ⇧: \a.[a] : α -> Mα
52                 compose: \fgh.concat(map f (gh))
53                 gloss: compose f and g pointwise
55     Maybe monad: types: α ==> Nothing | Just α
56                 ⇧: \a. Just a
57                 compose: \fgh.
58                   case gh of Nothing -> Nothing
59                            | Just x -> case fx of Nothing -> Nothing
60                                                 | Just y -> Just y
61                 gloss: strong Kline
63 Now we need a type for a continuation.  A continuized term is one that
64 expects its continuation as an argument.  The continuation of a term
65 is a function from the normal value of that term to a result.  So if
66 the term has type continuized term has type α, the continuized version
67 has type (α -> ρ) -> ρ:
69     Continuation monad: types: Mα => (α -> ρ) -> ρ
70                         ⇧: \ak.ka
71                         compose: \fghk.f(\f'.g h (\g'.f(g'h)
72                         gloss: first give the continuation to f, then build
73                                a continuation out of the result to give to
75 The first thing we should do is demonstrate that this monad is
76 suitable for accomplishing the task.
78 We lift the computation `("a" ++ ("b" ++ ("c" ++ "d")))` into
81     t1 = (map1 ((++) "a") (map1 ((++) "b") (map1 ((++) "c") (mid "d"))))
83 Here, `(++) "a"` is a function of type [Char] -> [Char] that prepends
84 the string "a", so `map1 ((++) "a")` takes a string continuation k and
85 returns a new string continuation that takes a string s returns "a" ++ k(s).
86 So `t1 (\k->k) == "abcd"`.
88 We can now define a shift operator to perform the work of "S":
90     shift u k = u(\s.k(ks))
92 Shift takes two arguments: a string continuation u of type (String -> String) -> String,
93 and a string continuation k of type String -> String.  Since u is the
94 result returned by the argument to shift, it represents the tail of
95 the list after the shift operator.  Then k is the continuation of the
96 expression headed by `shift`.  So in order to execute the task, shift
97 needs to invoke k twice.
99 Note that the shift operator constructs a new continuation by
100 composing its second argument with itself (i.e., the new doubled
101 continuation is \s.k(ks)).  Once it has constructed this
102 new continuation, it delivers it as an argument to the remaining part
103 of the computation!
105     (map1 ((++) "a") (map1 ((++) "b") (shift (mid "d")))) (\k->k) == "ababd"
107 Let's just make sure that we have the left-to-right evaluation we were
108 hoping for by evaluating "abSdeSf":
110     t6 = map1 ((++) "a")
111               (map1 ((++) "b")
112                     (shift
113                       (map1 ((++) "d")
114                             (map1 ((++) "e")
115                                   (shift (mid "f"))))))
117     t6 (\k->k) == "ababdeababdef"
119 As expected.
121 In order to add a reset operator #, we can have
123     # u k = k(u(\k.k))
124     ab#deSf ~~> abdedef
126 Note that the lifting of the original unmonadized computation treated
127 prepending "a" as a one-place operation.  If we decompose this
128 operation into a two-place operation of appending combined with a
129 string "a", an interesting thing happens.
132     map2 f u v k = u(\u' -> v (\v' -> k(f u' v')))
133     shift k = k (k "")
135     t2 = map2 (++) (mid "a")
136                    (map2 (++) (mid "b")
137                               (map2 (++) shift
138                                          (map2 (++) (mid "d")
139                                                     (mid []))))
140     t2 (\k->k) == "ababdd"
142 First, we need map2 instead of map1.  Second, the type of the shift
143 operator will be a string continuation, rather than a function from
144 string continuations to string continuations.
146 But here's the interesting part: from the point of view of the shift
147 operator, the continuation that it will be fed will be the entire rest
148 of the computation.  This includes not only what has come before, but
149 what will come after it as well.  That means when the continuation is
150 doubled (self-composed), the result duplicates not only the prefix
151 `(ab ~~> abab)`, but also the suffix `(d ~~> dd)`.  In some sense, then,
152 continuations allow functions to see into the future!
154 What do you expect will be the result of executing "aScSe" under the
155 second perspective?  The answer to this question is not determined by
156 the informal specification of the task that we've been using, since
157 under the new perspective, we're copying complete (bi-directional)
158 contexts rather than just left contexts.
160 It might be natural to assume that what execution does is choose an S,
161 and double its context, temporarily treating all other shift operators
162 as dumb letters, then choosing a remaining S to execute.  If that was
163 our interpreation of the task, then no string with more than one S
164 would ever terminate, since the number S's after each reduction step
165 would always be 2(n-1), where n is the number before reduction.
167 But there is another equally natural way to answer the question.
168 Assume the leftmost S is executed first.  What will the value of its
169 continuation k be?  It will be a function that maps a string s to the
170 result of computing `ascSe`, which will be `ascascee`.  So `k(k "")`
171 will be `k(acacee)`, which will result in `a(acacee)ca(acacee)cee`
172 (the parentheses are added to show stages in the construction of the
173 final result).
175 So the continuation monad behaves in a way that we expect a
176 continuation to behave.  But where did the continuation monad come
177 from?  Let's consider some ways of deriving the continuation monad.
179 ## Viewing Montague's PTQ as CPS
181 Montague's conception of determiner phrases as generalized quantifiers
182 is a limited form of continuation-passing.  (See, e.g., chapter 4 of
183 Barker and Shan 2014.)  Start by assuming that ordinary DPs such as
184 proper names denote objects of type `e`.  Then verb phrases denote
185 functions from individuals to truth values, i.e., functions of type `e
186 -> t`.
188 The meaning of extraordinary DPs such as *every woman* or *no dog*
189 can't be expressed as a simple individual.  As Montague argued, it
190 works much better to view them as predicates on verb phrase meanings,
191 i.e., as having type `(e->t)->t`.  Then *no woman left* is true just
192 in case the property of leaving is true of no woman:
194     no woman:  \k.not \exists x . (woman x) & kx
195     left: \x.left x
196     (no woman) (left) = not \exists x . woman x & left x
198 Montague also proposed that all determiner phrases should have the
199 same type.  After all, we can coordinate proper names with
200 quantificational DPs, as in *John and no dog left*.  Then generalized
201 quantifier corresponding to the proper name *John* is the quantifier
202 `\k.kj`.
204 At this point, we have a type for our Kliesli arrow and a value for
205 our mid.  Given some result type (such as `t` in the Montague application),
207     α ==> (α -> ρ) -> ρ
208     ⇧a = \k.ka
210 It remains only to find a suitable value for bind.  Montague didn't
211 provide one, but it's easy to find:
213     bind ::    Mα -> (α -> Mβ) -> Mβ
215 given variables of the following types
217     u :: Mα == (α -> ρ) -> ρ
218     f :: α -> Mβ
219     k :: β -> ρ
220     x :: α
222 We have
224     bind u f = \k.u(\x.fxk)
226 Let's carefully make sure that this types out:
228     bind u f = \k.       u      (\x .   f       x     k)
229                                       --------  --
230                                       α -> Mβ   α
231                                      ------------  ------
232                                          Mβ        β -> ρ
233                                   --  --------------------
234                                   α            ρ
235                   -------------  ------------------------
236                   (α -> ρ) -> ρ             α -> ρ
237                   ---------------------------------
238                                 ρ
239                 -----------------------
240                     (β -> ρ) -> ρ
242 Yep!
244 Is there any other way of building a bind operator?  Well, the
245 challenge is getting hold of the "a" that is buried inside of `u`.
246 In the Reader monad, we could get at the a inside of the box by
247 applying the box to an environment.  In the State monad, we could get
248 at the a by applying to box to a state and deconstructing the
249 resulting pair.  In the continuation case, the only way to do it is to
250 apply the boxed a (i.e., u) to a function that takes an a as an
251 argument.  That means that f must be invoked inside the scope of the
252 functional argument to u.  So we've deduced the structure
254     ... u (\x. ... f x ...) ...
256 At this point, in order to provide u with an argument of the
257 appropriate type, the argument must not only take objects of type
258 α as an argument, it must return a result of type ρ.  That means that
259 we must apply fx to an object of type β -> ρ.  We can hypothesize such
260 an object, as long as we eliminate that hypothesis later (by binding
261 it), and we have the complete bind operation.
263 The way in which the value of type α that is needed in order to unlock
264 the function f is hidden inside of u is directly analogous to the
265 concept of "data hiding" in object-oriented programming.  See Pierce's
266 discussion of how to extend system F with existential type
267 quantification by encoding the existential using continuations.
269 So the Kliesli type pretty much determines the bind operation.
271 ## What continuations are doing
273 Ok, we have a continuation monad.  We derived it from first
274 principles, and we have seen that it behaves at least in some respects
275 as we expect a continuation monad to behave (in that it allows us to
276 give a good implementation of the task).
278 ## How continuations can simulate other monads
280 Because the continuation monad allows the result type ρ to be any
281 type, we can choose ρ in clever ways that allow us to simulate other
284     Reader: ρ = env -> α
285     State: ρ = s -> (α, s)
286     Maybe: ρ = Just α | Nothing
288 You see how this is going to go.  Let's see an example by adding an
289 abort operator to our task language, which represents what
290 we want to have happen if we divide by zero, where what we want to do
291 is return Nothing.
293     abort k = Nothing
294     mid a k = k a
295     map2 f u v k = u(\u' -> v (\v' -> k(f u' v')))
296     t13 = map2 (++) (mid "a")
297                    (map2 (++) (mid "b")
298                               (map2 (++) (mid "c")
299                                          (mid "d")))
301     t13 (\k->Just k) == Just "abcd"
303     t14 = map2 (++) (mid "a")
304                    (map2 (++) abort
305                               (map2 (++) (mid "c")
306                                          (mid "d")))
309     t14 (\k->Just k) == Nothing
311 Super cool.
316 ## Delimited versus undelimited continuations
318 ## Natural language requries delimited continuations