author Jim Pryor Tue, 2 Nov 2010 14:50:46 +0000 (10:50 -0400) committer Jim Pryor Tue, 2 Nov 2010 14:50:46 +0000 (10:50 -0400)
Signed-off-by: Jim Pryor <profjim@jimpryor.net>

index 8552e65..deb5bac 100644 (file)
@@ -33,8 +33,8 @@ Some examples of monoids are:

*      finite strings of an alphabet `A`, with <code>&#8902;</code> being concatenation and `z` being the empty string
*      all functions <code>X&rarr;X</code> over a set `X`, with <code>&#8902;</code> being composition and `z` being the identity function over `X`
-*      the natural numbers with <code>&#8902;</code> being plus and `z` being `0` (in particular, this is a **commutative monoid**). If we use the integers, or the naturals mod n, instead of the naturals, then every element will have an inverse and so we have not merely a monoid but a **group**.)
-*      if we let <code>&#8902;</code> be multiplication and `z` be `1`, we get different monoids over the same sets as in the previous item.
+*      the natural numbers with <code>&#8902;</code> being plus and `z` being 0 (in particular, this is a **commutative monoid**). If we use the integers, or the naturals mod n, instead of the naturals, then every element will have an inverse and so we have not merely a monoid but a **group**.
+*      if we let <code>&#8902;</code> be multiplication and `z` be 1, we get different monoids over the same sets as in the previous item.

Categories
----------
@@ -58,7 +58,7 @@ To have a category, the elements and morphisms have to satisfy some constraints:

These parallel the constraints for monoids. Note that there can be multiple distinct morphisms between an element `E` and itself; they need not all be identity morphisms. Indeed from (iii) it follows that each element can have only a single identity morphism.

-A good intuitive picture of a category is as a generalized directed graph, where the category elements are the graph's nodes, and there can be multiple directed edges between a given pair of nodes, and nodes can also have multiple directed edges to themselves. (Every node must have at least one such, which is that node's identity morphism.)
+A good intuitive picture of a category is as a generalized directed graph, where the category elements are the graph's nodes, and there can be multiple directed edges between a given pair of nodes, and nodes can also have multiple directed edges to themselves. Morphisms correspond to directed paths of length &ge; 0 in the graph.

Some examples of categories are:
@@ -67,7 +67,7 @@ Some examples of categories are:

