last lecture

[lambda.git] / topics / _week14_continuations.mdwn

diff --git a/topics/_week14_continuations.mdwn b/topics/_week14_continuations.mdwn
index bb68260..0b99065 100644 (file)
--- a/topics/_week14_continuations.mdwn
+++ b/topics/_week14_continuations.mdwn
@@ -30,119 +30,243 @@ We then presented CPS transforms, and demonstrated how they provide
 an order-independent analysis of order of evaluation.
 
 In order to continue to explore continuations, we will proceed in the
 an order-independent analysis of order of evaluation.
 
 In order to continue to explore continuations, we will proceed in the

-followin fashion.
+following fashion: we introduce the traditional continuation monad,
+and show how it solves the task, then generalize the task to 
+include doubling of both the left and the right context.

 
 ## The continuation monad
 
 
 ## The continuation monad
 

-Let's take a look at some of our favorite monads from the point of
-view of types.  Here, `==>` is the Kleisli arrow.
-
-    Reader monad: types: Mα ==> β -> α
-                  ⇧: \ae.a : α -> Mα
-                  compose: \fghe.f(ghe)e : (Q->MR)->(P->MQ)->(P->MR)
-                  gloss: copy environment and distribute it to f and g
-
-    State monad: types: α ==> β -> (α x β)
-                 ⇧: \ae.(a,e) : α -> Mα
-                 compose: \fghe.let (x,s) = ghe in fxs
-                 thread the state through g, then through f                 
-
-    List monad: types: α ==> [α]
-                ⇧: \a.[a] : α -> Mα
-                compose: \fgh.concat(map f (gh))
-                gloss: compose f and g pointwise
-
-    Maybe monad: types: α ==> Nothing | Just α
-                ⇧: \a. Just a
-                compose: \fgh.
-                 case gh of Nothing -> Nothing
-                          | Just x -> case fx of Nothing -> Nothing
-                                                | Just y -> Just y
-                gloss: strong Kline
-
-Now we need a type for a continuation.  A continuized term is one that
-expects its continuation as an argument.  The continuation of a term
-is a function from the normal value of that term to a result.  So if
-the term has type continuized term has type α, the continuized version
-has type (α -> ρ) -> ρ:
-
-    Continuation monad: types: Mα => (α -> ρ) -> ρ
-                        ⇧: \ak.ka
-                        compose: \fghk.f(\f'.g h (\g'.f(g'h)
-                       gloss: first give the continuation to f, then build
-                               a continuation out of the result to give to 
-
-The first thing we should do is demonstrate that this monad is
-suitable for accomplishing the task.
-
-We lift the computation `("a" ++ ("b" ++ ("c" ++ "d")))` into 
-the monad as follows:
-
-    t1 = (map1 ((++) "a") (map1 ((++) "b") (map1 ((++) "c") (mid "d"))))
-
-Here, `(++) "a"` is a function of type [Char] -> [Char] that prepends
-the string "a", so `map1 ((++) "a")` takes a string continuation k and
-returns a new string continuation that takes a string s returns "a" ++ k(s).
-So `t1 (\k->k) == "abcd"`.
+In order to build a monad, we start with a Kleisli arrow.
+
+    Continuation monad: types: given some ρ, Mα => (α -> ρ) -> ρ
+                        ⇧ == \ak.ka : a -> Ma
+                        bind == \ufk. u(\x.fxk)
+
+We'll first show that this monad solves the task, then we'll consider
+the monad in more detail.
+
+The unmonadized computation (without the shifty "S" operator) is
+
+    t1 = + a (+ b (+ c d)) ~~> abcd
+
+where "+" is string concatenation and the symbol a is shorthand for
+the string "a".
+
+In order to use the continuation monad to solve the list task,
+we choose α = ρ = [Char].  So "abcd" is a list of characters, and
+a boxed list has type M[Char] == ([Char] -> [Char]) -> [Char].
+
+Writing ¢ in between its arguments, t1 corresponds to the following
+monadic computation:
+
+    mt1 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ ⇧c ¢ ⇧d))
+
+We have to lift each functor (+) and each object (e.g., "b") into the
+monad using mid (`⇧`), then combine them using monadic function
+application, where
+
+    ¢ mf mx = \k -> mf (\f -> mx (\a -> k(f x)))
+
+for the continuation monad.
+
+The way in which we extract a value from a continuation box is by
+applying it to a continuation; often, it is convenient to supply the
+trivial continuation, the identity function \k.k = I.  So in fact, 
+
+   t1 = mt1 I
+
+That is, the original computation is the monadic version applied to
+the trivial continuation.
+
+We can now imagine replacing the third element ("c") with a shifty
+operator.  We would like to replace just the one element, and we will
+do just that in a moment; but in order to simulate the original task,
+we'll have to take a different strategy initially.  We'll start by
+imagining a shift operator that combined direction with the tail of
+the list, like this:
+
+    mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))

 
 We can now define a shift operator to perform the work of "S":
 
     shift u k = u(\s.k(ks))
 
 
 We can now define a shift operator to perform the work of "S":
 
     shift u k = u(\s.k(ks))
 

