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 fmap
s 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.