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
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:β).
+## Not quite a monad
+
To demonstrate that this is indeed the continuation monad's ¢
operator:
== ------
fx
-Not a monad (Wadler); would be if the types were
+However, these continuations do not form an official monad. The
+reason is that (see Wadler's paper `Composable continuations' for details).
+
Neverthless, obeys the monad laws.
Oh, one more thing: because natural language allows the functor to be