(i') ((join G') (M γ) φ) etc are also in T
+


+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
==>
(ρ <=< γ) is a transformation from G to MR', so
@@ 409,45 +411,57 @@ Finally, we substitute ((join G') v (M γ) v φ)
for


+ (iii.1) (unit G') <=< γ = γ
when γ is a natural transformation from some FG' to MG'
==>
(unit G') is a transformation from G' to MG', so:
 (unit G') <=< γ becomes: ((join G') (M unit G') γ)
+ (unit G') <=< γ becomes: ((join G') (M (unit G')) γ)
+ which is: ((join G') ((M unit) G') γ)
substituting in (iii.1), we get:
 ((join G') (M unit G') γ) = γ
+ ((join G') ((M unit) G') γ) = γ
 which will be true for all γ 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
+ which is:
+ (((join (M unit)) G') γ) = γ
+ [ Are the next two steps too cavalier? ]
+ which will be true for all γ just in case:
+ for any G', ((join (M unit)) G') = the identity transformation
+ which will in turn be true just in case:
+ (iii.1') (join (M unit)) = the identity transformation
+
+ (iii.2) γ = γ <=< (unit G)
when γ is a natural transformation from G to some MR'G
==>
 unit <=< γ becomes: ((join R'G) (M γ) unit)
+ γ <=< (unit G) becomes: ((join R'G) (M γ) (unit G))
substituting in (iii.2), we get:
γ = ((join R'G) (M γ) (unit G))
which by lemma 2, yields:
 γ = ((join R'G) ((unit MR'G) γ)
+ γ = (((join R'G) ((unit MR'G) γ)
+
+ which is:
+ γ = (((join (unit M)) R'G) γ)
+
+ [ Are the next two steps too cavalier? ]
which will be true for all γ just in case:
 ((join R'G) (unit MR'G)) = the identity transformation, for any R'G
+ for any R'G, ((join (unit M)) R'G) = the identity transformation
which will in turn be true just in case:
(iii.2') (join (unit M)) = the identity transformation
@@ 472,6 +486,7 @@ Collecting the results, our monad laws turn out in this format to be:
(iii.2') (join (unit M)) = the identity transformation
+In categorytheory presentations, you may see `unit` referred to as η
, and `join` referred to as μ
. Also, instead of the monad `(M, unit, join)`, you may sometimes see discussion of the "Kleisli triple" `(M, unit, =<<)`. Alternatively, `=<<` may be called ⋆
. These are interdefinable (see below).
Getting to the functional programming presentation of the monad laws
@@ 483,25 +498,21 @@ The base category C will have types as elements, and monadic functions as
A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions f:C1→C2
to functions M(f):M(C1)→M(C2)
. This is also known as lift_{M} f
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 f:x→y
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 (φ : F('t) → M(F'('t)))
to an argument `a` of type `F('t)`.

+In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad."
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:
+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`:
 let phi = fun ((_:char, x y) > [(1,x,y),(2,x,y)]
+ let phi = fun ((_:char), x, y) > [(1,x,y),(2,x,y)]
Here phi is defined when `'t = 't1*'t2`, `F('t1*'t2) = char * 't1 * 't2`, and `F'('t1 * 't2) = int * 't1 * 't2`.
+[ 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 into monad `M` of type F'('t) → MG'('t)
, we define:
+Now where `gamma` is another function of type F'('t) > M(G'('t))
, we define:
gamma =<< phi a =def. ((join G') v (M gamma)) (phi a)

= ((join G') v (M gamma) v phi) a
= (gamma <=< phi) a
@@ 509,7 +520,7 @@ Now where `gamma` is another function into monad `M` of type F'('t) →
Hence:
 gamma <=< phi = fun a > (gamma =<< phi a)
+ gamma <=< phi = (fun a > gamma =<< phi a)
`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`.
@@ 518,68 +529,69 @@ With these definitions, our monadic laws become:
 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)
+ Where phi is a polymorphic function of type F('t) > M(F'('t))
+ gamma is a polymorphic function of type G('t) > M(G'('t))
+ 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) for some type 't,
 and b ranges over values of type G('t):
+ and a ranges over values of type F('t),
+ and b ranges over values of type G('t),
+ and c ranges over values of type G'('t):
(i) γ <=< φ 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)


+ and is a function from type F('t) > M(G'('t))
+
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
==>
(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)
+


+ (iii.1) (unit G') <=< γ = γ
 when γ is a natural transformation from some FG' to MG'

+ whenever γ is a natural transformation from some FG' to MG'
+ ==>
(unit G') <=< gamma = gamma
 when gamma is a function of type FQ'('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
 As below, return will map arguments c of type G'('t)
 to the monadic value (unit G') b, of type M G'('t).
+ Let return be a polymorphic function mapping arguments of any
+ type 't to M('t). In particular, it maps arguments c of type
+ G'('t) to the monadic value (unit G') c, of type M(G'('t)).
(iii.1'') return =<< gamma b = gamma b
+


+ (iii.2) γ = γ <=< (unit G)
 when γ is a natural transformation from G to some MR'G
+ whenever γ 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)
 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).
+ 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
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`:
@@ 588,7 +600,7 @@ Summarizing (ii''), (iii.1''), (iii.2''), these are the monadic laws as usually
* `return =<< gamma b = gamma b`
 Usually written reversed, and with `u` standing in for `phi a`:
+ Usually written reversed, and with `u` standing in for `gamma b`:
`u >>= return = u`