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)?
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.