# 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.

• Thanks for you detailed response! 1. For the binary search tree constructor BST a, I don't think this is a counter-example, because it's not actually a type-constructor. A type-constructor has to be defined on every type; limiting the domain to ordered types precludes this. 2. A contravariant functor is just a normal covariant functor in the dual category, so while technically this is a counter-example, it's not a very interesting one. 3. You're talking about natural transformations. This fact very recently blew my mind. 4. I am going to read the paper you linked – gardenhead Oct 13 '16 at 23:41
• In Haskell, BST could be a generalised algebraic datatype. GADTs allow type constructors to be qualified with constraints such as Ord. See wiki.haskell.org/Data_declaration_with_constraint – Pseudonym Oct 14 '16 at 1:58
• How do GADTs fit into category theory, if at all? – gardenhead Oct 14 '16 at 1:59
• Well enough. They have an obvious Church encoding representation, so in that sense they don't really introduce anything new. – Pseudonym Oct 14 '16 at 2:00
• Implicit type parameters always bothered me in Haskell and SML. Having to explicitly instantiate the polymorphic function with a specific type makes it much clearer what's going on. However, I think we can assume that is being done "under the hood" with type inference. With regards to your second comment, to me the intuition goes the other way; understanding what a natural transformation was made me "get" polymorphic functions. I mean, I understood them before, but category theory showed them in a new light. – gardenhead Oct 14 '16 at 2:11