From 935fb6c127006b69a492ef8e04cdb52a44e88169 Mon Sep 17 00:00:00 2001
From: Chris
Date: Tue, 12 May 2015 09:08:24 0400
Subject: [PATCH] last lecture

topics/_week14_continuations.mdwn  295 ++++++++++++++
topics/_week15_continuation_applications.mdwn  377 ++++++++++++++++++++++++++
2 files changed, 587 insertions(+), 85 deletions()
create mode 100644 topics/_week15_continuation_applications.mdwn
diff git a/topics/_week14_continuations.mdwn b/topics/_week14_continuations.mdwn
index bb682603..0b99065f 100644
 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 orderindependent 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
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))
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 lefttoright 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.
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 oneplace operation. If we decompose this
operation into a twoplace 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 bynow 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 constructionit 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 inputif 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 oneshift 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.
+(\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
@@ 322,3 +446,4 @@ Super cool.
+"*the* continuation monad"
diff git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
new file mode 100644
index 00000000..eeb397be
 /dev/null
+++ b/topics/_week15_continuation_applications.mdwn
@@ 0,0 +1,377 @@
+
+[[!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 elementthe 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 continuationbased 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.
+
+Instead, we'll reinterpreting what the continuation monad was doing
+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: scopetaking
+
+We have seen that continuations allow a deeplyembedded 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 scopetaking 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 onsee 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 scopetaking 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
+
+The yield of this tree (the sequence of leaf nodes) is aadadeedaadadeedee.
+
+Exercise: the result is different, by the way, if the QR occurs in a
+different order.
+
+Three lessons:
+
+* Generalizing from onesided, listbased continuation
+ operators to twosided, treebased 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 twosided, treebased 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 finegrained 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 atissue (premonadic) computation with a layer at which
+sideeffects occur.
+
+The tower notation is a precise way of articulating continuationbased
+computations into a payload and (potentially multiple) layers of sideeffects.
+We won't keep the outer box, but we will keep the horizontal line
+dividing main effects from sideeffects.
+
+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 simplytyped 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 typeshifters for
+determiner phrases. Importantly, LIFT applied to an
+individualdenoting expression yields the generalized quantifier
+proposed by Montague as the denotation for proper names:
+
+ [] SS
+ 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
+
+Not a monad (Wadler); would be if the types were
+Neverthless, obeys the monad laws.
+
+This is (almost) all we need to get some significant linguistic work
+done.
+

2.11.0