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 followin fashion.
  34
  35 ## The continuation monad
  36
  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.
  39
  40     Reader monad: types: Mα ==> β -> α
  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
  44
  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
  49
  50     List monad: types: α ==> [α]
  51                 ⇧: \a.[a] : α -> Mα
  52                 compose: \fgh.concat(map f (gh))
  53                 gloss: compose f and g pointwise
  54
  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
  62
  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 (α -> ρ) -> ρ:
  68
  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
  74
  75 The first thing we should do is demonstrate that this monad is
  76 suitable for accomplishing the task.
  77
  78 We lift the computation `("a" ++ ("b" ++ ("c" ++ "d")))` into
  79 the monad as follows:
  80
  81     t1 = (map1 ((++) "a") (map1 ((++) "b") (map1 ((++) "c") (mid "d"))))
  82
  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"`.
  87
  88 We can now define a shift operator to perform the work of "S":
  89
  90     shift u k = u(\s.k(ks))
  91
  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.
  98
  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!
 104
 105     (map1 ((++) "a") (map1 ((++) "b") (shift (mid "d")))) (\k->k) == "ababd"
 106
 107 Let's just make sure that we have the left-to-right evaluation we were
 108 hoping for by evaluating "abSdeSf":
 109
 110     t6 = map1 ((++) "a")
 111               (map1 ((++) "b")
 112                     (shift
 113                       (map1 ((++) "d")
 114                             (map1 ((++) "e")
 115                                   (shift (mid "f"))))))
 116
 117     t6 (\k->k) == "ababdeababdef"
 118
 119 As expected.
 120
 121 In order to add a reset operator #, we can have
 122
 123     # u k = k(u(\k.k))
 124     ab#deSf ~~> abdedef
 125
 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.
 130
 131
 132     map2 f u v k = u(\u' -> v (\v' -> k(f u' v')))
 133     shift k = k (k "")
 134
 135     t2 = map2 (++) (mid "a")
 136                    (map2 (++) (mid "b")
 137                               (map2 (++) shift
 138                                          (map2 (++) (mid "d")
 139                                                     (mid []))))
 140     t2 (\k->k) == "ababdd"
 141
 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.
 145
 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!
 153
 154 What do you expect will be the result of executing "aScSe" under the
 155 second perspective?
 156
 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).
 163
 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).
 170
 171
 172 ## Viewing Montague's PTQ as CPS
 173
 174
 175
 176
 177
 178 ## How continuations can simulate other monads
 179
 180 ## Delimited versus undelimited continuations
 181
 182 ## Natural language requries delimited continuations
 183
 184
 185
 186
 187
 188