Insights into why a contravariant type can’t be a Haskell Functor

In learning Haskell’s core types, type classes, and concepts, one often finds counterexamples useful in learning what certain abstract concepts “really are”. One of the more commmon type class hierarchies is Functor-Applicative-Monad. We encounter Functor in the context of things that are “mappable”. It’s a producer, and using fmap we can “post-transform” all of the things that it produces in a way that preserves any underlying structure.

We quickly become familiar with a number of useful functors, like Maybe, [], (->) r, IO. Functors seem to be everywhere. So, one asks, what might be a parameterized type that’s not a functor? The go-to example is something that’s contravariant in its type parameter, like a -> Int, as a type-level function of parameter a. There doesn’t seem to be any useful way to make it a Functor in a. That said, seemingly “useless” type-level artifacts are often quite useful, like the Const Functor, defined as Const r a ~= r (the a is a phantom type and functions being fmaped are ignored). So usefulness in this world isn’t always intuitive. Still, it remains true that something like a -> Int is not a functor? Why?

Let’s work with the type a -> Bool, just because it’s the simplest example of what goes wrong. Is there a way to make a Functor instance for that? To me, it’s not intuitive that that thing isn’t a Functor. It’s “almost” a set (stepping around, for a moment, debates about what is a set) and Set, meaning the actual collection type in Data.Set is “almost” a Functor. It’s not one, because a Functor demands that the mapping be structure-preserving, which a set’s notion of mapping is not (for example, if you map the squaring function on the set {2, -2}, you get a smaller set, {4}). There are many ways to get at the point that Set is not a Functor, most relying on the fact that Set a‘s methods almost invariably require Eq a and Ord a. But what about the type-agnostic “(<-) a” (my notation) above? It places no such constraints on a.

To answer this, let’s try to create the method, fmap, on which Functor relies.

-- pretend Haskell supports (<-) b a as a syntax for (->) a b = a -> b

instance Functor (<-) Bool where

-- fmap :: (a -> b) -> f a -> f b
-- in this case, (a -> b) -> (a -> Bool) -> (b -> Bool)
fmap f x = ??

The type signature that we’re demanding of our fmap is an interesting one: (a -> b) -> (a -> Bool) -> (b -> Bool). Notice that such a function doesn’t have any a to work with. One might not exist: the Functor needs to be valid over empty types (e.g. Void; note that [Void] is not empty but has exactly one element, []). In typical Functor cases, the a = Void case is handled soundly. For example, consider the list case: ([] :: [Void] maps to [] :: [b] for any b), and any non-empty list has as to work with. In this case, fmap‘s type signature gives us two things that we can do with a‘s but no a. This means that we have to ignore the first two arguments; we can’t use them.

instance Functor (<-) Bool where

-- fmap :: (a -> b) -> f a -> f b
-- in this case, (a -> b) -> (a -> Bool) -> (b -> Bool)
fmap _ _ = (?? :: b -> Bool)

This rules out any useful Functors. In fact, our need for an expression that inhabits b -> Bool for any b limits us to two non-pathological possibilities: the constant functions! Since we don’t have any b to work with, either, we have to commit to one of those. Without loss of generality, I’m going to use the definition fmap _ _ = const True. With a few tweaks to what I’ve done, Haskell will actually allow such a “Functor” instance to be created. But will it be right? It turns out that it won’t be. To show this, we consult the laws for the Functor type class. In fact, we only need the simplest one (Identity): fmap id === id to refute this one. That law is violated by the constant “Functor” above:

fmap id (const True) = const True -- OK!
fmap id (const False) = const True -- whoops!

So it turns out that (<-) Bool (my notation) has no Functor instances at all (the only properly polymorphic candidate fails the type class’s most basic law) and the more complicated cases fail similarly.