X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek14_continuations.mdwn;h=42f2c1180d924d655c74f3ff1b3936e0d569ac51;hp=0000000000000000000000000000000000000000;hb=30e80630a4bdb0ec23dd7098f735b060f6a3de0f;hpb=1efbaa05ade48388ad996f60091c9b6f8bc58c1d;ds=sidebyside

diff --git a/topics/week14_continuations.mdwn b/topics/week14_continuations.mdwn
new file mode 100644
index 00000000..42f2c118
--- /dev/null
+++ b/topics/week14_continuations.mdwn
@@ -0,0 +1,277 @@
+<!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
+
+[[!toc]]
+
+# Continuations
+
+Last week we saw how to turn a list zipper into a continuation-based
+list processor.  The function computed something we called "the task",
+which was a simplified langauge involving control operators.
+
+    abSdS ~~> ababdS ~~> ababdababd
+
+The task is to process the list from left to right, and at each "S",
+double the list so far.  Here, "S" is a kind of control operator, and
+captures the entire previous computation.  We also considered a
+variant in which '#' delimited the portion of the list to be copied:
+
+    ab#deSfg ~~> abededfg
+
+In this variant, "S" and "#" correspond to `shift` and `reset`, which
+provide access to delimited continuations.
+
+The expository logic of starting with this simplified task is the
+notion that as lists are to trees, so is this task to full-blown
+continuations.  So to the extent that, say, list zippers are easier to
+grasp than tree zippers, the task is easier to grasp than full
+continuations.
+
+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
+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
+
+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
+
+    ¢ M N = \k -> M (\f -> N (\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 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))
+
+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 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.  The expression `\s.k(ks)` is just the composition of k with itself.
+
+    mt2 I == "ababd"
+
+just as desired.
+
+Let's just make sure that we have the left-to-right evaluation we were
+hoping for by evaluating "abSdeSf":
+
+    mt3 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (shift ¢ (⇧+ ¢ ⇧d ¢ (⇧+ ¢ ⇧e ¢ (shift ⇧f)))))
+
+Then
+
+    mt3 I = "ababdeababdef"   -- structure: (ababde)(ababde)f
+             
+
+As expected.
+
+For a reset operator #, we can have 
+
+    # 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.
+
+## 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))
+
+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"")
+
+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:
+
+<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
+   ~~> (\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))
+</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
+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
+
+Montague's conception of determiner phrases as generalized quantifiers
+is a limited form of continuation-passing.  (See, e.g., chapter 4 of
+Barker and Shan 2014.)  Start by assuming that ordinary DPs such as
+proper names denote objects of type `e`.  Then verb phrases denote
+functions from individuals to truth values, i.e., functions of type `e
+-> t`.
+
+The meaning of extraordinary DPs such as *every woman* or *no dog*
+can't be expressed as a simple individual.  As Montague argued, it
+works much better to view them as predicates on verb phrase meanings,
+i.e., as having type `(e->t)->t`.  Then *no woman left* is true just
+in case the property of leaving is true of no woman:
+
+    no woman:  \k.not \exists x . (woman x) & kx
+    left: \x.left x
+    (no woman) (left) = not \exists x . woman x & left x
+
+Montague also proposed that all determiner phrases should have the
+same type.  After all, we can coordinate proper names with
+quantificational DPs, as in *John and no dog left*.  Then generalized
+quantifier corresponding to the proper name *John* is the quantifier
+`\k.kj`.
+
+## How continuations can simulate other monads
+
+Because the continuation monad allows the result type ρ to be any
+type, we can choose ρ in clever ways that allow us to simulate other
+monads.
+
+    Reader: ρ = env -> α
+    State: ρ = s -> (α, s)
+    Maybe: ρ = Just α | Nothing
+
+You see how this is going to go.  Let's see an example by adding an
+abort operator to our task language, which represents what
+we want to have happen if we divide by zero, where what we want to do
+is return Nothing.
+
+    abort k = Nothing
+    mid a k = k a
+    map2 f u v k = u(\u' -> v (\v' -> k(f u' v'))) 
+    t13 = map2 (++) (mid "a")
+                   (map2 (++) (mid "b")
+                              (map2 (++) (mid "c")
+		 	                 (mid "d")))
+
+    t13 (\k->Just k) == Just "abcd"
+
+    t14 = map2 (++) (mid "a")
+                   (map2 (++) abort
+                              (map2 (++) (mid "c")
+		 	                 (mid "d")))
+
+
+    t14 (\k->Just k) == Nothing
+
+Super cool.
+