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=d5c0941da9a74e539a9e4944ca686ed0473ae91e;hp=f05747f675b416fa5d5af01dee2d0f0278258874;hb=115b2bc2456adb01295e074ccc825942e45c46c0;hpb=704abdbe4afe78e553738662a3cb0bb6944b54ff

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index f05747f6..d5c0941d 100644
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -273,8 +273,8 @@ Summarizing then, the monad laws can be expressed as:
 
 
 
-The standard category-theory presentation of the monad laws
------------------------------------------------------------
+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 `<=<`.
 
 <!--
@@ -308,7 +308,7 @@ Recall that `join` is a natural transformation from the (composite) functor `MM`
 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> 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 `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
 
@@ -318,10 +318,10 @@ Composing them:
 	(2) ((join MG') -v- (MM &gamma;)) assigns to C1 the morphism join[MG'(C1)] &#8728; MM(&gamma;*).
 </pre>
 
-Next:
+Next, consider the composite transformation <code>((M &gamma;) -v- (join G))</code>:
 
 <pre>
-	(3) Consider the composite transformation <code>((M &gamma;) -v- (join G))</code>. 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>:
@@ -347,16 +347,16 @@ Next recall that `unit` is a natural transformation from `1C` to `M`. So for ele
 	(4) unit[C2] &#8728; f = M(f) &#8728; unit[C1]
 </pre>
 
-Next:
+Next, consider the composite transformation <code>((M &gamma;) -v- (unit G))</code>:
 
 <pre>
-	(5) Consider the composite transformation ((M &gamma;) -v- (unit G)). 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:
+Next, consider the composite transformation <code>((unit MG') -v- &gamma;)</code>:
 
 <pre>
-	(6) Consider the composite transformation ((unit MG') -v- &gamma;). 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>:
@@ -379,123 +379,223 @@ So our **(lemma 2)** is:
 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;)
-                     ---------------------
-			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;)
-                                                             ---------------
-			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;)
+			 similarly, &rho; <=< (&gamma; <=< &phi;) is:
+							((join R') (M &rho;) ((join G') (M &gamma;) &phi;))
 
-			which will be true for all &rho;,&gamma;,&phi; just in case:
+		 	 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;)
+  
+			 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')) = ((join R') (join MR')), for any R'.
+			 which will be true for all &rho;,&gamma;,&phi; only when:
+	         ((join R') (M join R')) = ((join R') (join MR')), for any R'.
 
-			which will in turn be true just in case:
+			 which will in turn be true when:
+       (ii') (join (M join)) = (join (join M))
 
-	(ii') (join (M join)) = (join (join M))
 
 
-	(iii.1) (unit F') <=< &phi;  =  &phi;
+	 (iii.1) (unit G') <=< &gamma;  =  &gamma;
+	         when &gamma; is a natural transformation from some FG' to MG'
 	==>
-			(unit F') is a transformation from F' to MF', so:
-				(unit F') <=< &phi; becomes: (join F') (M unit F') &phi;
-						   which is: (join F') (M unit F') &phi;
-				substituting in (iii.1), we get:
-			((join F') (M unit F') &phi;) = &phi;
-
-			which will be true for all &phi; just in case:
+			 (unit G') is a transformation from G' to MG', so:
+			 (unit G') <=< &gamma; becomes: ((join G') (M unit G') &gamma;)
 
-	         ((join F') (M unit F')) = the identity transformation, for any F'
+			 substituting in (iii.1), we get:
+			 ((join G') (M unit G') &gamma;) = &gamma;
 
-			which will in turn be true just in case:
+			 which will be true for all &gamma; just in case:
+	         ((join G') (M unit G')) = the identity transformation, for any G'
 
+			 which will in turn be true just in case:
 	(iii.1') (join (M unit) = the identity transformation
 
 
-	(iii.2) &phi;  =  &phi; <=< (unit F)
+
+
+	 (iii.2) &gamma;  =  &gamma; <=< (unit G)
+	         when &gamma; is a natural transformation from G to some MR'G
 	==>
-			&phi; is a transformation from F to MF', so:
-				unit <=< &phi; becomes: (join F') (M &phi;) unit
-				substituting in (iii.2), we get:
-			&phi; = ((join F') (M &phi;) (unit F))
-						   --------------
-				which by lemma (2), yields:
-                            ------------
-			&phi; = ((join F') ((unit MF') &phi;)
+			 unit <=< &gamma; becomes: ((join R'G) (M &gamma;) unit)
+			
+			 substituting in (iii.2), we get:
+			 &gamma; = ((join R'G) (M &gamma;) (unit G))
+		
+			 which by lemma 2, yields:
+			 &gamma; = ((join R'G) ((unit MR'G) &gamma;)
+
+			  which will be true for all &gamma; just in case:
+	         ((join R'G) (unit MR'G)) = the identity transformation, for any R'G
+
+			 which will in turn be true just in case:
+	(iii.2') (join (unit M)) = the identity transformation
+</pre>
 
-				which will be true for all &phi; just in case:
 
-	        ((join F') (unit MF')) = the identity transformation, for any F'
+Collecting the results, our monad laws turn out in this format to be:
 
-				which will in turn be true just in case:
+<pre>
+	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') ((join G') (M &gamma;) &phi;) etc also in T
+
+	   (ii') (join (M join)) = (join (join M))
+
+	(iii.1') (join (M unit)) = the identity transformation
 
 	(iii.2') (join (unit M)) = the identity transformation
 </pre>
 
 
-Collecting the results, our monad laws turn out in this format to be:
 
+Getting to the functional programming presentation of the monad laws
+--------------------------------------------------------------------
+In functional programming, `unit` is sometimes called `return` and the monad laws are usually stated in terms of `unit`/`return` and an operation called `bind` which is interdefinable with `<=<` or with `join`.
+
+The base category <b>C</b> will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
+
+A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1&rarr;C2</code> to functions <code>M(f):M(C1)&rarr;M(C2)</code>. This is also known as <code>lift<sub>M</sub> f</code> for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the list monad, `M` maps every type `'t` into the type `'t list`, and maps every function <code>f:x&rarr;y</code> into the function that maps `[x1,x2...]` to `[y1,y2,...]`.
+
+
+In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad" in question.
+
+A "monadic value" is any member of a type M('t), for any type 't. For example, a list is a monadic value for the list monad. We can think of these monadic values as the result of applying some function <code>(&phi; : F('t) &rarr; M(F'('t)))</code> to an argument `a` of type `F('t)`.
+
+
+Let `'t` be a type variable, and `F` and `F'` be functors, and let `phi` be a polymorphic function that takes arguments of type `F('t)` and yields results of type `MF'('t)` in the monad `M`. An example with `M` being the list monad:
+
+<pre>
+	let phi = fun ((_:char, x y) -> [(1,x,y),(2,x,y)]
 </pre>
-	when &phi; a transformation from F to MF', &gamma; a transformation from F' to MG', &rho; a transformation from G' to MR' all in T:
 
-	(i') ((join G') (M &gamma;) &phi;) etc also in T
+Here phi is defined when `'t = 't1*'t2`, `F('t1*'t2) = char * 't1 * 't2`, and `F'('t1 * 't2) = int * 't1 * 't2`.
 
-	(ii') (join (M join)) = (join (join M))
 
-	(iii.1') (join (M unit)) = the identity transformation
+Now where `gamma` is another function into monad `M` of type <code>F'('t) &rarr; MG'('t)</code>, we define:
 
-	(iii.2')(join (unit M)) = the identity transformation
+<pre>
+	gamma =<< phi a  =def. ((join G') -v- (M gamma)) (phi a)
+
+	                 = ((join G') -v- (M gamma) -v- phi) a
+					 = (gamma <=< phi) a
 </pre>
 
+Hence:
 
+<pre>
+	gamma <=< phi = fun a -> (gamma =<< phi a)
+</pre>
 
-7. 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.
+`gamma =<< phi a` is called the operation of "binding" the function gamma to the monadic value `phi a`, and is usually written as `phi a >>= gamma`.
 
-Additionally, whereas in category-theory one works "monomorphically", in functional programming one usually works with "polymorphic" functions.
+With these definitions, our monadic laws become:
 
-The base category <b>C</b> will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
 
-A monad M will consist of a mapping from types C1 to types M(C1), and a mapping from functions f:C1&rarr;C2 to functions M(f):M(C1)&rarr;M(C2). This is also known as "fmap f" or "liftM f" for M, and is called "function f lifted into the monad M." For example, where M is the list monad, M maps every type X into the type "list of Xs", and maps every function f:x&rarr;y into the function that maps [x1,x2...] to [y1,y2,...].
+<pre>
+	Where phi is a polymorphic function from type F('t) -> M F'('t)
+	and gamma is a polymorphic function from type G('t) -> M G' ('t)
+	and rho is a polymorphic function from type R('t) -> M R' ('t)
+	and F' = G and G' = R, 
+	and a ranges over values of type F('t) for some type 't,
+	and b ranges over values of type G('t):
+
+	      (i) &gamma; <=< &phi; is defined,
+			  and is a natural transformation from F to MG'
+	==>
+		(i'') fun a -> gamma =<< phi a is defined,
+			  and is a function from type F('t) -> M G' ('t)
 
 
 
+	     (ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
+	==>
+			  (fun a -> (rho <=< gamma) =<< phi a)  =  (fun a -> rho =<< (gamma <=< phi) a)
+			  (fun a -> (fun b -> rho =<< gamma b) =<< phi a)  =  (fun a -> rho =<< (gamma =<< phi a))
 
-A natural transformation t assigns to each type C1 in <b>C</b> a morphism t[C1]: C1&rarr;M(C1) such that, for every f:C1&rarr;C2:
-	t[C2] &#8728; f = M(f) &#8728; t[C1]
+	   (ii'') (fun b -> rho =<< gamma b) =<< phi a  =  rho =<< (gamma =<< phi a)
 
-The composite morphisms said here to be identical are morphisms from the type C1 to the type M(C2).
 
 
+	  (iii.1) (unit G') <=< &gamma;  =  &gamma;
+	          when &gamma; is a natural transformation from some FG' to MG'
 
-In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad" in question.
+			  (unit G') <=< gamma  =  gamma
+			  when gamma is a function of type FQ'('t) -> M G'('t)
+
+			  fun b -> (unit G') =<< gamma b  =  gamma
+
+			  (unit G') =<< gamma b  =  gamma b
+
+			  As below, return will map arguments c of type G'('t)
+			  to the monadic value (unit G') b, of type M G'('t).
+
+	(iii.1'') return =<< gamma b  =  gamma b
+
+
+
+	  (iii.2) &gamma;  =  &gamma; <=< (unit G)
+	          when &gamma; is a natural transformation from G to some MR'G
+	==>
+			  gamma  =  gamma <=< (unit G)
+			  when gamma is a function of type G('t) -> M R' G('t)
+
+			  gamma  =  fun b -> gamma =<< ((unit G) b)
+
+			  Let return be a polymorphic function mapping arguments
+			  of any type 't to M('t). In particular, it maps arguments
+			  b of type G('t) to the monadic value (unit G) b, of
+			  type M G('t).
+
+			  gamma  =  fun b -> gamma =<< return b
+
+	(iii.2'') gamma b  =  gamma =<< return b
+</pre>
+
+Summarizing (ii''), (iii.1''), (iii.2''), these are the monadic laws as usually stated in the functional programming literature:
+
+*	`fun b -> rho =<< gamma b) =<< phi a  =  rho =<< (gamma =<< phi a)`
+
+	Usually written reversed, and with a monadic variable `u` standing in
+	for `phi a`:
+
+	`u >>= (fun b -> gamma b >>= rho)  =  (u >>= gamma) >>= rho`
 
-For an example of the latter, let &phi; be a function that takes arguments of some (schematic, polymorphic) type C1 and yields results of some (schematic, polymorphic) type M(C2). An example with M being the list monad, and C2 being the tuple type schema int * C1:
+*	`return =<< gamma b  =  gamma b`
 
-	let &phi; = fun c &rarr; [(1,c), (2,c)]
+	Usually written reversed, and with `u` standing in for `phi a`:
 
-&phi; is polymorphic: when you apply it to the int 0 you get a result of type "list of int * int": [(1,0), (2,0)]. When you apply it to the char 'e' you get a result of type "list of int * char": [(1,'e'), (2,'e')].
+	`u >>= return  =  u`
 
-However, to keep things simple, we'll work instead with functions whose type is settled. So instead of the polymorphic &phi;, we'll work with (&phi; : C1 &rarr; M(int * C1)). This only accepts arguments of type C1. For generality, I'll talk of functions with the type (&phi; : C1 &rarr; M(C1')), where we assume that C1' is a function of C1.
+*	`gamma b  =  gamma =<< return b`
 
-A "monadic value" is any member of a type M(C1), for any type C1. For example, a list is a monadic value for the list monad. We can think of these monadic values as the result of applying some function (&phi; : C1 &rarr; M(C1')) to an argument of type C1.
+	Usually written reversed:
 
+	`return b >>= gamma  =  gamma b`
+