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
+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
+In terms of list zippers, the continuation of a focused 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:
continuation
In terms of tree zippers, the continuation is the entire context of
-the focussed element--the entire rest of the tree.
+the focused element--the entire rest of the tree.
[drawing of a broken tree]
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.
+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.
+operators below 2. (There are ways around this limitation of tree zippers,
+but they are essentially equivalent to the technique given just below.)
Instead, we'll re-interpreting what the continuation monad was doing
-in defunctionalized terms by using Quantifier Raising (a technique
-from linguistics).
+in more or less defunctionalized terms by using Quantifier Raising, a technique
+from linguistics.
But first, motivating quantifier scope as a linguistic application.
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.
+quantificational DP *everyone* 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
Quantifier Raising: given a sentence [... [QDP] ...], build a new
sentence [QDP (\x.[... [x] ...])].
+Here, QDP is a scope-taking quantificational DP.
+
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)))))
+-->
+<pre>
.
__|___
| |
d _|__
| |
S e
+</pre>
-First we QR the lower shift operator
+First we QR the lower shift operator, replacing it with a variable and
+abstracting over that variable.
+<!--
\tree (. (S) ((\\x) ((a)((S)((d)((x)(e)))))))
+-->
+<pre>
.
___|___
| |
d _|__
| |
x e
+</pre>
Next, we QR the upper shift operator
+<!--
\tree (. (S) ((\\y) ((S) ((\\x) ((a)((y)((d)((x)(e)))))))))
+-->
+<pre>
.
___|___
| |
d _|__
| |
x e
+</pre>
We then evaluate, using the same value for the shift operator proposed before:
- shift = \k.k(k "")
+ S = 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).
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)))))))
+-->
+<pre>
.
___|___
| |
d __|__
| |
"" e
+</pre>
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))))))
+-->
+<pre>
.
|
______|______
d __|__
| |
"" e
+</pre>
-The yield of this tree (the sequence of leaf nodes) is aadadeedaadadeedee.
+The yield of this tree (the sequence of leaf nodes) is
+aadadeedaadadeedee, which is the expected output of the double-shifted tree.
-Exercise: the result is different, by the way, if the QR occurs in a
-different order.
+Exercise: the result is different, by the way, if the QR occurs in the
+opposite order.
Three lessons:
dramatic increase in power and complexity.
* Operators that
- compose multiple copies of a context can be hard to understand.
+ compose multiple copies of a context can be hard to understand
+ (though keep this in mind when we see the continuations-based
+ analysis of coordination, which involves context doubling).
* When considering two-sided, tree-based continuation operators,
quantifier raising is a good tool for visualizing (defunctionalizing)
Simple quantificational binding using parasitic scope should be easy,
but how reconstruction would work is not so clear.]
+## Introducting the tower notation
+
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
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] |
- ------------------- ------------------ ------------------
+<pre>
+ _______________ _______________ _______________
+ | [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.)
+ | +2 | | y | | 5 |
+ |______________| |______________| |______________|
+</pre>
For people who are familiar with Discourse Representation Theory (Kamp
1981, Kamp and Reyle 1993), this separation of boxes into payload and
dividing main effects from side-effects.
Tower convention for types:
+<pre>
γ | β
(α -> β) -> γ can be equivalently written -----
α
+</pre>
Tower convention for values:
+<pre>
g[]
\k.g[k(x)] can be equivalently written ---
x
+</pre>
If \k.g[k(x)] has type (α -> β) -> γ, then k has type (α -> β).
We'll use a simply-typed system with two atomic types, DP (the type of
individuals) and S (the type of truth values).
+## LIFT
+
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 α
+ [] β|β
+ 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
+Notice that LIFT requires the result type of the continuation argument
+and the result type of the overall expression to match (here, both are β).
+
+The name LIFT 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:
generalized quantifier that maps each property k of type DP -> S to true
just in case kj is true.
+Crucially for the discussion here, LIFT does not apply only to DPs, as
+in Montague and Partee, but to any expression whatsoever. For
+instance, here is LIFT applied to a lexical verb phrase:
+
+ [] S|S
+ LIFT (left:DP->S) = \k.kx : ((DP->S) -> S) -> S == ---- : ---
+ left DP
+
Once we have expressions of type (α -> β) -> γ, we'll need to combine
them. We'll use the ¢ operator from the continuation monad:
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:
+## Not quite a monad
+
+The unit and the combination rule work very much like we are used to
+from the various monads we've studied.
+
+In particular, we can easily see that the ¢ operator defined just
+above is exactly the same as the ¢ operator from the continuation monad:
¢ (\k.g[kf]) (\k.h[kx])
= (\MNk.M(\m.N(\n.k(mn)))) (\k.g[kf]) (\k.h[kx])
== ------
fx
-Not a monad (Wadler); would be if the types were
-Neverthless, obeys the monad laws.
+However, these continuations do not form an official monad.
+One way to see this is to consider the type of the bind operator.
+The type of the bind operator in a genuine monad is
+
+ mbind : Mα -> (α -> Mβ) -> Mβ
+
+In particular, the result type of the second argument (Mβ) must be
+identical to the result type of the bind operator overall. For the
+continuation monad, this means that mbind has the following type:
+
+ ((α -> γ) -> ρ)
+ -> α -> ((β -> δ) -> ρ)
+ -> ((β -> δ) -> ρ)
+
+But the type of the bind operator in our generalized continuation
+system (call it "kbind") is
+
+ kbind :
+ ((α -> γ) -> ρ)
+ -> α -> ((β -> δ) -> γ)
+ -> ((β -> δ) -> ρ)
+
+Note that `(β -> δ) -> γ` is not the same as `(β -> δ) -> ρ`.
+
+ kbind u f = \k. u (\x. f x k )
+ β->δ (α->γ)->ρ α α->(β->δ)->γ α β->δ
+ -----------------
+ (β->δ)->γ
+ ------------------------
+ γ
+ -------------------
+ α->γ
+ ---------------------
+ ρ
+ --------------
+ (β->δ)->ρ
+
+See Wadler's paper `Composable continuations' for discussion.
+
+Neverthless, it's easy to see that the generalized continuation system
+obeys the monad laws. We haven't spent much time proving monad laws,
+so this seems like a worthy occasion on which to give some details.
+Since we're working with bind here, we'll use the version of the monad
+laws that are expressed in terms of bind:
+
+ Prove u >>= ⇧ == u:
+
+ u >>= (\ak.ka)
+ == (\ufk.u(\x.fxk)) u (\ak.ka)
+ ~~> \k.u(\x.(\ak.ka)xk)
+ ~~> \k.u(\x.kx)
+ ~~> \k.uk
+ ~~> u
+
+The last two steps are eta reductions.
+
+ Prove ⇧a >>= f == f a:
+
+ ⇧a >>= f
+ == (\ak.ka)a >>= f
+ ~~> (\k.ka) >>= f
+ == (\ufk.u(\x.fxk)) (\k.ka) f
+ ~~> \k.(\k.ka)(\x.fxk)
+ ~~> \k.fak
+ ~~> fa
+
+ Prove u >>= (\a.fa >>= g) == (u >>= f) >>= g:
+
+ u >>= (\a.fa >>= g)
+ == u >>= (\a.(\k.fa(\x.gxk)))
+ == (\ufk.u(\x.fxk)) u (\a.(\k.fa(\x.gxk)))
+ == \k.u(\x.(\a.(\k.fa(\x.gxk)))xk)
+ ~~> \k.u(\x.fx(\y.gyk))
+
+ (u >>= f) >>= g
+ == (\ufk.u(\x.fxk)) u f >>= g
+ ~~> (\k.u(\x.fxk)) >>= g
+ == (\ufk.u(\x.fxk)) (\k.u(\x.fxk)) g
+ ~~> \k.(\k.u(\x.fxk))(\y.gyk)
+ ~~> \k.u(\x.fx(\y.gyk))
+
+## Syntactic refinements: subtypes of implication
+
+Because natural language allows the functor to be on the left or on
+the right, we replace the type arrow -> with a left-leaning version \
+and a right-leaning version, as follows:
+
+ α/β β = α
+ β β\α = α
+
+This means (without adding some fancy footwork, as in Charlow 2014) we
+need two versions of ¢ too, one for each direction for the unmonadized types.
+
+\\ //
+
+
This is (almost) all we need to get some significant linguistic work
done.