Recently I have been reading the Category for programmers book from Bartosz Milewski, and one thing that amazes me is the realization that the implementation of well known functors such as Maybe or List could in fact be mechanically derived from some primitive functors.

However, I was struggling to understand the demonstration of this result (see the “Functorial Algebraic data Types” section here, or section 8.3 in the pdf). So I decided to try to convince myself with code.

TL; DR

If you want to get the result directly, here it is: you can automatically derive Functor instances from algebraic data types (ie sum and / or products of types), much like you would derive Eq or Show instances. To that end, you can use the DerivFunctor extension.

For instance, you could redefine the Maybe type and automagically derive its Functor instance this way.

{-# LANGUAGE DeriveFunctor #-}

-- first hide the Maybe from the standard Prelude
import Prelude hiding (Maybe(..))

data Maybe a = Nothing | Just a
  deriving Functor

Functoriality of algebraic data types, examples

The underlying property which permits this mechanical derivation can be stated this way: a parameterized algebraic data type (ADT) T is functorial in any of its type parameters.

For example, according to this result, the ADT Maybe a is functorial in a. The following ADT:

newtype Pair a b =
  Pair (a, b)

is functorial in a and b. Indeed, the following Functor instance accounts for the functoriality in b:

instance Functor (Pair a) where
  fmap f (Pair (a, b)) = Pair (a, f b)

Haskell doesn’t allow us to declare a Functor of Pair in a, but we can get its equivalent by declaring another type:

newtype ReversedPair b a =
  ReversedPair (a, b)

instance Functor (ReversedPair b) where
  fmap f (ReversedPair (a, b)) = ReversedPair (f a, b)

ReversedPair is the same as Pair, but with parameterized types reversed. This accounts for the functoriality of Pair in a.

Functoriality of algebraic data types: refinement

The result stated in the previous section can actually be refined. Indeed, not only do we know that a parameterized ADT is functorial in any of its parameterized types, but we also know how to build the corresponding functors.

Namely, those functors can mechanically be derived from the following things:

• the Functor instance for Const ()
• the Functor instance for Identity
• The Bifunctor instance for Either
• The Bifunctor instance for (,)

How do we prove that ? The proof can be decomposed like this:

• (Fact 1): we know from, as Bartosz Milewski is saying in the paragraph we are looking at, that any algebraic data type is isomorphic to a combination of sum and products of Const () and Identity. So Const () and Indentity can be seen as basic building blocks for ADT. Moreover, we know that sum and product can be be represented as Eithers and tuples respectively (ie via the (,) operator).
• (Fact 2): a finite sum and / or product of basic ADTs is functorial. This result can be obtained by induction, the base case being Const () and Identity, and the induction case being the sum or product of a functorial ADT with Const () or Identity.
• (Fact 3): We can deduce from Fact 1 and fact 2 that any ADT is functorial, with the added bonus that we know how to mechanically build the corresponding functors.

Fact 1 being known, let’s try to get an intuition of why Fact 2 Fact 3 are true.

“Proof” with code (Part 1)

Recall that Fact 2 is obtained by induction. The base case is trivial, since both basic ADTs are notoriously functorial.

Let’s move on to the induction case. It can be stated as follows: let T be a functorial ADT; then T+Const(), T*Const (), T+Identity and T*Identity are functorial.

To simplify things, let’s try to convince ourselves of this induction with a sum or product of two basic ADTs (ie Const () or Identity).

Such an ADT can be represented by the following type:

newtype BiComp bf fu gu a b =
  BiComp (bf (fu a) (gu b))

Where bf represents the sum or the product of two basics ADTS fu and gu; a and b are the parameters of the ADT.

So proving Fact 2 amounts to prove that BiComp is functorial in a and b. Let’s review our assumptions:

• fu is Const () or Identity. In particular, it is functorial.
• gu is Const () or Identity. In particular, it is functorial.
• bf is Either (sum) or (,) (product). In particular, it is bifunctorial.

Using these assumptions, we can deduce that BiComp is bifunctorial; indeed, we can declare its Bifunctor instance like this:

instance (Bifunctor bf, Functor fu, Functor gu) =>
         Bifunctor (BiComp bf fu gu) where
  bimap f g (BiComp x) = BiComp (bimap (fmap f) (fmap g) x)

To paraphrase Bartosz Milewski, bimap breaks through the outer bf layer, while the two fmaps dig under fu and gu respectively. So Bicomp bf fu gu is bifunctorial, in particular it is functorial in a and b. This gives us an intuition of Fact 2.

“Proof” with code (Part 2)

Let’s now consider Fact 3. Again, to simplify let us consider an ADT with two type parameters, such as Pair a b from above. The goal here is to prove that Pair a b is functorial in a and b.

We know from Fact 1 that such an ADT is isomorphic to a sum or product of Const () or Identity. More precisely, Pair a b is isomorphic to the following type:

type Pair' a b = BiComp (,) Identity Identity a b

Indeed, this ismorhism can be expressed through the following two functions:

isoPair' :: Pair a b -> Pair' a b
isoPair' (Pair (a, b)) = BiComp (Identity a, Identity b)

isoPair :: Pair' a b -> Pair a b
isoPair (BiComp (Identity a, Identity b)) = Pair (a, b)

From this, we can recover the functoriality of Pair in b like this:

instance Functor (Pair a) where
  fmap f = isoPair . second f . isoPair'

Where second comes from the Bifunctor typeclass. The functoriality in a could be obtained by declaring a new type inverting a and b, much like in the previous section. So we finally got our result: Pair is functorial in a and b, and we have an explicit way of building the underlying functors from the basic functors Const () and Indentity.

We can easily convince ourselves that this result holds any other sum / product of basic types. For example, let’s consider the Maybe type:

data Maybe a
  = Nothing
  | Just a

In this case it’s even easier since we have only one type parameter. We can build an isomorphic type out of the sum (Either) of Const () and Identity:

type Maybe' a = BiComp Either (Const ()) Identity () a

The corresponding isomorphisms from Maybe to Maybe':

isoMaybe' :: Maybe a -> Maybe' a
isoMaybe' Nothing = BiComp (Left $ Const ())
isoMaybe' (Just x) = BiComp (Right (Identity x))

isoMaybe :: Maybe' a -> Maybe a
isoMaybe (BiComp (Left _)) = Nothing
isoMaybe (BiComp (Right (Identity x))) = Just x

And the following Functor instance:

instance Functor Maybe where
  fmap f = isoMaybe . second f . isoMaybe'

Conclusion

This post turned out to be much longer than expected, and frankly speaking, quite annoying to write. But it definitely deepened my understanding of functor derivation in Haskell, and I hope it’s the same for you! You can find a gist containing the code here.