Are there any type constructors which are *not* functors?

So I'm almost done teaching myself category theory. One of the main take-aways for me is that type constructors (higher-kinded types) are endo-functors.

But it this always the case? What's throwing me off is Haskell's Functor typeclass:

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

If all type constructors were a priori functors, there would be no need to define a special type-class. But I can't think of any type-constructors that fail to satisfy the Functor type-class: product, sum, function, list, set, option, etc.

I also cannot imagine the utility of a type-constructors that is "one-half" of a functor, i.e. it has a map from objects to objects, but no map between morphisms.

One obvious counterexample is a binary search tree. You cannot freely substitute the values in a binary search tree because a substitution might change the ordering (relative to Ord), or even replace the values with a type which is not an instance of Ord at all.

A possibly less-obvious example is a contravariant endofunctor. Consider:

data Tricky a = Tricky (a -> String)

Try writing a Functor instance for this.

But that doesn't mean you can't construct a functor-like class which it the type does satisfy. This Tricky type, after all, is a contravariant functor:

-- Somebody has probably already implemented this in a library
-- somewhere, with a better name.
class ContraFunctor f :: * -> * where
    contramap :: (b -> a) -> (f a -> f b)

instance ContraFunctor Tricky where
    contramap f (Tricky t) = Tricky (t . f)

and like fmap, it must satisfy some axioms which are left as an exercise.

What's interesting, though, is that you can usually come up with a functor-like class (and its axioms, of course) which applies type substitutions in a principled way, from the types of the functions which comprise their API.

The full details are beyond the scope, but it's based on a remarkable property of a polymorphic function is known as the "free theorem". Any polymorphic function has a theorem that it satisfies simply by virtue of being polymorphic, and the theorem is mechanically derivable from its type.

What the theorem essentially states is that a polymorphic function commutes with a type substitution. This is what "polymorphic" really means.

Let's take reverse as an example:

reverse :: forall a. [a] -> [a]

There are no constraints whatsoever on the type of a, so it will commute with any type substition:

forall f :: A -> B. fmap f . reverse = reverse . fmap f

(Remember, . is function composition in Haskell.)

This is true for any types A and B. In a deep sense, this is what the "forall" actually means in the type of reverse.

Now consider sort:

sort :: forall a. Ord a => [a] -> [a]

The problem here is that Ord is a constraint on the type of a. What this means is that this is a constraint on any type substitution: it must be a homomorphism of Ord.

forall f :: A -> B.
    (forall x y : A, compare x y = compare (f x) (f y))
    => fmap f . sort = sort . fmap f

That extra precondition, that f is an Ord-homomorphism, intuitively means that f is a function which preserves the order. This should make sense: if a type substitution doesn't change the ordering of elements, then that type substitution commutes with sort.

But here's my favourite example of all. Suppose that F and G are functors. Now consider this function:

eta :: forall a. F a -> G a

The free theorem of this function is:

forall f : A -> B.  fmap f . eta = eta . fmap f

Note that the two fmaps are different instances; the first one is the instance for G and the second is the instance for F. What this is saying is that eta, by virtue of its type alone, is a natural transformation.

StackExchange Computer Science Q#64584, answer score: 11