cat theory ready

[lambda.git] / advanced_topics / monads_in_category_theory.mdwn

diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn
index 173160e..e77de46 100644 (file)
--- a/advanced_topics/monads_in_category_theory.mdwn
+++ b/advanced_topics/monads_in_category_theory.mdwn
@@ -502,9 +502,10 @@ In functional programming, instead of working with natural transformations we wo
 A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the list monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t)->M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the list monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`:
 
 <pre>
-       let phi = fun ((_:char, x y) -> [(1,x,y),(2,x,y)]
+       let phi = fun ((_:char), x, y) -> [(1,x,y),(2,x,y)]
 </pre>
 
+[-- I intentionally chose this polymorphic function because simpler ways of mapping the polymorphic monad operations from functional programming onto the category theory notions can't accommodate it. We have all the F, MF' (unit G') and so on in order to be able to be handle even phis like this. --]
 
 
 Now where `gamma` is another function of type <code>F'('t) &rarr; M(G'('t))</code>, we define:
@@ -518,7 +519,7 @@ Now where `gamma` is another function of type <code>F'('t) &rarr; M(G'('t))</cod
 Hence:
 
 <pre>
-       gamma <=< phi = fun a -> (gamma =<< phi a)
+       gamma <=< phi = (fun a -> gamma =<< phi a)
 </pre>
 
 `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`.
@@ -532,7 +533,7 @@ With these definitions, our monadic laws become:
        rho is a polymorphic function of type R('t) -> M(R'('t))
        and F' = G and G' = R, 
        and a ranges over values of type F('t),
-       b ranges over values of type G('t),
+       and b ranges over values of type G('t),
        and c ranges over values of type G'('t):
 
              (i) &gamma; <=< &phi; is defined,
@@ -546,19 +547,20 @@ With these definitions, our monadic laws become:
             (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))
+                         (fun a -> (fun b -> rho =<< gamma b) =<< phi a)  =
+                                                     (fun a -> rho =<< (gamma =<< phi a))
 
           (ii'') (fun b -> rho =<< gamma b) =<< phi a  =  rho =<< (gamma =<< phi a)
 </pre>
 
 <pre>
          (iii.1) (unit G') <=< &gamma;  =  &gamma;
-                 when &gamma; is a natural transformation from some FG' to MG'
+                 whenever &gamma; is a natural transformation from some FG' to MG'
        ==>
                          (unit G') <=< gamma  =  gamma
-                         when gamma is a function of type F(G'('t)) -> M(G'('t))
+                         whenever gamma is a function of type F(G'('t)) -> M(G'('t))
 
-                         fun b -> (unit G') =<< gamma b  =  gamma
+                         (fun b -> (unit G') =<< gamma b)  =  gamma
 
                          (unit G') =<< gamma b  =  gamma b
 
@@ -571,24 +573,24 @@ With these definitions, our monadic laws become:
 
 <pre>
          (iii.2) &gamma;  =  &gamma; <=< (unit G)
-                 when &gamma; is a natural transformation from G to some MR'G
+                 whenever &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)))
+                         whenever gamma is a function of type G('t) -> M(R'(G('t)))
 
-                         gamma  =  fun b -> gamma =<< (unit G) b
+                         gamma  =  (fun b -> gamma =<< (unit G) b)
 
                          As above, return will map arguments b of type G('t) to the
                          monadic value (unit G) b, of type M(G('t)).
 
-                         gamma  =  fun b -> gamma =<< return b
+                         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)`
+*      `(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`: