How is `arr fst` a natural transformation?

user_11143763 0
Viewed 230

I asked this question a while ago. It was about the following arrow law:

arr fst . first f = f . arr fst -- (.) :: Category k => k b c -> k a b -> k a c

In the comments under the post Asad Saeeduddin explained it in terms of natural transformations. I would like to check whether I got their explanation right and compare it a bit to Bartosz Milewski's article on natural transformations.

So, the definition of natural transformations goes:

We have two categories C and D and functors F, G : C ~> D. A natural transformation α is a family of arrows in D such that:

  1. These arrows go from the results of F to the results of G. That is, for every object a in C there exists an arrow (called the component of α at a) α_a :: F a ~> G a.
  2. For every f :: a ~> b, a and b being objects in C, holds: Gf . α_a = α_b . Ff. That is the naturality.

Basically, we need to figure what four variables are in our case: C, D, F and G.

As far as I get it:

  • C and D are the same category of arbitrary types, k a b being arrows in it, where k is the Arrow instance we are working with. Therefore, F and G are endofunctors.

  • F is (, c) and G is Identity. In other words, if we no longer work with types, we map F with first and G with id. It would probably be easier NOT to think in terms of types as the Category and Arrow classes help us construct category's arrows, not objects

Is this right?

Moreover, Bartosz Milewski wrote those ideas down like that:

fmap f . alpha = alpha . fmap f

As far as I get it, we need a more general form for our purposes as here alpha :: forall a. F a -> G a deals with Hask only as the category it works with. Or am I wrong? Which place does fmap have in this picture?

category-theory arrows functor haskell
2 Answers

As far as I get it:

  • C and D are the same category of arbitrary types, k a b being arrows in it, where k is the Arrow instance we are working with. Therefore, F and G are endofunctors.

  • F is (, c) and G is Identity. In other words, if we no longer work with types, we map F with first and G with id. [...]

Yup, that's it. Every choice of k and c in arr fst :: k (b, c) b gives us a natural transformation between the (, c) endofunctor and the identity functor in the k-category. Carrying out the specialisations gives us a signature that looks more obviously like that of a natural transformation:

arr @K (fst @_ @C) :: forall b. K (b, C) b

Moreover, Bartosz Milewski wrote those ideas down like that:

fmap f . alpha = alpha . fmap f

As far as I get it, we need a more general form for our purposes as here alpha :: forall a. F a -> G a deals with Hask only as the category it works with. Or am I wrong? Which place does fmap have in this picture?

Also correct. fmap would have to be replaced by whatever the appropriate morphism mappings are for the involved functors. In your example, these happen to be first and id, as you had noticed before, which brings us back to the arrow law we began with.

(As for replacing fmap, the method of Functor which abstracts from specific functor morphism mappings, by a more general analogue, that requires making the proper arrangements so that we can express functors involving non-Hask categories in Haskell code. You might want to have a look at how constrained-categories and data-category handle that.)

user_27518510

You don't need to worry about extra categories, because arr fst doesn't involve an arbitrary Arrow, just the (,) instance of it.

In Haskell, a function of type f a -> g a for some functors f and c is a natural transformation. In the case of arr fst :: (b -> c) -> (b, c), let f ~ (->) b and g ~ (,) b.

user_11268410
Related