edits

diff --git a/topics/_week14_continuations.mdwn b/topics/_week14_continuations.mdwn
index 0b99065..42f2c11 100644 (file)
--- a/topics/_week14_continuations.mdwn
+++ b/topics/_week14_continuations.mdwn
@@ -65,7 +65,7 @@ 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
 
 monad using mid (`⇧`), then combine them using monadic function
 application, where
 

-    ¢ mf mx = \k -> mf (\f -> mx (\a -> k(f x)))
+    ¢ M N = \k -> M (\f -> N (\a -> k(f x)))

 
 for the continuation monad.
 
 
 for the continuation monad.
 


@@ -73,17 +73,16 @@ 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, 
 
 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
+    t1 = mt1 I

 
 That is, the original computation is the monadic version applied to
 the trivial continuation.
 
 
 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:
+We can now add 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))
 
 
     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
 


@@ -96,7 +95,7 @@ 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
 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.
+twice.  The expression `\s.k(ks)` is just the composition of k with itself.

 
     mt2 I == "ababd"
 
 
     mt2 I == "ababd"
 


@@ -118,19 +117,26 @@ For a reset operator #, we can have
 
     # u k = k(u(\k.k))   -- ex.: ab#deSf ~~> abdedef
 
 
     # u k = k(u(\k.k))   -- ex.: ab#deSf ~~> abdedef
 

+The reset operator executes the remainder of the list separately, by
+giving it the trivial continuation (\k.k), then feeds the result to
+the continuation corresponding to the position of the reset.
+

 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.
 
 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.
 

+## Generalizing to the tree doubling task
+

 Now we should consider what happens when we write a shift operator
 that takes the place of a single letter.
 
     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
     mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d))
 
 Now we should consider what happens when we write a shift operator
 that takes the place of a single letter.
 
     mt2 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ ⇧d))
     mt4 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ shift' ¢ ⇧d))
 

-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'.
+Instead of mt2 (copied from above), we have mt4.  So now the type of a
+leaf (a boxed string, type M[Char]) is the same as the type of the new
+shift operator, shift'.

 
     shift' = \k.k(k"")
 
 
     shift' = \k.k(k"")
 


@@ -179,6 +185,7 @@ 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:
 
 the shift' operator sees as its argument k by replacing ⇧ and ¢ with
 their definitions:
 

+<pre>

       ⇧+ ¢ ⇧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
       ⇧+ ¢ ⇧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


@@ -199,106 +206,14 @@ their definitions:
    ~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
    = shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
    ~~> shift(\x.(+a)((+x)c))
    ~~> shift(\x.⇧c(\x'.(+a)((+x)x'))))
    = shift(\x.(\k.kc)(\x'.(+a)((+x)x'))))
    ~~> shift(\x.(+a)((+x)c))

+</pre>

 
 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
 
 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.
