Is (\f -> fmap f id) always equivalent to arr?
First let's be clear what Arrow C
means. Well, it's two quite separate things combined – in my book,
- The class of well-pointed monoidal categories.
- The class of categories which generalise Hask.
arr
comes from the latter. “Generalise” Hask? What this means is just to have a mapping from the category Hask to C
. – And mathematically, mapping from one category to another is exactly what a functor does! (The standard Functor
class actually covers only a very specific sort of functors, namely endofunctors on Hask.) arr
is the morphism-aspect of a non-endofunctor, namely the “canonical embedding functor” Hask → C
.
From this point of view, the first two arrow laws
arr id = id
arr (f >>> g) = arr f >>> arr g
are just the functor laws.
Now, what does it mean if you're implementing a Functor
instance for a category? Why, I daresay it simply means you're expressing that same canonical embedding functor, but via the necessary representation of C
back in Hask (which makes it an endofunctor overall). Hence I'd argue that yes, \f -> fmap f id
should be equivalent to arr
, since basically they're two ways of expressing the same thing.
Here is a derivation to supplement leftaroundabout's explanation. For clarity, I will reserve (.)
and id
for (->)
, and use (<<<)
and id'
for the general Category
methods.
We begin with preComp
, also known as (>>>)
:
preComp :: Category y => y a b -> (y b c -> y a c)
preComp v = \u -> u <<< v
fmap
commutes with natural transformations between Hask endofunctors. For a Category
which also has a Functor
instance, preComp v
is a natural transformation (from y b
to y a
), and so it commutes with fmap
. It follows that:
fmap f . preComp v = preComp v . fmap f
fmap f (u <<< v) = fmap f u <<< v
fmap f (id' <<< v) = fmap f id' <<< v
fmap f v = fmap f id' <<< v
That's our candidate arr
! So let's define arr' f = fmap f id'
. We can now verify that arr'
follows the first arrow law...
-- arr id = id'
arr' id
fmap id id'
id'
... and the second one too:
-- arr (g . f) = arr g <<< arr f
arr' (g . f)
fmap (g . f) id'
(fmap g . fmap f) id'
fmap g (fmap f id')
fmap g (arr' f)
fmap g id' <<< arr' f -- Using the earlier result.
arr' g <<< arr' f
I suppose that is as far as we can get. The other five arrow laws involve first
, and as leftaroundabout points out arr
and first
are independent.