Showing that `newtype T a = T (a -> Int)` is a Type Constructor that is Not a Functor

Question

It's been claimed that newtype T a = T (a -> Int) is a type constructor that is not a functor (but is a contravariant functor). How so? Or what is the contravariant functor (whence I assume it will be obvious why this can't be made a normal functor)?

Answer 1

Given

newtype T a = T (a -> Int)

let's try to build the Contravariant instance for this datatype.

Here's the typeclass in question:

class Contravariant f where
  contramap :: (a -> b) -> f b -> f a

Basically, contramap is akin to fmap, but instead of lifting a function a -> b to f a -> f b, it lifts it to f b -> f a.

Let's begin writing the instance...

instance Contravariant T where
  contramap g (T f) = ?

Before we fill in the ?, let's think about what the types of g and f are:

g :: a -> b
f :: b -> Int

And for clarity, we might as well mention that

f a ~ T (a -> Int)
f b ~ T (b -> Int)

So we can fill in the ? as follows:

instance Contravariant T where
  contramap g (T f) = T (f . g)

To be super pedantic, you might rename g as aToB, and f as bToInt.

instance Contravariant T where
  contramap aToB (T bToInt) = T (bToInt . aToB)

The reason you can write a Contravariant instance for T a boils down to the fact that a is in contravariant position in T (a -> Int). The best way to convince yourself that T a isn't a Functor is to try (and fail) to write the Functor instance yourself.

Answer 2

Suppose that T is a functor. Then we have

fmap :: (a -> b) -> T a -> T b

Now, let's try implementing it.

instance Functor T where
  fmap f (T g) = T $ \x -> _y

Clearly we start with something like this, and combine the values f, g, and x somehow to compute a value for y that's of the right type. How can we do that? Well, notice I've called it _y, which tells GHC I need some help figuring out what to put there. What does GHC have to say?

<interactive>:7:28: error:
    • Found hole: _y :: Int
      Or perhaps ‘_y’ is mis-spelled, or not in scope
    • In the expression: _y
      In the second argument of ‘($)’, namely ‘\ x -> _y’
      In the expression: T $ \ x -> _y
    • Relevant bindings include
        x :: b (bound at <interactive>:7:23)
        g :: a -> Int (bound at <interactive>:7:13)
        f :: a -> b (bound at <interactive>:7:8)
        fmap :: (a -> b) -> T a -> T b (bound at <interactive>:7:3)

So now we're clear about the types of everything relevant, right? We need to return an Int somehow, and what we have to build it out of are:

        x :: b
        g :: a -> Int
        f :: a -> b

Well, okay, the only thing we have that can possibly create an Int is g, so let's fill that in, leaving g's argument blank to ask GHC for more help:

instance Functor T where
  fmap f (T g) = T $ \x -> g _y

<interactive>:7:31: error:
    • Found hole: _y :: a
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 fmap :: forall a b. (a -> b) -> T a -> T b
               at <interactive>:7:3
      Or perhaps ‘_y’ is mis-spelled, or not in scope
    • In the first argument of ‘g’, namely ‘(_y)’
      In the expression: g (_y)
      In the second argument of ‘($)’, namely ‘\ x -> g (_y)’
    • Relevant bindings include
        x :: b (bound at <interactive>:7:23)
        g :: a -> Int (bound at <interactive>:7:13)
        f :: a -> b (bound at <interactive>:7:8)
        fmap :: (a -> b) -> T a -> T b (bound at <interactive>:7:3)

Okay, we could have predicted this ourselves: to call g, we need a value of type a from somewhere. But we don't have any values of type a in scope, and we don't have any functions that return a value of type a either! We're stuck: it's impossible to produce a value of the type we want now, even though at every step we did the only possible thing: there's nothing we could back up and try differently.

Why did this happen? Because if I give you a function of type a -> Int and say "but by the way, here's a function from a -> b, please give me back a function from b -> Int instead", you can't actually use the function from a -> b, because nobody ever gives you any as to call it on! If I had given you a function from b -> a instead, that would be quite helpful, right? You could produce a function from b -> Int then, by first calling the b -> a function to get an a, and then calling the original a -> Int function to get out the desired Int.

And that's what a contravariant functor is about: we reverse the arrow in the function passed to fmap, so it can fmap over things you "need" (function arguments) instead of things you "have" (concrete values, return values of functions, etc).

---

Aside: I claimed earlier that we had done "the only possible thing" at each step, which was a bit of a fib. We can't build an Int out of f, g, and x, but of course we can make up all sorts of numbers out of the air. We don't know anything about the type b, so we can't get an Int that's derived from it in some way, but we could just say "let's always return zero", and this technically satisfies the type checker:

instance Functor T where
  fmap f (T g) = T $ const 0

Obviously this looks quite wrong, since it seems like f and g ought to be pretty important and we're ignoring them! But it type-checks, so we're okay, right?

No, this violates one of the Functor laws:

fmap id = id

We can prove this easily enough:

fmap id (T $ const 5) = (T $ const 0) /= (T $ const 5)

And now we really have tried everything: the only way we have to build an Int without using our b type at all is to make it up out of nothing, and all such uses will be isomorphic to using const, which will violate the Functor laws.

Answer 3

Here's another bit of perspective. As liminalisht showed, T is Contravariant. What can we tell about types that are both covariant and contravariant?

import Data.Void


change1, change1', change2 :: (Functor f, Contravariant f) => f a -> f b
change1 = contramap (const ()) . fmap (const ())
change1' = (() >$) . (() <$)
change2 = fmap absurd . contramap absurd

The first two implementations are basically the same (change1' being an optimization of change1); each of them uses the fact that () is a "terminal object" of Hask. change2 instead uses the fact that Void is an "initial object".

Each of these functions replaces all the as in f a with bs without knowing anything whatsoever about a, b, or the relationship between them, leaving everything else the same. It should probably be clear that this means f a doesn't really depend on a. That is, f's parameter must be phantom. That is not the case for T, so it can't also be covariant.