```  .
__|___
|    |
a  __|___
|    |
S  __|__
|   |
d  _|__
|  |
S  e
```
First we QR the lower shift operator, replacing it with a variable and abstracting over that variable.
```   .
___|___
|     |
S  ___|___
|     |
\x  __|___
|    |
a  __|___
|    |
S  __|__
|   |
d  _|__
|  |
x  e
```
Next, we QR the upper shift operator
```   .
___|___
|     |
S  ___|____
|      |
\y  ___|___
|     |
S  ___|___
|     |
\x  __|___
|    |
a  __|___
|    |
y  __|__
|   |
d  _|__
|  |
x  e
```
We then evaluate, using the same value for the shift operator proposed before: 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). 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:
```   .
___|___
|     |
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.
```      .
|
______|______
|           |
a  _________|__________
|                  |
|               ___|___
___|___            |     |
|     |            d  ___|____
a  ___|____           |      |
|      |        ___|____  e
""  ___|___     |      |
|     |     a  ____|_____
d  ___|___     |        |
|     |     |      __|___
___|___  e  ___|___   |    |
|     |     |     |   d  __|__
a  ___|___  a  ___|____  |   |
|     |     |      |  ""  e
""  __|___  ""  ___|___
|    |      |     |
d  __|__    d  ___|___
|   |       |     |
""  e    ___|___  e
|     |
a  ___|___
|     |
""  __|___
|    |
d  __|__
|   |
""  e
```
```    _______________               _______________            _______________
| [x->2, y->3] |	          | [x->2, y->3] |          | [x->2, y->3] |
------------------- 	         ------------------        ------------------
|              |     ¢        |              |    =     |              |
|    +2        |	          |     y        |          |     5        |
|______________|	          |______________|          |______________|
```
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. 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: [] 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. 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: 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. Oh, one more thing: 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 we need two versions of ¢ too (see Barker and Shan 2014 chapter 1 for full details). This is (almost) all we need to get some significant linguistic work done.