Search code examples
haskellcategory-theory

Is every type constructor (`Type -> Type`) some kind of functor


It is well-known that a type constructor with kind Type -> Type (in System F-omega) is only a Functor if it implements a function (a -> b) -> f a -> f b. This is a lawless functor though, it should also adhere to the functor laws (preserve composition and identity). So a type constructor with Type -> Type is not always a functor. But this is only about covariant endofunctors in the category of types. There's also contravariant functors and many more kinds of functors.

My question: is any type constructor/function with kind Type -> Type some kind of (category-theoretic) lawful functor (covariant, contravariant, or some other kind)?


Solution

  • Yes, it is always a functor to and from the discrete category (a category with only identity arrows) of Haskell types. It assigns to every object a an object f a. And we have automatically an arrow f a -> f a, namely the identity function, for every arrow (which are only identity functions) a -> a. The laws hold trivially since the only composition that is going on is identity arrows composed with themselves.