author Chris Tue, 12 May 2015 13:08:24 +0000 (09:08 -0400) committer Chris Tue, 12 May 2015 13:08:24 +0000 (09:08 -0400)
 topics/_week14_continuations.mdwn patch | blob | history topics/_week15_continuation_applications.mdwn [new file with mode: 0644] patch | blob

index bb68260..0b99065 100644 (file)
@@ -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.
+and show how it solves the task, then generalize the task to
+include doubling of both the left and the right context.

-Let's take a look at some of our favorite monads from the point of
-view of types.  Here, `==>` is the Kleisli arrow.
-
-                  ⇧: \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
-
-We lift the computation `("a" ++ ("b" ++ ("c" ++ "d")))` into
-
-    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 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
+
+    mt1 = ⇧+ ¢ ⇧a ¢ (⇧+ ¢ ⇧b ¢ (⇧+ ¢ ⇧c ¢ ⇧d))
+
+We have to lift each functor (+) and each object (e.g., "b") into the
+application, where
+
+    ¢ mf mx = \k -> mf (\f -> mx (\a -> k(f x)))
+
+
+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.
+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:
+
+
+    \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.

diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
new file mode 100644 (file)
index 0000000..eeb397b
--- /dev/null
@@ -0,0 +1,377 @@
+<!-- λ ◊ ≠ ∃ Λ ∀ ≡ α β γ ρ ω φ ψ Ω ○ μ η δ ζ ξ ⋆ ★ • ∙ ● ⚫ 𝟎 𝟏 𝟐 𝟘 𝟙 𝟚 𝟬 𝟭 𝟮 ⇧ (U+2e17) ¢ -->
+[[!toc]]
+
+# Applications of continuations to natural language
+
+We've seen a number of applications of monads to natural language,
+including presupposition projection, binding, intensionality, and the
+dynamics of the GSV fragment.
+
+In the past couple of weeks, we've introduced continuations, first as
+a functional programming technique, then in terms of list and tree
+zippers, then as a monad.  In this lecture, we will generalize
+continuations slightly beyond a monad, and then begin to outline some
+of the applications of monads.  In brief, the generalization can be
+summarized in terms of types: instead of using a Kleisli arrow mapping
+a type α to a continuized type α -> ρ -> ρ, we'll allow the result
+types to differ, i.e., we'll map α to α -> β -> γ.  This will be
+crucial for some natural language applications.
+
+Many (though not all) of the applications are discussed in detail in
+Barker and Shan 2014, *Continuations in Natural Language*, OUP.
+
+In terms of list zippers, the continuation of a focussed element in
+the list is the front part of the list.
+
+    list zipper for the list [a;b;c;d;e;f] with focus on d:
+
+        ([c;b;a], [d;e;f])
+         -------
+     defunctionalized
+     continuation
+
+In terms of tree zippers, the continuation is the entire context of
+the focussed element--the entire rest of the tree.
+
+[drawing of a broken tree]
+
+Last week we had trouble computing the doubling task when there was more
+than one shifty operator after moving from a list perspective to a
+tree perspective.  That is, it remained unclear why "aScSe" was
+
+    "aacaceecaacaceecee"
+
+We'll burn through that conceptual fog today.  The natural thing to
+try would have been to defunctionalize the continuation-based solution
+using a tree zipper.  But that would not have been easy, since the
+natural way to implement the doubling behavior of the shifty operator
+would have been to simply copy the context provided by the zipper.
+This would have produced two uncoordinated copies of the other shifty
+operator, and we'd have been in the situation described in class of
+having a reduction strategy that never reduced the number of shifty
+operators below 2.
+
+in defunctionalized terms by using Quantifier Raising (a technique
+from linguistics).
+
+But first, motivating quantifier scope as a linguistic application.
+
+# The primary application of continuations to natural language: scope-taking
+We have seen that continuations allow a deeply-embedded element to
+take control over (a portion of) the entire computation that contains
+it.  In natural language semantics, this is exactly what it means for
+a scope-taking expression to take scope.
+
+    1. [Ann put a copy of [everyone]'s homeworks in her briefcase]
+
+    2. For every x, [Ann put a copy of x's homeworks in her briefcase]
+
+The sentence in (1) can be paraphrased as in (2), in which the
+quantificational DP *every student* takes scope over the rest of the sentence.
+Even if you suspect that there could be an analysis of (2) on which
+"every student's term paper" could denote some kind of mereological
+fusion of a set of papers, it is much more difficult to be satisfied
+with a referential analysis when *every student* is replaced with
+*no student*, or *fewer than three students*, and so on---see any
+semantics text book for abundant discussion.
+
+We can arrive at an analysis by expressing the meaning of
+quantificational DP such as *everyone* using continuations:
+
+    3. everyone = shift (\k.∀x.kx)
+
+Assuming there is an implicit reset at the top of the sentence (we'll
+explicitly address determining where there is or isn't a reset), the
+reduction rules for `shift` will apply the handler function (\k.∀x.kx)
+to the remainder of the sentence after abstracting over the position
+of the shift expression:
+
+    [Ann put a copy of [shift (\k.∀x.kx)]'s homeworks in her briefcase]
+    ~~> (\k.∀x.kx) (\v. Ann put a copy of v's homeworks in her briefcase)
+    ~~> ∀x. Ann put a copy of x's homeworks in her briefcase
+
+(To be a bit pedantic, this reduction sequence is more suitable for
+shift0 than for shift, but we're not being fussy here about subflavors
+of shifty operators.)
+
+The standard technique for handling scope-taking in linguistics is
+Quantifier Raising (QR).  As you might suppose, the rule for Quantifier
+Raising closely resembles the reduction rule for shift:
+
+    Quantifier Raising: given a sentence [... [QDP] ...], build a new
+    sentence [QDP (\x.[... [x] ...])].
+
+Just to emphasize the similarity between QR and shift, we can use QR
+to provide insight into the tree task that mystified us earlier.
+
+\tree (. (a)((S)((d)((S)(e)))))
+
+  .
+__|___
+|    |
+a  __|___
+   |    |
+   S  __|__
+      |   |
+      d  _|__
+         |  |
+         S  e
+
+First we QR the lower shift operator
+
+\tree (. (S) ((\\x) ((a)((S)((d)((x)(e)))))))
+
+   .
+___|___
+|     |
+S  ___|___
+   |     |
+   \x  __|___
+       |    |
+       a  __|___
+          |    |
+          S  __|__
+             |   |
+             d  _|__
+                |  |
+                x  e
+
+Next, we QR the upper shift operator
+
+\tree (. (S) ((\\y) ((S) ((\\x) ((a)((y)((d)((x)(e)))))))))
+
+   .
+___|___
+|     |
+S  ___|____
+   |      |
+   \y  ___|___
+       |     |
+       S  ___|___
+          |     |
+          \x  __|___
+              |    |
+              a  __|___
+                 |    |
+                 y  __|__
+                    |   |
+                    d  _|__
+                       |  |
+                       x  e
+
+We then evaluate, using the same value for the shift operator proposed before:
+
+    shift = \k.k(k "")
+
+It will be easiest to begin evaluating this tree with the lower shift
+operator (we get the same result if we start with the upper one).
+The relevant value for k is (\x.a(y(d(x e)))).  Then k "" is
+a(y(d(""(e)))), and k(k "") is a(y(d((a(y(d(""(e)))))(e)))).  In tree
+form:
+
+\tree (. (S) ((\\y) ((a)((y)((d)(((a)((y)((d)(("")(e)))))(e)))))))
+
+   .
+___|___
+|     |
+S  ___|____
+   |      |
+   \y  ___|___
+       |     |
+       a  ___|___
+          |     |
+          y  ___|___
+             |     |
+             d  ___|___
+                |     |
+              __|___  e
+              |    |
+              a  __|___
+                 |    |
+                 y  __|___
+                    |    |
+                    d  __|__
+                       |   |
+                       ""  e
+
+
+Repeating the process for the upper shift operator replaces each
+occurrence of y with a copy of the whole tree.
+
+\tree (. ((a)((((a)(("")((d)(((a)(("")((d)(("")(e)))))(e))))))((d)(((a)((((a)(("")((d)(((a)(("")((d)(("")(e)))))(e))))))((d)(("")(e)))))(e))))))
+
+      .
+      |
+______|______
+|           |
+a  _________|__________
+   |                  |
+   |               ___|___
+___|___            |     |
+|     |            d  ___|____
+a  ___|____           |      |
+   |      |        ___|____  e
+   ""  ___|___     |      |
+       |     |     a  ____|_____
+       d  ___|___     |        |
+          |     |     |      __|___
+       ___|___  e  ___|___   |    |
+       |     |     |     |   d  __|__
+       a  ___|___  a  ___|____  |   |
+          |     |     |      |  ""  e
+          ""  __|___  ""  ___|___
+              |    |      |     |
+              d  __|__    d  ___|___
+                 |   |       |     |
+                 ""  e    ___|___  e
+                          |     |
+                          a  ___|___
+                             |     |
+                             ""  __|___
+                                 |    |
+                                 d  __|__
+                                    |   |
+                                    ""  e
+
+
+Exercise: the result is different, by the way, if the QR occurs in a
+different order.
+
+Three lessons:
+
+* Generalizing from one-sided, list-based continuation
+  operators to two-sided, tree-based continuation operators is a
+  dramatic increase in power and complexity.
+
+* Operators that
+  compose multiple copies of a context can be hard to understand.
+
+* When considering two-sided, tree-based continuation operators,
+  quantifier raising is a good tool for visualizing (defunctionalizing)
+  the computation.
+
+## Tower notation
+
+At this point, we have three ways of representing computations
+involving control operators such as shift and reset: using a CPS
+transform, lifting into a continuation monad, and by using QR.
+
+QR is the traditional system in linguistics, but it will not be
+adequate for us in general.  The reason has to do with order.  As
+we've discussed, especially with respect to the CPS transform,
+continuations allow fine-grained control over the order of evaluation.
+One of the main empirical claims of Barker and Shan 2014 is that
+natural language is sensitive to evaluation order.  Unlike other
+presentations of continuations, QR does not lend itself to reasoning
+about evaluation order, so we will need to use a different strategy.
+
+[Note to self: it is interesting to consider what it would take to
+reproduce the analyses giving in Barker and Shan in purely QR terms.
+Simple quantificational binding using parasitic scope should be easy,
+but how reconstruction would work is not so clear.]
+
+We'll present tower notation, then comment and motivate several of its
+features as we consider various applications.  For now, we'll motivate
+the tower notation by thinking about box types.  In the discussion of
+monads, we've thought of monadic types as values inside of a box.  The
+box will often contain information in addition to the core object.
+For instance, in the Reader monad, a boxed int contains an expression
+of type int as the payload, but also contains a function that
+manipulates a list of information.  It is natural to imagine
+separating a box into two regions, the payload and the hidden scratch
+space:
+
+    _______________               _______________           _______________
+    | [x->2, y->3] |             | [x->2, y->3] |          | [x->2, y->3] |
+  -------------------          ------------------         ------------------
+    |              |     ¢        |              |    =     |              |
+    |    +2        |             |     y        |          |     5        |
+    |______________|             |______________|          |______________|
+
+
+(Imagine the + operation has been lifted into the Reader monad too.)
+
+For people who are familiar with Discourse Representation Theory (Kamp
+1981, Kamp and Reyle 1993), this separation of boxes into payload and
+discourse scorekeeping will be familiar (although many details differ).
+
+The general pattern is that monadic treatments separate computation
+into an at-issue (pre-monadic) computation with a layer at which
+side-effects occur.
+
+The tower notation is a precise way of articulating continuation-based
+computations into a payload and (potentially multiple) layers of side-effects.
+We won't keep the outer box, but we will keep the horizontal line
+dividing main effects from side-effects.
+
+Tower convention for types:
+                                              γ | β
+    (α -> β) -> γ can be equivalently written -----
+                                                α
+
+Tower convention for values:
+                                           g[]
+    \k.g[k(x)] can be equivalently written ---
+                                            x
+
+If \k.g[k(x)] has type (α -> β) -> γ, then k has type (α -> β).
+
+Here "g[ ]" is a *context*, that is, an expression with (exactly) one
+hole in it.  For instance, we might have g[x] = \forall x.P[x].
+
+We'll use a simply-typed system with two atomic types, DP (the type of
+individuals) and S (the type of truth values).
+
+Then in the spirit of monadic thinking, we'll have a way of lifting an
+arbitrary value into the tower system:
+
+                                           []    γ|β
+    LIFT (x:α) = \k.kx : (α -> β) -> γ ==  --- : ---
+                                           x      α
+
+Obviously, LIFT is exactly the midentity (the unit) for the continuation monad.
+The name comes from Partee's 1987 theory of type-shifters for
+determiner phrases.  Importantly, LIFT applied to an
+individual-denoting expression yields the generalized quantifier
+proposed by Montague as the denotation for proper names:
+
+                                            []   S|S
+    LIFT (j:DP) = \k.kx : (DP -> S) -> S == -- : ---
+                                            j    DP
+
+So if the proper name *John* denotes the individual j, LIFT(j) is the
+generalized quantifier that maps each property k of type DP -> S to true
+just in case kj is true.
+
+Once we have expressions of type (α -> β) -> γ, we'll need to combine
+them.  We'll use the ¢ operator from the continuation monad:
+
+    g[]    γ | δ      h[]   δ | ρ    g[h[]]   γ | ρ
+    --- : -------  ¢  --- : ----- == ------ : -----
+    f     α -> β      x       α        fx       β
+
+Note that the types below the horizontal line combine just like
+functional application (i.e, f:(α->β) (x:α) = fx:β).
+
+To demonstrate that this is indeed the continuation monad's ¢
+operator:
+
+      ¢ (\k.g[kf]) (\k.h[kx])
+    = (\MNk.M(\m.N(\n.k(mn)))) (\k.g[kf]) (\k.h[kx])
+    ~~> \k.(\k.g[kf])(\m.(\k.h[kx])(\n.k(mn))
+    ~~> \k.g[(\k.h[kx])(\n.k(fn))
+    ~~> \k.g[h[k(fx)]]
+
+       g[h[]]
+    == ------
+         fx
+