From: Chris <chris.barker@nyu.edu>
Date: Tue, 12 May 2015 14:03:24 +0000 (-0400)
Subject: edits
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=0f8ff4c3540567e649fcabd628c6e4aa208df052

edits
---

diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
index d13efa7f..001f8b19 100644
--- a/topics/_week15_continuation_applications.mdwn
+++ b/topics/_week15_continuation_applications.mdwn
@@ -300,6 +300,8 @@ 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.]
 
+## 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
@@ -355,6 +357,8 @@ 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).  
 
+## LIFT
+
 Then in the spirit of monadic thinking, we'll have a way of lifting an
 arbitrary value into the tower system:
 
@@ -383,9 +387,9 @@ 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
+                                                        []    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:
@@ -397,6 +401,8 @@ 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:
 
@@ -410,7 +416,9 @@ 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