-Shift takes two arguments: a string continuation u of type (String -> String) -> String,
-and a string continuation k of type String -> String.  Since u is the
-result returned by the argument to shift, it represents the tail of
-the list after the shift operator.  Then k is the continuation of the
-expression headed by `shift`.  So in order to execute the task, shift
-needs to invoke k twice.
+Shift takes two arguments: a string continuation u of type M[Char],
+and a string continuation k of type [Char] -> [Char].  Since u is the
+the argument to shift, it represents the tail of the list after the
+shift operator.  Then k is the continuation of the expression headed
+by `shift`.  So in order to execute the task, shift needs to invoke k
+twice.

 
 

-Note that the shift operator constructs a new continuation by
-composing its second argument with itself (i.e., the new doubled
-continuation is \s.k(ks)).  Once it has constructed this
-new continuation, it delivers it as an argument to the remaining part
-of the computation!  
+    mt2 I == "ababd"

 
 

-    (map1 ((++) "a") (map1 ((++) "b") (shift (mid "d")))) (\k->k) == "ababd"
+just as desired.

 
 Let's just make sure that we have the left-to-right evaluation we were
 hoping for by evaluating "abSdeSf":
 
 
 Let's just make sure that we have the left-to-right evaluation we were
 hoping for by evaluating "abSdeSf":
 

-    t6 = map1 ((++) "a")
-              (map1 ((++) "b")
-                    (shift
-                     (map1 ((++) "d")
-                            (map1 ((++) "e")
-                                  (shift (mid "f"))))))
+    mt3 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ (⇧+ ¢ ⇧d ¢ (⇧+ ¢ ⇧e ¢ (shift ⇧f)))))

 
 

-    t6 (\k->k) == "ababdeababdef"
+Then
+
+    mt3 I = "ababdeababdef"   -- structure: (ababde)(ababde)f
+             

 
 As expected.
 
 
 As expected.
 

-In order to add a reset operator #, we can have
+For a reset operator #, we can have 

 
 

-    # u k = k(u(\k.k))
-    ab#deSf ~~> abdedef
+    # u k = k(u(\k.k))   -- ex.: ab#deSf ~~> abdedef

 
 

-Note that the lifting of the original unmonadized computation treated
-prepending "a" as a one-place operation.  If we decompose this
-operation into a two-place operation of appending combined with a
-string "a", an interesting thing happens.
+So the continuation monad solves the list task using continuations in
+a way that conforms to our by-now familiar strategy of lifting a
+computation into a monad, and then writing a few key functions (shift,
+reset) that exploit the power of the monad.

 
 

+Now we should consider what happens when we write a shift operator
+that takes the place of a single letter.

 
 

-    map2 f u v k = u(\u' -> v (\v' -> k(f u' v'))) 
-    shift k = k (k "")
+    mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
+    mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d))

 
 

