From 30ab04be8bbff031e9516db53b3666f0cdb4503f Mon Sep 17 00:00:00 2001
From: Chris
Date: Wed, 13 May 2015 08:40:30 -0400
Subject: [PATCH] edits
---
topics/_week15_continuation_applications.mdwn | 109 +++++++++++++++++++++++---
1 file changed, 97 insertions(+), 12 deletions(-)
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.
--
2.11.0