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

index d5c0941..c45c948 100644 (file)
@@ -8,11 +8,16 @@ 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 this does seem to
-me to be the reasonable way to put the pieces together. We very much welcome
+none of the pieces here is mistaken.
+In particular, it wasn't completely obvious how to map the polymorphism on the
+programming theory side into the category theory. The way I accomplished this
+may be more complex than it needs to be.
+Also I'm bothered by the fact that our `<=<` operation is only partly defined
+on our domain of natural transformations.
+There are three additional points below that I wonder whether may be too
+cavalier.
+But all considered, this does seem to
+me to be a reasonable way to put the pieces together. We very much welcome
feedback from anyone who understands these issues better, and will make
corrections.

@@ -51,12 +56,12 @@ To have a category, the elements and morphisms have to satisfy some constraints:

(ii) composition of morphisms has to be associative

-       (iii) every element E of the category has to have an identity
-             morphism 1<sub>E</sub>, which is such that for every morphism f:C1&rarr;C2:
+       (iii) every element X of the category has to have an identity
+             morphism 1<sub>X</sub>, which is such that for every morphism f:C1&rarr;C2:
1<sub>C2</sub> &#8728; f = f = f &#8728; 1<sub>C1</sub>
</pre>

-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.
+These parallel the constraints for monoids. Note that there can be multiple distinct morphisms between an element `X` 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. Morphisms correspond to directed paths of length &ge; 0 in the graph.

@@ -65,14 +70,14 @@ 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/set is just the identity function for that set.

-*      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`.
+*      any monoid <code>(S,&#8902;,z)</code> generates a category with a single element `Q`; this `Q` 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 `Q` 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 `Q` 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 `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:
+*      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)

-       Any pre-order <code>(S,&le;)</code> 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 <code>s1&le;s2</code>.
+       Any pre-order <code>(S,&le;)</code> 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 <code>s1 &le; s2</code>.

