arrows

[Wolfgang Jeltsch]

On Saturday, 2002-05-25, 20:37, CEST Ashley Yakeley wrote: 
> At 2002-05-25 01:32, Koen Claessen wrote:
> 
> >Might I remind you that an arrow (as defined in category
> >theory) only requires identy and composition to be defined
> >and satisfying some laws?
> >
> >In particular, an arrow does not have to have the operations
> >"arr" and "first".
> 
> Well either "arrow" is being used in two different senses or the "Arrow" 
> class should be renamed. If you can't define "arr" and "first", it may be 
> an arrow but it's not an Arrow.
> 
> -- 
> Ashley Yakeley, Seattle WA

Hello,
[1] says that a category consists of
        * a set O of objects;
        * a set M of morphisms or arrows;
        * a pair of functions, dom (domain) and cod (codomain), from M
          to O;
        * for each x `elem` O, an identity morphism 1_x;
        * a partial operation of composition on M, the composition of f
          and g (if it exists) being written fg
If a is a valid instance of the Arrow class as defined today, a category
can be constructed from it using the following rules:
        * O is the set of all Haskell types;
        * M is the set of all values which have type a b c with b and c
          being arbitrary types
        * for all types b and c, for every m :: a b c, dom m = b and cod
          m = c are true
        * 1_x = arr id :: a x x for every type x
        * fg = f >>> g
This way of constructing a category would, of course, also work if Arrow
wouldn't have first, and, with a small modification, even if it wouldn't
have arr but instead have a member for identity --- you would just have
to change arr id to this member.
Note that not arrows but categories "have" operations like id and (>>>).
Including arr or even first in the Arrow class will result in less
categories constructable according to the rules above. But you still
construct categories and the values of type a b c are the arrows of
them. If values of type a b c are arrows it would, strictly speaking,
not wrong to call a's class Arrow, even if it includes operations which
do not belong to a category. But doing so could, of course, be
misleading. I think, it would be better to
        * create a class, which has only an identity and a composition
          member, and call this class Arrow or Morphism;
        * create a subclass of this class which introduces pure (arr);
        * create a subclass of the class introducing pure in order to
          introduce first.

Wolfgang

[1] Peter J. Cameron. Sets, Logic and Categories. Springer-Verlag London
Ltd., 1999