-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 `<=<`.
<!--
Next, let <code>γ</code> be a transformation from `G` to `MG'`, and
consider the composite transformation <code>((join MG') -v- (MM γ))</code>.
-* <code>γ</code> assigns elements `C1` in <b>C</b> a morphism <code>γ\*: G(C1) → MG'(C1)</code>. <code>(MM γ)</code> is a transformation that instead assigns `C1` the morphism <code>MM(γ\*)</code>.
+* <code>γ</code> assigns elements `C1` in <b>C</b> a morphism <code>γ\*:G(C1) → MG'(C1)</code>. <code>(MM γ)</code> is a transformation that instead assigns `C1` the morphism <code>MM(γ\*)</code>.
* `(join MG')` is a transformation from `MM(MG')` to `M(MG')` that assigns `C1` the morphism `join[MG'(C1)]`.
(2) ((join MG') -v- (MM γ)) assigns to C1 the morphism join[MG'(C1)] ∘ MM(γ*).
</pre>
-Next:
+Next, consider the composite transformation <code>((M γ) -v- (join G))</code>:
<pre>
- (3) Consider the composite transformation <code>((M γ) -v- (join G))</code>. This assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
+ (3) ((M γ) -v- (join G)) assigns to C1 the morphism M(γ*) ∘ join[G(C1)].
</pre>
So for every element `C1` of <b>C</b>:
(4) unit[C2] ∘ f = M(f) ∘ unit[C1]
</pre>
-Next:
+Next, consider the composite transformation <code>((M γ) -v- (unit G))</code>:
<pre>
- (5) Consider the composite transformation ((M γ) -v- (unit G)). This assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].
+ (5) ((M γ) -v- (unit G)) assigns to C1 the morphism M(γ*) ∘ unit[G(C1)].
</pre>
-Next:
+Next, consider the composite transformation <code>((unit MG') -v- γ)</code>:
<pre>
- (6) Consider the composite transformation ((unit MG') -v- γ). This assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
+ (6) ((unit MG') -v- γ) assigns to C1 the morphism unit[MG'(C1)] ∘ γ*.
</pre>
So for every element C1 of <b>C</b>:
Finally, we substitute <code>((join G') -v- (M γ) -v- φ)</code> for <code>γ <=< φ</code> in the monad laws. For simplicity, I'll omit the "-v-".
<pre>
- for all φ,γ,ρ in T, where φ is a transformation from F to MF', γ is a transformation from G to MG', R is a transformation from R to MR', and F'=G and G'=R:
+ For all ρ, γ, φ in T,
+ where φ is a transformation from F to MF',
+ γ is a transformation from G to MG',
+ ρ is a transformation from R to MR',
+ and F'=G and G'=R:
- (i) γ <=< φ etc are also in T
+ (i) γ <=< φ etc are also in T
==>
- (i') ((join G') (M γ) φ) etc are also in T
+ (i') ((join G') (M γ) φ) etc are also in T
- (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
+
+ (ii) (ρ <=< γ) <=< φ = ρ <=< (γ <=< φ)
==>
- (ρ <=< γ) is a transformation from G to MR', so:
- (ρ <=< γ) <=< φ becomes: (join R') (M (ρ <=< γ)) φ
- which is: (join R') (M ((join R') (M ρ) γ)) φ
- substituting in (ii), and helping ourselves to associativity on the rhs, we get:
+ (ρ <=< γ) is a transformation from G to MR', so
+ (ρ <=< γ) <=< φ becomes: ((join R') (M (ρ <=< γ)) φ)
+ which is: ((join R') (M ((join R') (M ρ) γ)) φ)
- ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ)
- ---------------------
- which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
- ------------------------
- ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ)
- ---------------
- which by lemma 1, with ρ a transformation from G' to MR', yields:
- -----------------
- ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ)
+ similarly, ρ <=< (γ <=< φ) is:
+ ((join R') (M ρ) ((join G') (M γ) φ))
- which will be true for all ρ,γ,φ just in case:
+ substituting these into (ii), and helping ourselves to associativity on the rhs, we get:
+ ((join R') (M ((join R') (M ρ) γ)) φ) = ((join R') (M ρ) (join G') (M γ) φ)
+
+ which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (M ρ) (join G') (M γ) φ)
+
+ which by lemma 1, with ρ a transformation from G' to MR', yields:
+ ((join R') (M join R') (MM ρ) (M γ) φ) = ((join R') (join MR') (MM ρ) (M γ) φ)
- ((join R') (M join R')) = ((join R') (join MR')), for any R'.
+ which will be true for all ρ,γ,φ 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') <=< φ = φ
+ (iii.1) (unit G') <=< γ = γ
+ when γ is a natural transformation from some FG' to MG'
==>
- (unit F') is a transformation from F' to MF', so:
- (unit F') <=< φ becomes: (join F') (M unit F') φ
- which is: (join F') (M unit F') φ
- substituting in (iii.1), we get:
- ((join F') (M unit F') φ) = φ
-
- which will be true for all φ just in case:
+ (unit G') is a transformation from G' to MG', so:
+ (unit G') <=< γ becomes: ((join G') (M unit G') γ)
- ((join F') (M unit F')) = the identity transformation, for any F'
+ substituting in (iii.1), we get:
+ ((join G') (M unit G') γ) = γ
- which will in turn be true just in case:
+ 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
- (iii.2) φ = φ <=< (unit F)
- ==>
- φ is a transformation from F to MF', so:
- unit <=< φ becomes: (join F') (M φ) unit
- substituting in (iii.2), we get:
- φ = ((join F') (M φ) (unit F))
- --------------
- which by lemma (2), yields:
- ------------
- φ = ((join F') ((unit MF') φ)
-
- which will be true for all φ just in case:
-
- ((join F') (unit MF')) = the identity transformation, for any F'
- which will in turn be true just in case:
+ (iii.2) γ = γ <=< (unit G)
+ when γ is a natural transformation from G to some MR'G
+ ==>
+ unit <=< γ becomes: ((join R'G) (M γ) unit)
+
+ substituting in (iii.2), we get:
+ γ = ((join R'G) (M γ) (unit G))
+
+ which by lemma 2, yields:
+ γ = ((join R'G) ((unit MR'G) γ)
+
+ which will be true for all γ 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>
Collecting the results, our monad laws turn out in this format to be:
-</pre>
- when φ a transformation from F to MF', γ a transformation from F' to MG', ρ a transformation from G' to MR' all in T:
+<pre>
+ For all ρ, γ, φ in T,
+ where φ is a transformation from F to MF',
+ γ is a transformation from G to MG',
+ ρ is a transformation from R to MR',
+ and F'=G and G'=R:
- (i') ((join G') (M γ) φ) etc also in T
+ (i') ((join G') (M γ) φ) etc also in T
- (ii') (join (M join)) = (join (join M))
+ (ii') (join (M join)) = (join (join M))
(iii.1') (join (M unit)) = the identity transformation
- (iii.2')(join (unit M)) = the identity transformation
+ (iii.2') (join (unit M)) = the identity transformation
</pre>
-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.