X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=advanced_topics%2Fmonads_in_category_theory.mdwn;h=588d1a30f237dcad0f82b0a26d875af84b9459da;hp=deb5bace5b8656474b48d69a80d985c9bf5c493d;hb=c0a6070f7c11da38419b5e5da90afeddc6520b95;hpb=4bc7f125d288c543b0d22f9f8e69775dc9460317

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index deb5bace..588d1a30 100644
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -233,7 +233,8 @@ If <code>&phi;</code> is a natural transformation from `F` to `M(1C)` and <code>
 	  = (((join 1C) G') -v- ((M unit) G') -v- (&phi; G'))
 	  = ((join (1C G')) -v- (M (unit G')) -v- &gamma;)
 	  = ((join G') -v- (M (unit G')) -v- &gamma;)
-	  since (unit G') is a natural transformation to MG', this satisfies the definition for <=<:
+	  since (unit G') is a natural transformation to MG',
+	  this satisfies the definition for &lt;=&lt;:
 	  = (unit G') <=< &gamma;
 </pre>
 
@@ -247,17 +248,33 @@ Similarly, if <code>&rho;</code> is a natural transformation from `1C` to `MR'`,
 	  = (((join R') -v- (M &rho;) -v- unit) G)
 	  = (((join R') G) -v- ((M &rho;) G) -v- (unit G))
 	  = ((join (R'G)) -v- (M (&rho; G)) -v- (unit G))
-	  since &gamma; = (&rho; G) is a natural transformation to MR'G, this satisfies the definition for <=<:
+	  since &gamma; = (&rho; G) is a natural transformation to MR'G,
+	  this satisfies the definition &lt;=&lt;:
 	  = &gamma; <=< (unit G)
 </pre>
 
 where as we said <code>&gamma;</code> is a natural transformation from `G` to some `MR'G`.
 
+Summarizing then, the monad laws can be expressed as:
 
+<pre>
+	For all &rho;, &gamma;, &phi; in T for which &rho; <=< &gamma; and &gamma; <=< &phi; are defined:
+
+	    (i) &gamma; <=< &phi; etc are also in T
 
+	   (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
 
-The standard category-theory presentation of the monad laws
------------------------------------------------------------
+	(iii.1) (unit G') <=< &gamma;  =  &gamma;
+	        when &gamma; is a natural transformation from some FG' to MG'
+
+	(iii.2)                     &gamma;  =  &gamma; <=< (unit G)
+	        when &gamma; is a natural transformation from G to some MR'G
+</pre>
+
+
+
+Getting to the standard category-theory presentation of the monad laws
+----------------------------------------------------------------------
 In category theory, the monad laws are usually stated in terms of `unit` and `join` instead of `unit` and `<=<`.
 
 <!--
@@ -271,22 +288,29 @@ Let's remind ourselves of some principles:
 
 *	functors "distribute over composition", that is for any morphisms `f` and `g` in `F`'s source category: <code>F(g &#8728; f) = F(g) &#8728; F(f)</code>
 
-*	if <code>&eta;</code> is a natural transformation from `F` to `G`, then for every <code>f:C1&rarr;C2</code> in `F` and `G`'s source category <b>C</b>: <code>&eta;[C2] &#8728; F(f) = G(f) &#8728; &eta;[C1]</code>.
+*	if <code>&eta;</code> is a natural transformation from `G` to `H`, then for every <code>f:C1&rarr;C2</code> in `G` and `H`'s source category <b>C</b>: <code>&eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]</code>.
+
+*	<code>(&eta; F)[E] = &eta;[F(E)]</code> 
+
+*	<code>(K &eta;)[E} = K(&eta;[E])</code>
+
+*	<code>((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))</code>
 
 Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas.
 
 
-Recall that join is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:
+Recall that `join` is a natural transformation from the (composite) functor `MM` to `M`. So for elements `C1` in <b>C</b>, `join[C1]` will be a morphism from `MM(C1)` to `M(C1)`. And for any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:
 
 <pre>
 	(1) join[C2] &#8728; MM(f)  =  M(f) &#8728; join[C1]
 </pre>
 
-Next, consider the composite transformation <code>((join MG') -v- (MM &gamma;))</code>.
+Next, let <code>&gamma;</code> be a transformation from `G` to `MG'`, and
+ consider the composite transformation <code>((join MG') -v- (MM &gamma;))</code>.
 
-*	<code>&gamma;</code> is a transformation from `G` to `MG'`, and assigns elements `C1` in <b>C</b> a morphism <code>&gamma;\*: G(C1) &rarr; MG'(C1)</code>. <code>(MM &gamma;)</code> is a transformation that instead assigns `C1` the morphism <code>MM(&gamma;\*)</code>.
+*	<code>&gamma;</code> assigns elements `C1` in <b>C</b> a morphism <code>&gamma;\*:G(C1) &rarr; MG'(C1)</code>. <code>(MM &gamma;)</code> is a transformation that instead assigns `C1` the morphism <code>MM(&gamma;\*)</code>.
 
-*	`(join MG')` is a transformation from `MMMG'` to `MMG'` that assigns `C1` the morphism `join[MG'(C1)]`.
+*	`(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
 
 Composing them:
 
@@ -294,17 +318,17 @@ Composing them:
 	(2) ((join MG') -v- (MM &gamma;)) assigns to C1 the morphism join[MG'(C1)] &#8728; MM(&gamma;*).
 </pre>
 
-Next, consider the composite transformation <code>((M &gamma;) -v- (join G))</code>.
+Next, consider the composite transformation <code>((M &gamma;) -v- (join G))</code>:
 
 <pre>
-	(3) This assigns to C1 the morphism M(&gamma;*) &#8728; join[G(C1)].
+	(3) ((M &gamma;) -v- (join G)) assigns to C1 the morphism M(&gamma;*) &#8728; join[G(C1)].
 </pre>
 
 So for every element `C1` of <b>C</b>:
 
 <pre>
 	((join MG') -v- (MM &gamma;))[C1], by (2) is:
-	join[MG'(C1)] &#8728; MM(&gamma;*), which by (1), with f=&gamma;*: G(C1)&rarr;MG'(C1) is:
+	join[MG'(C1)] &#8728; MM(&gamma;*), which by (1), with f=&gamma;*:G(C1)&rarr;MG'(C1) is:
 	M(&gamma;*) &#8728; join[G(C1)], which by 3 is:
 	((M &gamma;) -v- (join G))[C1]
 </pre>
@@ -312,33 +336,34 @@ So for every element `C1` of <b>C</b>:
 So our **(lemma 1)** is:
 
 <pre>
-	((join MG') -v- (MM &gamma;))  =  ((M &gamma;) -v- (join G)), where &gamma; is a transformation from G to MG'.
+	((join MG') -v- (MM &gamma;))  =  ((M &gamma;) -v- (join G)),
+	where as we said &gamma; is a natural transformation from G to MG'.
 </pre>
 
 
-Next recall that unit is a natural transformation from `1C` to `M`. So for elements `C1` in <b>C</b>, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism <code>f:a&rarr;b</code> in <b>C</b>:
+Next recall that `unit` is a natural transformation from `1C` to `M`. So for elements `C1` in <b>C</b>, `unit[C1]` will be a morphism from `C1` to `M(C1)`. And for any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:
 
 <pre>
-	(4) unit[b] &#8728; f = M(f) &#8728; unit[a]
+	(4) unit[C2] &#8728; f = M(f) &#8728; unit[C1]
 </pre>
 
-Next consider the composite transformation <code>((M &gamma;) -v- (unit G))</code>:
+Next, consider the composite transformation <code>((M &gamma;) -v- (unit G))</code>:
 
 <pre>
-	(5) This assigns to C1 the morphism M(&gamma;*) &#8728; unit[G(C1)].
+	(5) ((M &gamma;) -v- (unit G)) assigns to C1 the morphism M(&gamma;*) &#8728; unit[G(C1)].
 </pre>
 
-Next consider the composite transformation <code>((unit MG') -v- &gamma;)</code>.
+Next, consider the composite transformation <code>((unit MG') -v- &gamma;)</code>:
 
 <pre>
-	(6) This assigns to C1 the morphism unit[MG'(C1)] &#8728; &gamma;*.
+	(6) ((unit MG') -v- &gamma;) assigns to C1 the morphism unit[MG'(C1)] &#8728; &gamma;*.
 </pre>
 
 So for every element C1 of <b>C</b>:
 
 <pre>
 	((M &gamma;) -v- (unit G))[C1], by (5) =
-	M(&gamma;*) &#8728; unit[G(C1)], which by (4), with f=&gamma;*: G(C1)&rarr;MG'(C1) is:
+	M(&gamma;*) &#8728; unit[G(C1)], which by (4), with f=&gamma;*:G(C1)&rarr;MG'(C1) is:
 	unit[MG'(C1)] &#8728; &gamma;*, which by (6) =
 	((unit MG') -v- &gamma;)[C1]
 </pre>
@@ -346,46 +371,54 @@ So for every element C1 of <b>C</b>:
 So our **(lemma 2)** is:
 
 <pre>
-	(((M &gamma;) -v- (unit G))  =  ((unit MG') -v- &gamma;)), where &gamma; is a transformation from G to MG'.
+	(((M &gamma;) -v- (unit G))  =  ((unit MG') -v- &gamma;)),
+	where as we said &gamma; is a natural transformation from G to MG'.
 </pre>
 
 
 Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <code>&gamma; &lt;=&lt; &phi;</code> in the monad laws. For simplicity, I'll omit the "-v-".
 
 <pre>
-	for all &phi;,&gamma;,&rho; in T, where &phi; is a transformation from F to MF', &gamma; is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+	For all &rho;, &gamma;, &phi; in T,
+	where &phi; is a transformation from F to MF',
+	&gamma; is a transformation from G to MG',
+	&rho; is a transformation from R to MR',
+	and F'=G and G'=R:
 
-	(i) &gamma; <=< &phi; etc are also in T
+	     (i) &gamma; <=< &phi; etc are also in T
 	==>
-	(i') ((join G') (M &gamma;) &phi;) etc are also in T
+	    (i') ((join G') (M &gamma;) &phi;) etc are also in T
+
 
 
-	(ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
+	    (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
 	==>
-		 (&rho; <=< &gamma;) is a transformation from G to MR', so:
-			(&rho; <=< &gamma;) <=< &phi; becomes: (join R') (M (&rho; <=< &gamma;)) &phi;
-							which is: (join R') (M ((join R') (M &rho;) &gamma;)) &phi;
-		 	substituting in (ii), and helping ourselves to associativity on the rhs, we get:
+		    (&rho; <=< &gamma;) is a transformation from G to MR', so
+			(&rho; <=< &gamma;) <=< &phi; becomes: ((join R') (M (&rho; <=< &gamma;)) &phi;)
+							which is: ((join R') (M ((join R') (M &rho;) &gamma;)) &phi;)
 
-	     ((join R') (M ((join R') (M &rho;) &gamma;)) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
-                     ---------------------
+			similarly, &rho; <=< (&gamma; <=< &phi;) is:
+							((join R') (M &rho;) ((join G') (M &gamma;) &phi;))
+
+		 	substituting these into (ii), and helping ourselves to associativity on the rhs, we get:
+	        ((join R') (M ((join R') (M &rho;) &gamma;)) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
+    
 			which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
-                    ------------------------
-	     ((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
-                                                             ---------------
+	        ((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (M &rho;) (join G') (M &gamma;) &phi;)
+  
 			which by lemma 1, with &rho; a transformation from G' to MR', yields:
-                                                             -----------------
-	     ((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (join MR') (MM &rho;) (M &gamma;) &phi;)
+	        ((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (join MR') (MM &rho;) (M &gamma;) &phi;)
 
-			which will be true for all &rho;,&gamma;,&phi; just in case:
+			which will be true for all &rho;,&gamma;,&phi; only when:
+	        ((join R') (M join R')) = ((join R') (join MR')), for any R'.
 
-	      ((join R') (M join R')) = ((join R') (join MR')), for any R'.
+			which will in turn be true when:
+      (ii') (join (M join)) = (join (join M))
 
-			which will in turn be true just in case:
-
-	(ii') (join (M join)) = (join (join M))
 
 
+	 (iii.1) (unit G') <=< &gamma;  =  &gamma;
+	         when &gamma; is a natural transformation from some FG' to MG'
 	(iii.1) (unit F') <=< &phi;  =  &phi;
 	==>
 			(unit F') is a transformation from F' to MF', so:
@@ -403,6 +436,10 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
 	(iii.1') (join (M unit) = the identity transformation
 
 
+
+
+	 (iii.2)                     &gamma;  =  &gamma; <=< (unit G)
+	         when &gamma; is a natural transformation from G to some MR'G
 	(iii.2) &phi;  =  &phi; <=< (unit F)
 	==>
 			&phi; is a transformation from F to MF', so:
@@ -440,8 +477,8 @@ Collecting the results, our monad laws turn out in this format to be:
 
 
 
-7. The functional programming presentation of the monad laws
-------------------------------------------------------------
+Getting to the functional programming presentation of the monad laws
+--------------------------------------------------------------------
 In functional programming, unit is usually called "return" and the monad laws are usually stated in terms of return and an operation called "bind" which is interdefinable with <=< or with join.
 
 Additionally, whereas in category-theory one works "monomorphically", in functional programming one usually works with "polymorphic" functions.