+++ /dev/null
-**Don't try to read this yet!!! Many substantial edits are still in process.
-Will be ready soon.**
-
-Caveats
--------
-I really don't know much category theory. Just enough to put this
-together. Also, this really is "put together." I haven't yet found an
-authoritative source (that's accessible to a category theory beginner like
-myself) that discusses the correspondence between the category-theoretic and
-functional programming uses of these notions in enough detail to be sure that
-none of the pieces here is misguided. In particular, it wasn't completely
-obvious how to map the polymorphism on the programming theory side into the
-category theory. And I'm bothered by the fact that our `<=<` operation is only
-partly defined on our domain of natural transformations. But these do seem to
-me to be the reasonable way to put the pieces together. We very much welcome
-feedback from anyone who understands these issues better, and will make
-corrections.
-
-
-Monoids
--------
-A **monoid** is a structure `(S, *, z)` consisting of an associative binary operation `*` over some set `S`, which is closed under `*`, and which contains an identity element `z` for `*`. That is:
-
- for all s1,s2,s3 in S:
- (i) s1*s2 etc are also in S
- (ii) (s1*s2)*s3 = s1*(s2*s3)
- (iii) z*s1 = s1 = s1*z
-
-Some examples of monoids are:
-
-* finite strings of an alphabet `A`, with `*` being concatenation and `z` being the empty string
-* all functions `X->X` over a set `X`, with `*` being composition and `z` being the identity function over `X`
-* the natural numbers with `*` 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 `*` be multiplication and `z` be `1`, we get different monoids over the same sets as in the previous item.
-
-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."
-
-When a morphism `f` in category `C` has source `c1` and target `c2`, we'll write `f:c1->c2`.
-
-To have a category, the elements and morphisms have to satisfy some constraints:
-
- (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]
-
-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.)
-
-
-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.
-
-* 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:
-
- * 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
------------
-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)
-
-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`.
-
-How functors compose: If `G` is a functor from category `C` to category `D`, and `K` is a functor from category `D` to category `E`, then `KG` is a functor which maps every element `c1` of `C` to element `K(G(c1))` of `E`, and maps every morphism `f` of `C` to morphism `K(G(f))` of `E`.
-
-I'll assert without proving that functor composition is associative.
-
-
-
-4. 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]
-
-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)`.
-
-
-How natural transformations compose:
-
-Consider four categories `B`, `C`, `D`, and `E`. Let `F` be a functor from `B` to `C`; `G`, `H`, and `J` be functors from `C` to `D`; and `K` and `L` be functors from `D` to `E`. Let `eta` be a natural transformation from `G` to `H`; `phi` be a natural transformation from `H` to `J`; and `psi` be a natural transformation from `K` to `L`. Pictorally:
-
- - B -+ +--- C --+ +---- D -----+ +-- E --
- | | | | | |
- F: ------> G: ------> K: ------>
- | | | | | eta | | | psi
- | | | | v | | v
- | | H: ------> L: ------>
- | | | | | phi | |
- | | | | v | |
- | | J: ------> | |
- -----+ +--------+ +------------+ +-------
-
-Then `(eta F)` is a natural transformation from the (composite) functor `GF` to the composite functor `HF`, such that where `b1` is an element of category `B`, `(eta F)[b1] = eta[F(b1)]`---that is, the morphism in `D` that `eta` assigns to the element `F(b1)` of `C`.
-
-And `(K eta)` is a natural transformation from the (composite) functor `KG` to the (composite) functor `KH`, such that where `c1` is an element of category `C`, `(K eta)[c1] = K(eta[c1])`---that is, the morphism in `E` that `K` assigns to the morphism `eta[c1]` of `D`.
-
-
-`(phi -v- eta)` is a natural transformation from `G` to `J`; this is known as a "vertical composition". We will rely later on this, where `f:c1->c2`:
-
- phi[c2] o H(f) o eta[c1] = phi[c2] o H(f) o eta[c1]
-
-by naturalness of phi, is:
-
- phi[c2] o H(f) o eta[c1] = J(f) o phi[c1] o eta[c1]
-
-by naturalness of eta, is:
-
- 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`:
-
- (phi -v- eta)[c2] o G(f) = J(f) o (phi -v- eta)[c1]
-
-I'll assert without proving that vertical composition is associative and has an identity, which we'll call "the identity transformation."
-
-
-`(psi -h- eta)` is natural transformation from the (composite) functor `KG` to the (composite) functor `LH`; this is known as a "horizontal composition." It's trickier to define, but we won't be using it here. For reference:
-
- (phi -h- eta)[c1] = L(eta[c1]) o psi[G(c1)]
- = psi[H(c1)] o K(eta[c1])
-
-Horizontal composition is also associative, and has the same identity as vertical composition.
-
-
-
-Monads
-------
-In earlier days, these were also called "triples."
-
-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.
-
-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).
-
-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:
-
- 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
-
-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:
-
- for all p,q,r in T:
- (i) q <=< p etc are also in T
- (ii) (r <=< q) <=< p = r <=< (q <=< p)
- (iii.1) (unit P') <=< p = p
- (iii.2) p = p <=< (unit P)
-
-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
---------------------------------------------------------------
-In category theory, the monad laws are usually stated in terms of unit and join instead of unit and <=<.
-
-(*
- P2. every element c1 of a category C has an identity morphism id[c1] such that for every morphism f:c1->c2 in C: id[c2] o f = f = f o id[c1].
- P3. functors "preserve identity", that is for every element c1 in F's source category: F(id[c1]) = id[F(c1)].
-*)
-
-Let's remind ourselves of some principles:
- * composition of morphisms, functors, and natural compositions is associative
- * functors "distribute over composition", that is for any morphisms f and g in F's source category: F(g o f) = F(g) o F(f)
- * if eta is a natural transformation from F to G, then for every f:c1->c2 in F and G's source category C: eta[c2] o F(f) = G(f) o eta[c1].
-
-
-Let's use the definitions of naturalness, and of composition of natural transformations, to establish two lemmas.
-
-
-Recall that join is a natural transformation from the (composite) functor MM to M. So for elements c1 in C, join[c1] will be a morphism from MM(c1) to M(c1). And for any morphism f:a->b in C:
-
- (1) join[b] o MM(f) = M(f) o join[a]
-
-Next, consider the composite transformation ((join MQ') -v- (MM q)).
- q is a transformation from Q to MQ', and assigns elements c1 in C a morphism q*: Q(c1) -> MQ'(c1). (MM q) is a transformation that instead assigns c1 the morphism MM(q*).
- (join MQ') is a transformation from MMMQ' to MMQ' that assigns c1 the morphism join[MQ'(c1)].
- Composing them:
- (2) ((join MQ') -v- (MM q)) assigns to c1 the morphism join[MQ'(c1)] o MM(q*).
-
-Next, consider the composite transformation ((M q) -v- (join Q)).
- (3) This assigns to c1 the morphism M(q*) o join[Q(c1)].
-
-So for every element c1 of C:
- ((join MQ') -v- (MM q))[c1], by (2) is:
- join[MQ'(c1)] o MM(q*), which by (1), with f=q*: Q(c1)->MQ'(c1) is:
- M(q*) o join[Q(c1)], which by 3 is:
- ((M q) -v- (join Q))[c1]
-
-So our (lemma 1) is: ((join MQ') -v- (MM q)) = ((M q) -v- (join Q)), where q is a transformation from Q to MQ'.
-
-
-Next recall that unit is a natural transformation from 1C to M. So for elements c1 in C, unit[c1] will be a morphism from c1 to M(c1). And for any morphism f:a->b in C:
- (4) unit[b] o f = M(f) o unit[a]
-
-Next consider the composite transformation ((M q) -v- (unit Q)). (5) This assigns to c1 the morphism M(q*) o unit[Q(c1)].
-
-Next consider the composite transformation ((unit MQ') -v- q). (6) This assigns to c1 the morphism unit[MQ'(c1)] o q*.
-
-So for every element c1 of C:
- ((M q) -v- (unit Q))[c1], by (5) =
- M(q*) o unit[Q(c1)], which by (4), with f=q*: Q(c1)->MQ'(c1) is:
- unit[MQ'(c1)] o q*, which by (6) =
- ((unit MQ') -v- q)[c1]
-
-So our lemma (2) is: (((M q) -v- (unit Q)) = ((unit MQ') -v- q)), where q is a transformation from Q to MQ'.
-
-
-Finally, we substitute ((join Q') -v- (M q) -v- p) for q <=< p in the monad laws. For simplicity, I'll omit the "-v-".
-
- for all p,q,r in T, where p is a transformation from P to MP', q is a transformation from Q to MQ', R is a transformation from R to MR', and P'=Q and Q'=R:
-
- (i) q <=< p etc are also in T
- ==>
- (i') ((join Q') (M q) p) etc are also in T
-
-
- (ii) (r <=< q) <=< p = r <=< (q <=< p)
- ==>
- (r <=< q) is a transformation from Q to MR', so:
- (r <=< q) <=< p becomes: (join R') (M (r <=< q)) p
- which is: (join R') (M ((join R') (M r) q)) p
- substituting in (ii), and helping ourselves to associativity on the rhs, we get:
-
- ((join R') (M ((join R') (M r) q)) p) = ((join R') (M r) (join Q') (M q) p)
- ---------------------
- which by the distributivity of functors over composition, and helping ourselves to associativity on the lhs, yields:
- ------------------------
- ((join R') (M join R') (MM r) (M q) p) = ((join R') (M r) (join Q') (M q) p)
- ---------------
- which by lemma 1, with r a transformation from Q' to MR', yields:
- -----------------
- ((join R') (M join R') (MM r) (M q) p) = ((join R') (join MR') (MM r) (M q) p)
-
- which will be true for all r,q,p just in case:
-
- ((join R') (M join R')) = ((join R') (join MR')), for any R'.
-
- which will in turn be true just in case:
-
- (ii') (join (M join)) = (join (join M))
-
-
- (iii.1) (unit P') <=< p = p
- ==>
- (unit P') is a transformation from P' to MP', so:
- (unit P') <=< p becomes: (join P') (M unit P') p
- which is: (join P') (M unit P') p
- substituting in (iii.1), we get:
- ((join P') (M unit P') p) = p
-
- which will be true for all p just in case:
-
- ((join P') (M unit P')) = the identity transformation, for any P'
-
- which will in turn be true just in case:
-
- (iii.1') (join (M unit) = the identity transformation
-
-
- (iii.2) p = p <=< (unit P)
- ==>
- p is a transformation from P to MP', so:
- unit <=< p becomes: (join P') (M p) unit
- substituting in (iii.2), we get:
- p = ((join P') (M p) (unit P))
- --------------
- which by lemma (2), yields:
- ------------
- p = ((join P') ((unit MP') p)
-
- which will be true for all p just in case:
-
- ((join P') (unit MP')) = the identity transformation, for any P'
-
- which will in turn be true just in case:
-
- (iii.2') (join (unit M)) = the identity transformation
-
-
-Collecting the results, our monad laws turn out in this format to be:
-
- when p a transformation from P to MP', q a transformation from P' to MQ', r a transformation from Q' to MR' all in T:
-
- (i') ((join Q') (M q) p) etc also in T
-
- (ii') (join (M join)) = (join (join M))
-
- (iii.1') (join (M unit)) = the identity transformation
-
- (iii.2')(join (unit M)) = the identity transformation
-
-
-
-7. 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.
-
-The base category C will have types as elements, and monadic functions as its morphisms. The source and target of a morphism will be the types of its argument and its result. (As always, there can be multiple distinct morphisms from the same source to the same target.)
-
-A monad M will consist of a mapping from types c1 to types M(c1), and a mapping from functions f:c1->c2 to functions M(f):M(c1)->M(c2). This is also known as "fmap f" or "liftM f" for M, and is called "function f lifted into the monad M." For example, where M is the list monad, M maps every type X into the type "list of Xs", and maps every function f:x->y into the function that maps [x1,x2...] to [y1,y2,...].
-
-
-
-
-A natural transformation t assigns to each type c1 in C a morphism t[c1]: c1->M(c1) such that, for every f:c1->c2:
- t[c2] o f = M(f) o t[c1]
-
-The composite morphisms said here to be identical are morphisms from the type c1 to the type M(c2).
-
-
-
-In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad" in question.
-
-For an example of the latter, let p be a function that takes arguments of some (schematic, polymorphic) type c1 and yields results of some (schematic, polymorphic) type M(c2). An example with M being the list monad, and c2 being the tuple type schema int * c1:
-
- let p = fun c -> [(1,c), (2,c)]
-
-p is polymorphic: when you apply it to the int 0 you get a result of type "list of int * int": [(1,0), (2,0)]. When you apply it to the char 'e' you get a result of type "list of int * char": [(1,'e'), (2,'e')].
-
-However, to keep things simple, we'll work instead with functions whose type is settled. So instead of the polymorphic p, we'll work with (p : c1 -> M(int * c1)). This only accepts arguments of type c1. For generality, I'll talk of functions with the type (p : c1 -> M(c1')), where we assume that c1' is a function of c1.
-
-A "monadic value" is any member of a type M(c1), for any type c1. 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 (p : c1 -> M(c1')) to an argument of type c1.
-
-