Categories
----------
-A **category** is a generalization of a monoid. A category consists of a class of elements, and a class of **morphisms** between those elements. Morphisms are sometimes also called maps or arrows. They are something like functions (and as we'll see below, given a set of functions they'll determine a category). However, a single morphism only maps between a single source element and a single target element. Also, there can be multiple distinct morphisms between the same source and target, so the identity of a morphism goes beyond its "extension."
+A **category** is a generalization of a monoid. A category consists of a class of **elements**, and a class of **morphisms** between those elements. Morphisms are sometimes also called maps or arrows. They are something like functions (and as we'll see below, given a set of functions they'll determine a category). However, a single morphism only maps between a single source element and a single target element. Also, there can be multiple distinct morphisms between the same source and target, so the identity of a morphism goes beyond its "extension."
When a morphism `f` in category `C` has source `c1` and target `c2`, we'll write `f:c1->c2`.
(i) the class of morphisms has to be closed under composition: where f:c1->c2 and g:c2->c3, g o f is also a morphism of the category, which maps c1->c3.
(ii) composition of morphisms has to be associative
- (iii) every element e of the category has to have an identity morphism id[e], which is such that for every morphism f:c1->c2:
- id[c2] o f = f = f o id[c1]
+ (iii) every element e of the category has to have an identity morphism id[e], which is such that for every morphism f:c1->c2: id[c2] o f = f = f o id[c1]
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.
Some examples of categories are:
-* Categories whose elements are sets and whose morphisms are functions between those sets. Here the source and target of a function are its domain and range, so distinct functions sharing a domain and range (e.g., sin and cos) are distinct morphisms between the same source and target elements. The identity morphism for any element is the identity function over that set.
+* Categories whose elements are sets and whose morphisms are functions between those sets. Here the source and target of a function are its domain and range, so distinct functions sharing a domain and range (e.g., sin and cos) are distinct morphisms between the same source and target elements. The identity morphism for any element/set is just the identity function for that set.
-* any monoid `(S,*,z)` 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 `s3=s1+s2`. The identity morphism for the (single) category element `x` is the monoid's identity `z`.
+* any monoid `(S,*,z)` 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 `s3=s1*s2`. The identity morphism for the (single) category element `x` is the monoid's identity `z`.
-* a **preorder** is a structure `(S, <=)` 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 `x<=y` nor `y<=x`). It need not be anti-symmetric (that is, there may be members `s1`,`s2` of `S` such that `s1<=s2` and `s2<=s1` but `s1` and `s2` are not identical).
-
- Some examples:
+* a **preorder** is a structure `(S, <=)` 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 `x<=y` nor `y<=x`). It need not be anti-symmetric (that is, there may be members `s1`,`s2` of `S` such that `s1<=s2` and `s2<=s1` 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)
Any pre-order `(S,<=)` generates a category whose elements are the members of `S` and which has only a single morphism between any two elements `s1` and `s2`, iff `s1<=s2`.
-3. Functors
------------
+Functors
+--------
A **functor** is a "homomorphism", that is, a structure-preserving mapping, between categories. In particular, a functor `F` from category `C` to category `D` must:
(i) associate with every element c1 of C an element F(c1) of D
(ii) associate with every morphism f:c1->c2 of C a morphism F(f):F(c1)->F(c2) of D
- (iii) "preserve identity", that is, for every element c1 of C: F of c1's identity morphism in C must be the identity morphism of F(c1) in D:
- F(id[c1]) = id[F(c1)].
- (iv) "distribute over composition", that is for any morphisms f and g in C:
- F(g o f) = F(g) o F(f)
+ (iii) "preserve identity", that is, for every element c1 of C: F of c1's identity morphism in C must be the identity morphism of F(c1) in D: F(id[c1]) = id[F(c1)].
+ (iv) "distribute over composition", that is for any morphisms f and g in C: F(g o f) = F(g) o F(f)
A functor that maps a category to itself is called an **endofunctor**. The (endo)functor that maps every element and morphism of `C` to itself is denoted `1C`.
-4. Natural Transformation
--------------------------
+Natural Transformation
+----------------------
So categories include elements and morphisms. Functors consist of mappings from the elements and morphisms of one category to those of another (or the same) category. **Natural transformations** are a third level of mappings, from one functor to another.
Where `G` and `H` are functors from category `C` to category `D`, a natural transformation `eta` between `G` and `H` is a family of morphisms `eta[c1]:G(c1)->H(c1)` in `D` for each element `c1` of `C`. That is, `eta[c1]` has as source `c1`'s image under `G` in `D`, and as target `c1`'s image under `H` in `D`. The morphisms in this family must also satisfy the constraint:
- for every morphism f:c1->c2 in C:
- eta[c2] o G(f) = H(f) o eta[c1]
+ for every morphism f:c1->c2 in C: eta[c2] o G(f) = H(f) o eta[c1]
That is, the morphism via `G(f)` from `G(c1)` to `G(c2)`, and then via `eta[c2]` to `H(c2)`, is identical to the morphism from `G(c1)` via `eta[c1]` to `H(c1)`, and then via `H(f)` from `H(c1)` to `H(c2)`.
phi[c2] o eta[c2] o G(f) = J(f) o phi[c1] o eta[c1]
-Hence, we can define `(phi -v- eta)[c1]` as: `phi[c1] o eta[c1]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
+Hence, we can define `(phi -v- eta)[x]` as: `phi[x] o eta[x]` and rely on it to satisfy the constraints for a natural transformation from `G` to `J`:
(phi -v- eta)[c2] o G(f) = J(f) o (phi -v- eta)[c1]
+An observation we'll rely on later: given the definitions of vertical composition and of how natural transformations compose with functors, it follows that:
+
+ ((phi -v- eta) F) = ((phi F) -v- (eta F))
+
I'll assert without proving that vertical composition is associative and has an identity, which we'll call "the identity transformation."
A **monad** is a structure consisting of an (endo)functor `M` from some category `C` to itself, along with some natural transformations, which we'll specify in a moment.
-Let T be a set of natural transformations p, each being between some (variable) functor P and another functor which is the composite MP' of M and a (variable) functor P'. That is, for each element c1 in C, p assigns c1 a morphism from element P(c1) to element MP'(c1), satisfying the constraints detailed in the previous section. For different members of T, the relevant functors may differ; that is, p is a transformation from functor P to MP', q is a transformation from functor Q to MQ', and none of P,P',Q,Q' need be the same.
+Let `T` be a set of natural transformations `p`, each being between some (variable) functor `P` and another functor which is the composite `MP'` of `M` and a (variable) functor `P'`. That is, for each element `c1` in `C`, `p` assigns `c1` a morphism from element `P(c1)` to element `MP'(c1)`, satisfying the constraints detailed in the previous section. For different members of `T`, the relevant functors may differ; that is, `p` is a transformation from functor `P` to `MP'`, `q` is a transformation from functor `Q` to `MQ'`, and none of `P`, `P'`, `Q`, `Q'` 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 on C 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 `C` 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 p and q be members of T, that is they are natural transformations from P to MP' and from Q to MQ', respectively. Let them be such that P' = Q. Now (M q) will also be a natural transformation, formed by composing the functor M with the natural transformation q. Similarly, (join Q') will be a natural transformation, formed by composing the natural transformation join with the functor Q'; it will transform the functor MMQ' to the functor MQ'. Now take the vertical composition of the three natural transformations (join Q'), (M q), and p, and abbreviate it as follows:
+Let `p` and `q` be members of `T`, that is they are natural transformations from `P` to `MP'` and from `Q` to `MQ'`, respectively. Let them be such that `P' = Q`. Now `(M q)` will also be a natural transformation, formed by composing the functor `M` with the natural transformation `q`. Similarly, `(join Q')` will be a natural transformation, formed by composing the natural transformation `join` with the functor `Q'`; it will transform the functor `MMQ'` to the functor `MQ'`. Now take the vertical composition of the three natural transformations `(join Q')`, `(M q)`, and `p`, and abbreviate it as follows:
- q <=< p =def. ((join Q') -v- (M q) -v- p) --- since composition is associative I don't specify the order of composition on the rhs
+ q <=< p =def. ((join Q') -v- (M q) -v- p)
-In other words, <=< is a binary operator that takes us from two members p and q of T to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes its written p >=> q where that's the same as q <=< p.)
+Since composition is associative I don't specify the order of composition on the rhs.
-p is a transformation from P to MP' which = MQ; (M q) is a transformation from MQ to MMQ'; and (join Q') is a transformation from MMQ' to MQ'. So the composite q <=< p will be a transformation from P to MQ', and so also eligible to be a member of T.
+In other words, `<=<` is a binary operator that takes us from two members `p` and `q` of `T` to a composite natural transformation. (In functional programming, at least, this is called the "Kleisli composition operator". Sometimes its written `p >=> q` where that's the same as `q <=< p`.)
+
+`p` is a transformation from `P` to `MP'` which = `MQ`; `(M q)` is a transformation from `MQ` to `MMQ'`; and `(join Q')` is a transformation from `MMQ'` to `MQ'`. So the composite `q <=< p` will be a transformation from `P` to `MQ'`, and so also eligible to be a member of `T`.
Now we can specify the "monad laws" governing a monad as follows:
(T, <=<, unit) constitute a monoid
-That's it. In other words:
+That's it. (Well, perhaps we're cheating a bit, because `q <=< p` isn't fully defined on `T`, but only when `P` is a functor to `MP'` and `Q` is a functor from `P'`. But wherever `<=<` is defined, the monoid laws are satisfied:
- for all p,q,r in T:
- (i) q <=< p etc are also in T
+ (i) q <=< p is also in T
(ii) (r <=< q) <=< p = r <=< (q <=< p)
- (iii.1) (unit P') <=< p = p
- (iii.2) p = p <=< (unit P)
+ (iii.1) unit <=< p = p (here p has to be a natural transformation to M(1C))
+ (iii.2) p = p <=< unit (here p has to be a natural transformation from 1C)
+
+If `p` is a natural transformation from `P` to `M(1C)` and `q` is `(p Q')`, that is, a natural transformation from `PQ` to `MQ`, then we can extend (iii.1) as follows:
+
+ q = (p Q')
+ = ((unit <=< p) Q')
+ = ((join -v- (M unit) -v- p) Q')
+ = (join Q') -v- ((M unit) Q') -v- (p Q')
+ = (join Q') -v- (M (unit Q')) -v- q
+ = (unit Q') <=< q
+
+where as we said `q` is a natural transformation from some `PQ'` to `MQ'`.
+
+Similarly, if `p` is a natural transformation from `1C` to `MP'`, and `q` is `(p Q)`, that is, a natural transformation from `Q` to `MP'Q`, then we can extend (iii.2) as follows:
+
+ q = (p Q)
+ = ((p <=< unit) Q)
+ = (((join P') (M p) unit) Q)
+ = ((join P'Q) ((M p) Q) (unit Q))
+ = ?
+ = q <=< (unit Q)
+
+where as we said `q` is a natural transformation from `Q` to some `MP'Q`.
-A word about the P' and P in (iii.1) and (iii.2): since unit on its own is a transformation from 1C to M(1C), it doesn't have the appropriate "type" for unit <=< p or p <=< unit to be defined, for arbitrary p. However, if p is a transformation from P to MP', then (unit P') <=< p and p <=< (unit P) will both be defined.
-6. The standard category-theory presentation of the monad laws
---------------------------------------------------------------
+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 <=<.
(*