What categorical concept do the `fmap_i` mappings (implied by an applicative) formed?

Question

According to Programming in Haskell by Hutton, in Haskell, class Functor is declared as:

class   Functor f   where
fmap    ::  (a  ->  b)  ->  f   a   ->  f   b

Is it correct that f and fmap form an endofunctor on the category of types?

Class Applicative is declared as:

class Functor f   =>  Applicative f   where
pure  ::  a   ->  f   a
(<*>) ::  f   (a  ->  b)  ->  f   a   ->  f   b

which provides:

fmap0 ::  a   ->  f   a
fmap0 =   pure
fmap1 ::  (a  ->  b)  ->  f   a   ->  f   b
fmap1 g   x   =   pure    g   <*> x
fmap2 ::  (a  ->  b   ->  c)  ->  f   a   ->  f   b   ->  f   c
fmap2 g   x   y   =   pure    g   <*> x   <*> y
fmap3 ::  (a  ->  b   ->  c   ->  d)  ->  f   a   ->  f   b   ->  f   c   ->  f   d
fmap3 g   x   y   z   =   pure    g   <*> x   <*> y   <*> z

Is it correct that fmap0 and fmap1 form an endofunctor on the category of types?

Do fmap0, fmap1, and fmap2 form an endofunctor too? If not, what categorical concept do they form?

Similar questions for fmap0, fmap1, fmap2, and fmap3, and for more.

Thanks.

Answer 1

The answer is yes and no.

When you declare a Functor, you're promising the users of your code that composition and identity are preserved by the functor, but Haskell's type checker doesn't check that for you.

Likewise, when you declare an Applicative, you're promising users that the axioms for a lax monoidal functor with strength are satisfied. But again, this isn't verified by the type checker.

Newer languages in the ML family (Agda or Idris, say) can exhibit "verified" versions of Functor and Applicative, which require the programmer to provide proofs that the axioms are satisfied along with the definitions.