X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week15_continuation_applications.mdwn;h=fd25ccec641202b6eda7298d5a9a778e34dd695e;hp=001f8b19d9b0a6e23fb6bcb38a64823e3cba9e27;hb=30ab04be8bbff031e9516db53b3666f0cdb4503f;hpb=0f8ff4c3540567e649fcabd628c6e4aa208df052

diff --git a/topics/_week15_continuation_applications.mdwn b/topics/_week15_continuation_applications.mdwn
index 001f8b19..fd25ccec 100644
--- a/topics/_week15_continuation_applications.mdwn
+++ b/topics/_week15_continuation_applications.mdwn
@@ -403,8 +403,11 @@ functional application (i.e, f:(α->β) (x:α) = fx:β).
 
 ## Not quite a monad
 
-To demonstrate that this is indeed the continuation monad's ¢
-operator:
+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])
@@ -416,20 +419,102 @@ operator:
     == ------
          fx
 
-However, these continuations do not form an official monad.  The
-reason is that (see Wadler's paper `Composable continuations' for details).
+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:
+
+    α/β   β    = α
+      β   β\α  = α
 
-Neverthless, obeys the monad laws.
+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.
 
-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.