Functor composition rule necessary?

Question

Sorry if this is a dumb question, but I don't quite understand the composition rule for functors.
I see how the identity rule makes sense, as mapping the functor over the id function shouldn't change anything. But isn't this rule sufficient?
Is there an example of an fmap implementation that obeys the identity rule, but not the composition rule?

Answer 1

Suppose we are working in a parametric model (which is the case in bottom-free Haskell). Suppose that F is a functor, and that f is any function with this type:

f :: (a -> b) -> (F a -> F b)

If f id = id, then f = fmap. This is a consequence of the parametricity theorem.

This is a very interesting result, because it means that when Functor instances exist, they are in a sense unique.

However, we assumed that F is a functor, which means it has a fmap function which obeys the functor laws. This means that if you're looking for a counterexample, you can't start with a functor and then look for a fmap-like function. You must start with a non-functor.

What's especially interesting is that nobody knows of any counterexamples. At the time of writing, it hasn't been proven that any bottom-free seq-free Haskell function of the correct type which satisfies the identity law also satisfies the composition law.

Answer 2

Assuming parametricity (for example in a language like Haskell), the composition law follows from the identity law. (see comments)

For the general mathematical concept of functor, both laws are required. It's easy to come up with an example of something that is almost a functor but doesn't satisfy the composition law: let $\mathcal{C}$ be the following category (identities and composites not drawn):

$$a \overset{f}{\longrightarrow} b \overset{g}{\longrightarrow} c$$

and consider a "functor" $F : \mathcal{C} \to \mathbf{Set}$ that sends $a$, $b$ and $c$ to some set $X$, $f$ and $g$ to $\mathrm{id}_X$, and $g \circ f$ to a non-identity morphism $X \to X$.

Answer 3

It actually is possible to prove the functor composition rule from parametricity and identity. However, it requires more machinery than is usually talked about (i.e. more than 'free theorems'). Here is a formalization of the argument in cubical Agda. I'll explain how it works below. If you want a more thorough presentation of the parametricity principles involved, I was looking at this paper when formulating them.

First, parametricity is based on a relational interpretation of type theory. There is a structure on the collection of types called a "reflexive graph." Given two types $A$ and $B$, there is a collection of relations between them $A \Leftrightarrow B$. For every type $A$ there is a designated 'reflexive' relation $A \Leftrightarrow A$, and for types this is just the identity relation. In my formalization I technically take relations $A \Leftrightarrow B$ to be arbitrary families $A → B → \mathsf{Type}$, so they are not strictly relations (not propositional). This seems to fit in well with the homotopy aspects, though, because the identity type (the reflexive 'relation') may not be a proper "relation" there either, but it behaves similarly.

A sort of relation we'll need later is the graph of a function. If $f : A → B$, then $\newcommand{\G}{\mathsf{G}} \G_f : B \Leftrightarrow A$ is the relation $\G_f(y,x) := y = f(x)$.

A structure preserving map between reflexive graphs is called a "relator." For the special case of the reflexive graph of types, a relator is:

1. A mapping $F : \sf Type → Type$
2. An action of $F$ on relations, so if $R : A \Leftrightarrow B$, then $F(R) : F(A) \Leftrightarrow F(B)$
3. Such that the identity extension property is satisfied: $\newcommand{\Id}{\mathsf{Id}} F(\Id_A) = \Id_{F(A)}$

If we consider reflexive graphs to be analogous to categories, then relators are analogous to functors. But because there is no composition of edges in a reflexive graph, relators only have an identity preservation property.

The usual ways of forming types in type theory are relators. So, for instance, there is a relator for function types. Given two relations $R$ and $S$, there is a relation $R → S$ that relates functions given by:

$$(R → S)(f,g) = ∀ x\ y. R(x,y) → S(f(x), g(y))$$

$\Id_A → \Id_B$ is $\Id_{A → B}$. That's the only other relator that will come up for functors, but products, coproducts, etc. are relators as well. In something like System F, quantifications of relators also are relators.

Finally, a parametric transformation between relators $F$ and $G$ is a family of maps $t_A : F(A) → G(A)$ that satisfies the condition: $$∀(R : A \Leftrightarrow B). (F(R) → G(R))(t_A, t_B)$$

That is, $t_A$ and $t_B$ are related by $F(R) → G(R)$. Parametric transformations are the relational analogue of natural transformations, and also where the parametricity theorems for polymorphic functions come from. I.E. the parametricity statements for polymorphic functions correspond to them being parametric transformations between relevant relators.

---

So, with the above definitions, we can state how certain things are 'automatically' functors. Suppose we have the following:

1. A relator $F$ on types
2. A polymorphic function $m : ∀A\ B. (A → B) → F(A) → F(B)$
3. Given relations $R : A \Leftrightarrow A'$ and $S : B \Leftrightarrow B'$, $(R → S) → F(R) → F(S)$ relates $m_{A,B}$ to $m_{A',B'}$
4. For all $A$, $\newcommand{\id}{\mathsf{id}} m_{A,A}(\id_A) = \id_A$

Then for all appropriate $f$ and $g$, $m (g \circ f) = m(g) \circ m(f)$. The proof goes through several steps.

• For all $x : F(A)$, $F(\Id_A)(x,x)$ holds. This follows from the identity extension property for $F$, and reflexivity of equality.
• For all $f : A → B$ and $x : F(A)$, the relation $F(\G_f) : F(B) \Leftrightarrow F(A)$ relates $m(f)(x)$ and $m(\id_A)(x)$. This follows from parametricity of $m$, because $\Id → \G_f$ relates $f$ to $\id$, and the above reflexive lemma.
• But, because we've assumed that $m(\id) = \id$, it's also the case that $F(\G_f)$ relates $m(f)(x)$ to $x$
• Next, given $f : A → B$, $g : B → C$ and $x : F(A)$, $F(\Id_C)$ relates $m(g)(m(f)(x))$ to $m(g \circ f)(x)$. This again follows from parametricity, using that $\G_f → \Id_C$ relates $g$ to $g \circ f$, and the above step
• But, again by identity extension for $F$, $F(\Id_C) = Id_{F(C)}$, so $m(g)(m(f)(x)) = m(g \circ f)(x)$, and by extensionality of functions $m(g) \circ m(f) = m(g \circ f)$.

---

So, what does this mean? It means that if you have a relator $F$, then any polymorphic function $m$ that satisfies the identity rule for functors is sufficient to turn $F$ into a functor (on types at least; I haven't bothered to see how much it generalizes, although it might). In some sense, this probably isn't particularly surprising. A relator is the parametricity analogue of a functor, and the category structure of types embeds into the relational parametricity structure (by taking functions to their graphs). So it should already be close to being a functor. Perhaps it's a little surprising, because reflexive graphs have no notion of composition, so relators are not specified to preserve composition of relations.

It also means that there are no counterexamples for parametric structures. If you have an $F$ with an appropriate $m$ that does not give rise to a functor, then $F$ must not satisfy the parametric identity extension property (or act on relations at all, I suppose). Certainly you can have a type theory in which not every type former/polymorphic function is parametric. But most 'simple' ways of forming types are not examples.

Also, I imagine that the argument that starts from assuming that $F$ is a functor means that it's possible to prove that $m$ is essentially unique among operations for turning $F$ into a functor. Once you have any $m$, $F$ is a functor, so any other $m'$ must be equal to $m$.