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
space:
<pre>
- _______________ _______________ _______________
+ _______________ _______________ _______________
| [x->2, y->3] | | [x->2, y->3] | | [x->2, y->3] |
------------------- ------------------ ------------------
| | ¢ | | = | |
- | +2 | | y | | 5 |
- |______________| |______________| |______________|
+ | +2 | | y | | 5 |
+ |______________| |______________| |______________|
</pre>
For people who are familiar with Discourse Representation Theory (Kamp
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:
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
+ [] 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.