Functors
@@ -229,12 +234,12 @@ If <code>&phi;</code> is a natural transformation from `F` to `M(1C)` and <code>
<pre>
&gamma; = (&phi; G')
= ((unit <=< &phi;) G')
+         since unit is a natural transformation to M(1C), this is:
= (((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 &lt;=&lt;:
+         since (unit G') is a natural transformation to MG', this is:
= (unit G') <=< &gamma;
</pre>

@@ -245,11 +250,11 @@ Similarly, if <code>&rho;</code> is a natural transformation from `1C` to `MR'`,
<pre>
&gamma; = (&rho; G)
= ((&rho; <=< unit) G)
+         = since &rho; is a natural transformation to MR', this is:
= (((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 &lt;=&lt;:
+         since &gamma; = (&rho; G) is a natural transformation to MR'G, this is:
= &gamma; <=< (unit G)
</pre>

@@ -265,10 +270,10 @@ Summarizing then, the monad laws can be expressed as:
(ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)

(iii.1) (unit G') <=< &gamma;  =  &gamma;
-               when &gamma; is a natural transformation from some FG' to MG'
+               whenever &gamma; is a natural transformation from some FG' to MG'

(iii.2)                     &gamma;  =  &gamma; <=< (unit G)
-               when &gamma; is a natural transformation from G to some MR'G
+               whenever &gamma; is a natural transformation from G to some MR'G
</pre>

@@ -282,7 +287,7 @@ In category theory, the monad laws are usually stated in terms of `unit` and `jo
P3. functors "preserve identity", that is for every element C1 in F's source category: F(1<sub>C1</sub>) = 1<sub>F(C1)</sub>.
-->

-Let's remind ourselves of some principles:
+Let's remind ourselves of principles stated above:

*      composition of morphisms, functors, and natural compositions is associative

@@ -290,9 +295,9 @@ Let's remind ourselves of some principles:

*      if <code>&eta;</code> is a natural transformation from `G` to `H`, then for every <code>f:C1&rarr;C2</code> in `G` and `H`'s source category <b>C</b>: <code>&eta;[C2] &#8728; G(f) = H(f) &#8728; &eta;[C1]</code>.

-*      <code>(&eta; F)[E] = &eta;[F(E)]</code>
+*      <code>(&eta; F)[X] = &eta;[F(X)]</code>

-*      <code>(K &eta;)[E} = K(&eta;[E])</code>
+*      <code>(K &eta;)[X] = K(&eta;[X])</code>

*      <code>((&phi; -v- &eta;) F) = ((&phi; F) -v- (&eta; F))</code>

@@ -388,9 +393,9 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
(i) &gamma; <=< &phi; etc are also in T
==>
(i') ((join G') (M &gamma;) &phi;) etc are also in T
+</pre>

-
-
+<pre>
(ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
==>
(&rho; <=< &gamma;) is a transformation from G to MR', so
@@ -409,45 +414,57 @@ Finally, we substitute <code>((join G') -v- (M &gamma;) -v- &phi;)</code> for <c
which by lemma 1, with &rho; a transformation from G' to MR', yields:
((join R') (M join R') (MM &rho;) (M &gamma;) &phi;) = ((join R') (join MR') (MM &rho;) (M &gamma;) &phi;)

-                        which will be true for all &rho;,&gamma;,&phi; only when:
-                ((join R') (M join R')) = ((join R') (join MR')), for any R'.
+                        [-- Are the next two steps too cavalier? --]
+
+                        which will be true for all &rho;, &gamma;, &phi; only when:
+                ((join R') (M join R')) = ((join R') (join MR')), for any R'

which will in turn be true when:
(ii') (join (M join)) = (join (join M))
+</pre>

-
-
+<pre>
(iii.1) (unit G') <=< &gamma;  =  &gamma;
when &gamma; is a natural transformation from some FG' to MG'
==>
(unit G') is a transformation from G' to MG', so:
-                        (unit G') <=< &gamma; becomes: ((join G') (M unit G') &gamma;)
+                        (unit G') <=< &gamma; becomes: ((join G') (M (unit G')) &gamma;)
+                                             which is: ((join G') ((M unit) G') &gamma;)

substituting in (iii.1), we get:
-                        ((join G') (M unit G') &gamma;) = &gamma;
+                        ((join G') ((M unit) G') &gamma;) = &gamma;

-                        which will be true for all &gamma; 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
+                        which is:
+                        (((join (M unit)) G') &gamma;) = &gamma;

+                        [-- Are the next two steps too cavalier? --]

+                        which will be true for all &gamma; just in case:
+                        for any G', ((join (M unit)) G') = the identity transformation

+                        which will in turn be true just in case:
+       (iii.1') (join (M unit)) = the identity transformation
+</pre>

+<pre>
(iii.2) &gamma;  =  &gamma; <=< (unit G)
when &gamma; is a natural transformation from G to some MR'G
==>
-                        unit <=< &gamma; becomes: ((join R'G) (M &gamma;) unit)
+                        &gamma; <=< (unit G) becomes: ((join R'G) (M &gamma;) (unit G))

substituting in (iii.2), we get:
&gamma; = ((join R'G) (M &gamma;) (unit G))

which by lemma 2, yields:
-                        &gamma; = ((join R'G) ((unit MR'G) &gamma;)
+                        &gamma; = (((join R'G) ((unit MR'G) &gamma;)
+
+                        which is:
+                        &gamma; = (((join (unit M)) R'G) &gamma;)
+
+                        [-- Are the next two steps too cavalier? --]

which will be true for all &gamma; just in case:
-                ((join R'G) (unit MR'G)) = the identity transformation, for any R'G
+                        for any R'G, ((join (unit M)) R'G) = the identity transformation

which will in turn be true just in case:
(iii.2') (join (unit M)) = the identity transformation
@@ -483,25 +500,20 @@ The base category <b>C</b> will have types as elements, and monadic functions as
A monad `M` will consist of a mapping from types `'t` to types `M('t)`, and a mapping from functions <code>f:C1&rarr;C2</code> to functions <code>M(f):M(C1)&rarr;M(C2)</code>. This is also known as <code>lift<sub>M</sub> f</code> for `M`, and is pronounced "function f lifted into the monad M." For example, where `M` is the list monad, `M` maps every type `'t` into the type `'t list`, and maps every function <code>f:x&rarr;y</code> into the function that maps `[x1,x2...]` to `[y1,y2,...]`.

-In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad" in question.
-
-A "monadic value" is any member of a type M('t), for any type 't. 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 <code>(&phi; : F('t) &rarr; M(F'('t)))</code> to an argument `a` of type `F('t)`.
-
+In functional programming, instead of working with natural transformations we work with "monadic values" and polymorphic functions "into the monad."

-Let `'t` be a type variable, and `F` and `F'` be functors, and let `phi` be a polymorphic function that takes arguments of type `F('t)` and yields results of type `MF'('t)` in the monad `M`. An example with `M` being the list monad:
+A "monadic value" is any member of a type `M('t)`, for any type `'t`. For example, any `int list` is a monadic value for the list monad. We can think of these monadic values as the result of applying some function `phi`, whose type is `F('t)->M(F'('t))`. `'t` here is any collection of free type variables, and `F('t)` and `F'('t)` are types parameterized on `'t`. An example, with `M` being the list monad, `'t` being `('t1,'t2)`, `F('t1,'t2)` being `char * 't1 * 't2`, and `F'('t1,'t2)` being `int * 't1 * 't2`:

<pre>
let phi = fun ((_:char, x y) -> [(1,x,y),(2,x,y)]
</pre>

-Here phi is defined when `'t = 't1*'t2`, `F('t1*'t2) = char * 't1 * 't2`, and `F'('t1 * 't2) = int * 't1 * 't2`.

-Now where `gamma` is another function into monad `M` of type <code>F'('t) &rarr; MG'('t)</code>, we define:
+Now where `gamma` is another function of type <code>F'('t) &rarr; M(G'('t))</code>, we define:

<pre>
gamma =<< phi a  =def. ((join G') -v- (M gamma)) (phi a)
-
= ((join G') -v- (M gamma) -v- phi) a
= (gamma <=< phi) a
</pre>
@@ -518,59 +530,59 @@ With these definitions, our monadic laws become:

<pre>
-       Where phi is a polymorphic function from type F('t) -> M F'('t)
-       and gamma is a polymorphic function from type G('t) -> M G' ('t)
-       and rho is a polymorphic function from type R('t) -> M R' ('t)
+       Where phi is a polymorphic function of type F('t) -> M(F'('t))
+       gamma is a polymorphic function of type G('t) -> M(G'('t))
+       rho is a polymorphic function of type R('t) -> M(R'('t))
and F' = G and G' = R,
-       and a ranges over values of type F('t) for some type 't,
-       and b ranges over values of type G('t):
+       and a ranges over values of type F('t),
+       b ranges over values of type G('t),
+       and c ranges over values of type G'('t):

(i) &gamma; <=< &phi; is defined,
and is a natural transformation from F to MG'
==>
(i'') fun a -> gamma =<< phi a is defined,
-                         and is a function from type F('t) -> M G' ('t)
-
-
+                         and is a function from type F('t) -> M(G'('t))
+</pre>

+<pre>
(ii) (&rho; <=< &gamma;) <=< &phi;  =  &rho; <=< (&gamma; <=< &phi;)
==>
(fun a -> (rho <=< gamma) =<< phi a)  =  (fun a -> rho =<< (gamma <=< phi) a)
(fun a -> (fun b -> rho =<< gamma b) =<< phi a)  =  (fun a -> rho =<< (gamma =<< phi a))

(ii'') (fun b -> rho =<< gamma b) =<< phi a  =  rho =<< (gamma =<< phi a)
+</pre>

-
-
+<pre>
(iii.1) (unit G') <=< &gamma;  =  &gamma;
when &gamma; is a natural transformation from some FG' to MG'
-
+       ==>
(unit G') <=< gamma  =  gamma
-                         when gamma is a function of type FQ'('t) -> M G'('t)
+                         when gamma is a function of type F(G'('t)) -> M(G'('t))

fun b -> (unit G') =<< gamma b  =  gamma

(unit G') =<< gamma b  =  gamma b

-                         As below, return will map arguments c of type G'('t)
-                         to the monadic value (unit G') b, of type M G'('t).
+                         Let return be a polymorphic function mapping arguments of any
+                         type 't to M('t). In particular, it maps arguments c of type
+                         G'('t) to the monadic value (unit G') c, of type M(G'('t)).

(iii.1'') return =<< gamma b  =  gamma b
+</pre>

-
-
+<pre>
(iii.2) &gamma;  =  &gamma; <=< (unit G)
when &gamma; is a natural transformation from G to some MR'G
==>
gamma  =  gamma <=< (unit G)
-                         when gamma is a function of type G('t) -> M R' G('t)
+                         when gamma is a function of type G('t) -> M(R'(G('t)))

-                         gamma  =  fun b -> gamma =<< ((unit G) b)
+                         gamma  =  fun b -> gamma =<< (unit G) b

-                         Let return be a polymorphic function mapping arguments
-                         of any type 't to M('t). In particular, it maps arguments
-                         b of type G('t) to the monadic value (unit G) b, of
-                         type M G('t).
+                         As above, return will map arguments b of type G('t) to the
+                         monadic value (unit G) b, of type M(G('t)).

gamma  =  fun b -> gamma =<< return b

@@ -588,7 +600,7 @@ Summarizing (ii''), (iii.1''), (iii.2''), these are the monadic laws as usually

*      `return =<< gamma b  =  gamma b`

-       Usually written reversed, and with `u` standing in for `phi a`:
+       Usually written reversed, and with `u` standing in for `gamma b`:

`u >>= return  =  u`