author Chris Wed, 13 May 2015 12:40:30 +0000 (08:40 -0400) committer Chris Wed, 13 May 2015 12:40:30 +0000 (08:40 -0400)

index 001f8b1..fd25cce 100644 (file)
@@ -403,8 +403,11 @@ functional application (i.e, f:(α->β) (x:α) = fx:β).

-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:
+
+    α/β   β    = α
+      β   β\α  = α

+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.