-
-(\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
-what will come after it as well.  That means when the continuation is
-doubled (self-composed), the result duplicates not only the prefix
-`(ab ~~> abab)`, but also the suffix `(d ~~> dd)`.  In some sense, then,
-continuations allow functions to see into the future!
-
-What do you expect will be the result of executing "aScSe" under the
-second perspective?  The answer to this question is not determined by
-the informal specification of the task that we've been using, since
-under the new perspective, we're copying complete (bi-directional)
-contexts rather than just left contexts.  
-
-It might be natural to assume that what execution does is choose an S,
-and double its context, temporarily treating all other shift operators
-as dumb letters, then choosing a remaining S to execute.  If that was
-our interpreation of the task, then no string with more than one S
-would ever terminate, since the number S's after each reduction step
-would always be 2(n-1), where n is the number before reduction.
-
-But there is another equally natural way to answer the question.
-Assume the leftmost S is executed first.  What will the value of its
-continuation k be?  It will be a function that maps a string s to the
-result of computing `ascSe`, which will be `ascascee`.  So `k(k "")`
-will be `k(acacee)`, which will result in `a(acacee)ca(acacee)cee`
-(the parentheses are added to show stages in the construction of the
-final result).
-
-So the continuation monad behaves in a way that we expect a
-continuation to behave.  But where did the continuation monad come
-from?  Let's consider some ways of deriving the continuation monad.
+lambda conversion.  We'll see how to understand what is going on
+when we talk about quantifier raising in the next lecture.

 
 ## Viewing Montague's PTQ as CPS
 
 
 ## Viewing Montague's PTQ as CPS
 


@@ -325,80 +240,6 @@ quantificational DPs, as in *John and no dog left*.  Then generalized
 quantifier corresponding to the proper name *John* is the quantifier
 `\k.kj`.
 
 quantifier corresponding to the proper name *John* is the quantifier
 `\k.kj`.
 

-At this point, we have a type for our Kliesli arrow and a value for
-our mid.  Given some result type (such as `t` in the Montague application),
-
-    α ==> (α -> ρ) -> ρ
-    ⇧a = \k.ka    
-
-It remains only to find a suitable value for bind.  Montague didn't
-provide one, but it's easy to find:
-
-    bind ::    Mα -> (α -> Mβ) -> Mβ
-
-given variables of the following types
-
-    u :: Mα == (α -> ρ) -> ρ
-    f :: α -> Mβ
-    k :: β -> ρ
-    x :: α
-
-We have
-
-    bind u f = \k.u(\x.fxk)
-
-Let's carefully make sure that this types out:
-
-    bind u f = \k.       u      (\x .   f       x     k)
-                                      --------  --
-                                      α -> Mβ   α
-                                     ------------  ------
-                                         Mβ        β -> ρ
-                                  --  --------------------
-                                  α            ρ
-                  -------------  ------------------------
-                  (α -> ρ) -> ρ             α -> ρ
-                  ---------------------------------
-                                ρ
-                -----------------------
-                    (β -> ρ) -> ρ
-
-Yep!
-
-Is there any other way of building a bind operator?  Well, the
-challenge is getting hold of the "a" that is buried inside of `u`.
-In the Reader monad, we could get at the a inside of the box by
-applying the box to an environment.  In the State monad, we could get
-at the a by applying to box to a state and deconstructing the
-resulting pair.  In the continuation case, the only way to do it is to
-apply the boxed a (i.e., u) to a function that takes an a as an
-argument.  That means that f must be invoked inside the scope of the
-functional argument to u.  So we've deduced the structure
-
-    ... u (\x. ... f x ...) ...
-
-At this point, in order to provide u with an argument of the
-appropriate type, the argument must not only take objects of type 
-α as an argument, it must return a result of type ρ.  That means that
-we must apply fx to an object of type β -> ρ.  We can hypothesize such
-an object, as long as we eliminate that hypothesis later (by binding
-it), and we have the complete bind operation.
-
-The way in which the value of type α that is needed in order to unlock
-the function f is hidden inside of u is directly analogous to the
-concept of "data hiding" in object-oriented programming.  See Pierce's
-discussion of how to extend system F with existential type
-quantification by encoding the existential using continuations.
-
-So the Kliesli type pretty much determines the bind operation.
-
-## What continuations are doing
-
-Ok, we have a continuation monad.  We derived it from first
-principles, and we have seen that it behaves at least in some respects
-as we expect a continuation monad to behave (in that it allows us to
-give a good implementation of the task).
-

 ## How continuations can simulate other monads
 
 Because the continuation monad allows the result type ρ to be any
 ## How continuations can simulate other monads
 
 Because the continuation monad allows the result type ρ to be any


@@ -434,16 +275,3 @@ is return Nothing.
 
 Super cool.
 
 
 Super cool.
 

-
-
-
-## Delimited versus undelimited continuations
-
-## Natural language requries delimited continuations
-
-
-
-
-
-
-"*the* continuation monad"