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?
157 This depends on which S is executed first.  Assume the first S is
158 executed first.  What will the value of its continuation k be?
159 It will be a function that maps a string s to the result of computing
160 ascSe, which will be ascascee.  So k(k "") will be k(acacee), which
161 will result in a(acacee)ca(acacee)cee (the parenthesese are added to
162 show stages in the construction of the final result).
164 Note that this is a different result than assuming that what execution
165 does is choose an S, and double its context, treating all other shift
166 operators as dumb letters, then choosing a remaining S to execute.  If
167 that was our interpreation of the task, then no string with more than
168 one S would ever terminate (on the bi-directional continuation
169 perspective).
172 ## Viewing Montague's PTQ as CPS
178 ## How continuations can simulate other monads
180 ## Delimited versus undelimited continuations
182 ## Natural language requries delimited continuations