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/
(->) is often called the "function arrow" or "function type constructor", and while it does have some special syntax, there's not that much special about it. It's essentially an infix type operator. Give it two types, and it gives you the type of functions between those types.
The Arrow (either (->) or MyArr ) is an abstraction of a computation. For a function b -> c , b is the input and c is the output. For a MyArr b c , b is the input and c is the output. 2) To actually run an arrow computation, you use a function specific to your arrow type.
The left arrow gets used in do notation as something similar to variable binding, in list comprehensions for the same (I'm assuming they are the same, as list comprehensions look like condensed do blocks), and in pattern guards, which have the form (p <- e). All of those constructs bind a new variable.
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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With