haskellcategory-theoryarrow-abstraction

Arrow without arr

If we restrict our understanding of a category to be the usual Category class in Haskell:

class Category c where
  id :: c x x
  (>>>) :: c x y -> c y z -> c x z

Then let's say that an Arrow is a Category which can additionally:

class Category c => Arrow c where
  (***) :: c x y -> c x' y' -> c (x,x') (y,y')
  (&&&) :: c x y -> c x y' -> c x (y,y')

We can easily derive:

first :: c x y -> c (x,z) (y,z)
first a = a *** id

second :: c x y -> c (z,x) (z,y)
second a = id *** a

Or we can derive (***) from first and second:

a1 *** a2 = first a1 >>> second a2

We can also derive:

dup :: c x (x,x)
dup = id &&& id

Or we can derive (&&&) given dup and (***):

a1 &&& a2 = dup >>> (a1 *** a2)

What's my point and what's my question? It's this:

What is Arrow without arr? It seems perfectly coherent and useful. Are there any arrow laws (aside from just category laws) that don't involve arr and remain intact here? And what does this all mean in category theory?

I basically stole this question from reddit, but generalized and expounded on it: http://www.reddit.com/r/haskell/comments/2e0ane/category_with_fanout_and_split_but_not_an_arrow/

Solution

  • Just as Arrow is a category with product, Arrow without arr is also a category with product (thus the category laws always hold).

    arr is a functor from Hask category to c category. The code shown below indicates this. arr provides a way to lift normal functions (that are morphisms in Hask) into the instantiated c category. This is somewhat like fmap (endofunctor from Hask to Hask) but more generalized. Relating to this, some of the arrow laws here describe the functor laws (though there are also the laws for product).

    So by omitting arr, you lose the function to lift normal functions, or, from another point of view, get free from implementing it. However, all other characteristics are the same.

    {-# LANGUAGE TypeOperators, RankNTypes #-}

-- | Functor arrow
type (:->) c d = forall a b. c a b -> d a b

-- | Hask category; types are objects, functions are morphisms.
type Hask = (->)

arr :: Arrow c => Hask :-> c
arr = Control.Arrow.arr