From: Jim Pryor Date: Tue, 2 Nov 2010 01:15:56 +0000 (-0400) Subject: tweak cat theory X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=3a4225f3e0df9583725eac59035ffd6edb53d888 tweak cat theory Signed-off-by: Jim Pryor --- diff --git a/advanced_topics/monads_in_category_theory.mdwn b/advanced_topics/monads_in_category_theory.mdwn index 3c80bbbc..6ebcd8d6 100644 --- a/advanced_topics/monads_in_category_theory.mdwn +++ b/advanced_topics/monads_in_category_theory.mdwn @@ -35,7 +35,7 @@ Some examples of monoids are: 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`. @@ -43,8 +43,7 @@ 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] + (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. @@ -53,13 +52,11 @@ A good intuitive picture of a category is as a generalized directed graph, where 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) @@ -67,16 +64,14 @@ Some examples of categories are: 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`. @@ -86,14 +81,13 @@ I'll assert without proving that functor composition is associative. -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)`. @@ -130,10 +124,14 @@ 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`: +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." @@ -152,40 +150,62 @@ 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. +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 <=<. (*