-    t2 = map2 (++) (mid "a")
-                   (map2 (++) (mid "b")
-                              (map2 (++) shift
-                                        (map2 (++) (mid "d")
-                                                   (mid []))))
-    t2 (\k->k) == "ababdd"
+Instead of mt2, we have mt4.  So now the type of "c" (a boxed string,
+type M[Char]) is the same as the type of the new shift operator, shift'.
+
+    shift' = \k.k(k"")
+
+This shift operator takes a continuation k of type [Char]->[Char], and
+invokes it twice.  Since k requires an argument of type [Char], we
+need to use the first invocation of k to construction a [Char]; we do
+this by feeding it a string.  Since the task does not replace the
+shift operator with any marker, we give the empty string "" as the
+argument.
+
+But now the new shift operator captures more than just the preceeding
+part of the construction---it captures the entire context, including
+the portion of the sequence that follows it.  That is,
+
+    mt4 I = "ababdd"
+
+We have replaced "S" in "abSd" with "ab_d", where the underbar will be
+replaced with the empty string supplied in the definition of shift'.
+Crucially, not only is the prefix "ab" duplicated, so is the suffix
+"d".
+
+Things get interesting when we have more than one operator in the
+initial list.  What should we expect if we start with "aScSe"?
+If we assume that when we evaluate each S, all the other S's become
+temporarily inert, we expect a reduction path like
+
+    aScSe ~~> aacSecSe
+
+But note that the output has just as many S's as the input--if that is
+what our reduction strategy delivers, then any initial string with
+more than one S will never reach a normal form.
+
+But that's not what the continuation operator shift' delivers.
+
+    mt5 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ (⇧+ ¢ ⇧c ¢ (⇧+ ¢ shift' ¢ "e")))
+
+    mt5 I = "aacaceecaacaceecee" -- structure: "aacaceecaacaceecee"
+
+Huh?
+
+This is considerably harder to understand than the original list task.
+The key is figuring out in each case what function the argument k to
+the shift operator gets bound to.
+
+Let's go back to a simple one-shift example, "aSc".  Let's trace what
+the shift' operator sees as its argument k by replacing ⇧ and ¢ with
+their definitions:
+
+      ⇧+ ¢ ⇧a ¢ (⇧+ ¢ shift' ¢ ⇧c) I
+   = \k.⇧+(\f.⇧a(\x.k(fx))) ¢ (⇧+ ¢ shift' ¢ ⇧c) I
+   = \k.(\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.k(fx))) I
+   ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(\x.I(fx))) 
+   ~~> (\k.⇧+(\f.⇧a(\x.k(fx))))(\f.(⇧+ ¢ shift' ¢ ⇧c)(f)) 
+   ~~> ⇧+(\f.⇧a(\x.(\f.(⇧+ ¢ shift' ¢ ⇧c)(f))(fx)))) 
+   ~~> ⇧+(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx)))
+   = (\k.k+)(\f.⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(fx)))
+   ~~> ⇧a(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x))
+   = (\k.ka)(\x.(⇧+ ¢ shift' ¢ ⇧c)(+x))
+   ~~> (⇧+ ¢ shift' ¢ ⇧c)(+a)
+   = (\k.⇧+(\f.shift(\x.k(fx)))) ¢ ⇧c (+a)
+   = (\k.(\k.⇧+(\f.shift(\x.k(fx))))(\f.⇧c(\x.k(fx))))(+a)
+   ~~> (\k.⇧+(\f.shift(\x.k(fx))))(\f'.⇧c(\x'.(+a)(f'x')))
+   ~~> ⇧+(\f.shift(\x.(\f'.⇧c(\x'.(+a)(f'x')))(fx)))
+   ~~> ⇧+(\f.shift(\x.⇧c(\x'.(+a)((fx)x'))))
+   = (\k.k+)(\f.shift(\x.⇧c(\x'.(+a)((fx)x'))))
+   ~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
+   = shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
+   ~~> shift(\x.(+a)((+x)c))
+
+So now we see what the argument of shift will be: a function k from
+strings x to the string asc.  So shift k will be k(k "") = aacc.
+
+Ok, this is ridiculous.  We need a way to get ahead of this deluge of
+lambda conversion.  We'll adapt the notational strategy developed in
+Barker and Shan 2014:
+
+Instead of writing
+
+    \k.g(kf): (α -> ρ) -> ρ
+
+we'll write
+
+    g[]    ρ
+    --- : ---
+     f     α
+
+Then 
+             []
+    mid(x) = --
+             x
+
+and
+
+    g[]    ρ      h[]    ρ    g[h[]]    ρ
+    --- : ----  ¢ --- : --- = ------ : ---
+     f    α->β     x     α     fx       β
+
+Here's the justification:
+
+        (\FXk.F(\f.X(\x.k(fx)))) (\k.g(kf)) (\k.h(kx)) 
+    ~~> (\Xk.(\k.g(kf))(\f.X(\x.k(fx)))) (\k.h(kx))
+    ~~> \k.(\k.g(kf))(\f.(\k.h(kx))(\x.k(fx)))
+    ~~> \k.g((\f.(\k.h(kx))(\x.k(fx)))f)
+    ~~> \k.g((\k.h(kx))(\x.k(fx)))
+    ~~> \k.g(h(\x.k(fx))x)
+    ~~> \k.g(h(k(fx)))
+
+Then 
+                          (\ks.k(ks))[] 
+    shift = \k.k(k("")) = -------------
+                               ""
+
+Let 2 == \ks.k(ks).
+
+so aSc lifted into the monad is
+
+    []     2[]   []      
+    -- ¢ ( --- ¢ --- ) = 
+    a      ""    c       

 
 First, we need map2 instead of map1.  Second, the type of the shift
 operator will be a string continuation, rather than a function from
 string continuations to string continuations.
 
 
 First, we need map2 instead of map1.  Second, the type of the shift
 operator will be a string continuation, rather than a function from
 string continuations to string continuations.
 

+(\k.k(k1))(\s.(\k.k(k2))(\r.sr))
+(\k.k(k1))(\s.(\r.sr)((\r.sr)2))
+(\k.k(k1))(\s.(\r.sr)(s2))
+(\k.k(k1))(\s.s(s2))
+(\s.s(s2))((\s.s(s2))1)
+(\s.s(s2))(1(12))
+(1(12))((1(12)2))
+
+
+
+
+

 But here's the interesting part: from the point of view of the shift
 operator, the continuation that it will be fed will be the entire rest
 of the computation.  This includes not only what has come before, but
 But here's the interesting part: from the point of view of the shift
 operator, the continuation that it will be fed will be the entire rest
 of the computation.  This includes not only what has come before, but


@@ -322,3 +446,4 @@ Super cool.
 
 
 
 
 
 

+"*the* continuation monad"