*      any monoid <code>(S,&#8902;,z)</code> generates a category with a single element `x`; this `x` need not have any relation to `S`. The members of `S` play the role of *morphisms* of this category, rather than its elements. All of these morphisms are understood to map `x` to itself. The result of composing the morphism consisting of `s1` with the morphism `s2` is the morphism `s3`, where <code>s3=s1&#8902;s2</code>. The identity morphism for the (single) category element `x` is the monoid's identity `z`.

-*      a **preorder** is a structure <code>(S, &le;)</code> consisting of a reflexive, transitive, binary relation on a set `S`. It need not be connected (that is, there may be members `x`,`y` of `S` such that neither <code>x&le;y</code> nor <code>y&le;x</code>). It need not be anti-symmetric (that is, there may be members `s1`,`s2` of `S` such that <code>s1&le;s2</code> and <code>s2&le;s1</code> but `s1` and `s2` are not identical). Some examples:
+*      a **preorder** is a structure <code>(S, &le;)</code> consisting of a reflexive, transitive, binary relation on a set `S`. It need not be connected (that is, there may be members `s1`,`s2` of `S` such that neither <code>s1&le;s2</code> nor <code>s2&le;s1</code>). It need not be anti-symmetric (that is, there may be members `s1`,`s2` of `S` such that <code>s1&le;s2</code> and <code>s2&le;s1</code> but `s1` and `s2` are not identical). Some examples:

*       sentences ordered by logical implication ("p and p" implies and is implied by "p", but these sentences are not identical; so this illustrates a pre-order without anti-symmetry)
*       sets ordered by size (this illustrates it too)
@@ -136,7 +136,7 @@ Then <code>(&eta; F)</code> is a natural transformation from the (composite) fun
And <code>(K &eta;)</code> is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `C1` is an element of category <b>C</b>, <code>(K &eta;)[C1] = K(&eta;[C1])</code>---that is, the morphism in <b>E</b> that `K` assigns to the morphism <code>&eta;[C1]</code> of <b>D</b>.

-<code>(&phi; -v- &eta;)</code> is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where <code>f:C1&rarr;C2</code>:
+<code>(&phi; -v- &eta;)</code> is a natural transformation from `G` to `J`; this is known as a "vertical composition". For any morphism <code>f:C1&rarr;C2</code> in <b>C</b>:

<pre>
&phi;[C2] &#8728; H(f) &#8728; &eta;[C1] = &phi;[C2] &#8728; H(f) &#8728; &eta;[C1]
@@ -186,22 +186,20 @@ In earlier days, these were also called "triples."

A **monad** is a structure consisting of an (endo)functor `M` from some category <b>C</b> to itself, along with some natural transformations, which we'll specify in a moment.

-Let `T` be a set of natural transformations <code>&phi;</code>, each being between some (variable) functor `F` and another functor which is the composite `MF'` of `M` and a (variable) functor `F'`. That is, for each element `C1` in <b>C</b>, <code>&phi;</code> assigns `C1` a morphism from element `F(C1)` to element `MF'(C1)`, satisfying the constraints detailed in the previous section. For different members of `T`, the relevant functors may differ; that is, <code>&phi;</code> is a transformation from functor `F` to `MF'`, <code>&gamma;</code> is a transformation from functor `G` to `MG'`, and none of `F`, `F'`, `G`, `G'` need be the same.
+Let `T` be a set of natural transformations <code>&phi;</code>, each being between some arbitrary endofunctor `F` on <b>C</b> and another functor which is the composite `MF'` of `M` and another arbitrary endofunctor `F'` on <b>C</b>. That is, for each element `C1` in <b>C</b>, <code>&phi;</code> assigns `C1` a morphism from element `F(C1)` to element `MF'(C1)`, satisfying the constraints detailed in the previous section. For different members of `T`, the relevant functors may differ; that is, <code>&phi;</code> is a transformation from functor `F` to `MF'`, <code>&gamma;</code> is a transformation from functor `G` to `MG'`, and none of `F`, `F'`, `G`, `G'` need be the same.

-One of the members of `T` will be designated the "unit" transformation for `M`, and it will be a transformation from the identity functor `1C` for <b>C</b> to `M(1C)`. So it will assign to `C1` a morphism from `C1` to `M(C1)`.
+One of the members of `T` will be designated the `unit` transformation for `M`, and it will be a transformation from the identity functor `1C` for <b>C</b> to `M(1C)`. So it will assign to `C1` a morphism from `C1` to `M(C1)`.

-We also need to designate for `M` a "join" transformation, which is a natural transformation from the (composite) functor `MM` to `M`.
+We also need to designate for `M` a `join` transformation, which is a natural transformation from the (composite) functor `MM` to `M`.

These two natural transformations have to satisfy some constraints ("the monad laws") which are most easily stated if we can introduce a defined notion.

-Let <code>&phi;</code> and <code>&gamma;</code> be members of `T`, that is they are natural transformations from `F` to `MF'` and from `G` to `MG'`, respectively. Let them be such that `F' = G`. Now <code>(M &gamma;)</code> will also be a natural transformation, formed by composing the functor `M` with the natural transformation <code>&gamma;</code>. Similarly, `(join G')` will be a natural transformation, formed by composing the natural transformation `join` with the functor `G'`; it will transform the functor `MMG'` to the functor `MG'`. Now take the vertical composition of the three natural transformations `(join G')`, <code>(M &gamma;)</code>, and <code>&phi;</code>, and abbreviate it as follows:
+Let <code>&phi;</code> and <code>&gamma;</code> be members of `T`, that is they are natural transformations from `F` to `MF'` and from `G` to `MG'`, respectively. Let them be such that `F' = G`. Now <code>(M &gamma;)</code> will also be a natural transformation, formed by composing the functor `M` with the natural transformation <code>&gamma;</code>. Similarly, `(join G')` will be a natural transformation, formed by composing the natural transformation `join` with the functor `G'`; it will transform the functor `MMG'` to the functor `MG'`. Now take the vertical composition of the three natural transformations `(join G')`, <code>(M &gamma;)</code>, and <code>&phi;</code>, and abbreviate it as follows. Since composition is associative I don't specify the order of composition on the rhs.

<pre>
&gamma; <=< &phi;  =def.  ((join G') -v- (M &gamma;) -v- &phi;)
</pre>

-Since composition is associative I don't specify the order of composition on the rhs.
-
In other words, `<=<` is a binary operator that takes us from two members <code>&phi;</code> and <code>&gamma;</code> of `T` to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes it's written <code>&phi; >=> &gamma;</code> where that's the same as <code>&gamma; &lt;=&lt; &phi;</code>.)

<code>&phi;</code> is a transformation from `F` to `MF'`, where the latter = `MG`; <code>(M &gamma;)</code> is a transformation from `MG` to `MMG'`; and `(join G')` is a transformation from `MMG'` to `MG'`. So the composite <code>&gamma; &lt;=&lt; &phi;</code> will be a transformation from `F` to `MG'`, and so also eligible to be a member of `T`.
@@ -212,45 +210,48 @@ Now we can specify the "monad laws" governing a monad as follows:
(T, <=<, unit) constitute a monoid
</pre>

-That's it. Well, there may be a wrinkle here. I don't know whether the definition of a monoid requires the operation to be defined for every pair in its set. In the present case, <code>&gamma; &lt;=&lt; &phi;</code> isn't fully defined on `T`, but only when <code>&phi;</code> is a transformation to some `MF'` and <code>&gamma;</code> is a transformation from `F'`. But wherever `<=<` is defined, the monoid laws are satisfied:
+That's it. Well, there may be a wrinkle here. I don't know whether the definition of a monoid requires the operation to be defined for every pair in its set. In the present case, <code>&gamma; &lt;=&lt; &phi;</code> isn't fully defined on `T`, but only when <code>&phi;</code> is a transformation to some `MF'` and <code>&gamma;</code> is a transformation from `F'`. But wherever `<=<` is defined, the monoid laws must hold:

<pre>
(i) &gamma; <=< &phi; is also in T

(ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)

-       (iii.1) unit <=< &phi;  =  &phi;                 (here &phi; has to be a natural transformation to M(1C))
+       (iii.1) unit <=< &phi;  =  &phi;
+               (here &phi; has to be a natural transformation to M(1C))

-       (iii.2)                &phi;  =  &phi; <=< unit  (here &phi; has to be a natural transformation from 1C)
+       (iii.2)                &rho;  =  &rho; <=< unit
+               (here &rho; has to be a natural transformation from 1C)
</pre>

-If <code>&phi;</code> is a natural transformation from `F` to `M(1C)` and <code>&gamma;</code> is <code>(&phi; G')</code>, that is, a natural transformation from `FG` to `MG`, then we can extend (iii.1) as follows:
+If <code>&phi;</code> is a natural transformation from `F` to `M(1C)` and <code>&gamma;</code> is <code>(&phi; G')</code>, that is, a natural transformation from `FG'` to `MG'`, then we can extend (iii.1) as follows:

<pre>
&gamma; = (&phi; G')
= ((unit <=< &phi;) G')
-         = ((join -v- (M unit) -v- &phi;) G')
-         = (join G') -v- ((M unit) G') -v- (&phi; G')
-         = (join G') -v- (M (unit G')) -v- &gamma;
-         ??
+         = (((join 1C) -v- (M unit) -v- &phi;) G')
+         = (((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 <=<:
= (unit G') <=< &gamma;
</pre>

where as we said <code>&gamma;</code> is a natural transformation from some `FG'` to `MG'`.

-Similarly, if <code>&phi;</code> is a natural transformation from `1C` to `MF'`, and <code>&gamma;</code> is <code>(&phi; G)</code>, that is, a natural transformation from `G` to `MF'G`, then we can extend (iii.2) as follows:
+Similarly, if <code>&rho;</code> is a natural transformation from `1C` to `MR'`, and <code>&gamma;</code> is <code>(&rho; G)</code>, that is, a natural transformation from `G` to `MR'G`, then we can extend (iii.2) as follows:

<pre>
-       &gamma; = (&phi; G)
-         = ((&phi; <=< unit) G)
-         = (((join F') -v- (M &phi;) -v- unit) G)
-         = ((join F'G) -v- ((M &phi;) G) -v- (unit G))
-         = ((join F'G) -v- (M (&phi; G)) -v- (unit G))
-         ??
+       &gamma; = (&rho; G)
+         = ((&rho; <=< unit) G)
+         = (((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 <=<:
= &gamma; <=< (unit G)
</pre>

-where as we said <code>&gamma;</code> is a natural transformation from `G` to some `MF'G`.
+where as we said <code>&gamma;</code> is a natural transformation from `G` to some `MR'G`.

@@ -290,7 +291,7 @@ Next, consider the composite transformation <code>((join MG') -v- (MM &gamma;))<
Composing them:

<pre>
-       (2) ((join MG') -v- (MM &gamma;)) assigns to `C1` the morphism join[MG'(C1)] &#8728; MM(&gamma;*).
+       (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>.