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

1
votes

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

1
haskellcategory-theory
What about data F a = F (a -> a) ? This is neither covariant nor contravariant. – chi
Isn't that an invariant functor: hackage.haskell.org/package/invariant-0.5.4/docs/… – Labbekak
Contravariant functors aren't really mappings Type -> Type but rather Hask -> Hask⁰ᵠ (opposite category). If you mean Hask -> Hask then the answer is no. If you do allow for other categories then the answer will certainly be yes in some boring trivial sense. – leftaroundabout
If you get to choose your category, everything is a functor. – n. 1.8e9-where's-my-share m.
@Labbekak Quoting from your link "Any * -> * type parametric in the argument permits an instance of Invariant.". Hence, yes, it's an invariant functor but it looks like everything is. Perhaps you could rephrase the question as "is there some F :: * -> * which is not an invariant functor?". – chi

1 Answers

4
votes

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.