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
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
participants (2)
-
Ashley Yakeley -
Wolfgang Jeltsch