Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the functoriality conditions.
Is there a "free theorem" result for functoriality? i.e. is it sometimes possible to see from the type of a "functor" that it is indeed a functor?
There are two senses in which type formation operations are 'functorial,' but neither matches functoriality on the category of types.
First, you can interpret the collection of types as a groupoid, and consider isomorphisms between types to be 'arrows.' These compose, but also always have inverses, so are in some sense undirected. However, this is also why all constructions are able to be functorial, because type formation operations have both covariant and contravariant positions, and thus may not preserve the direction of arrows.
Anyhow, functoriality here says that if you have $P : A \cong B$ then there is always $F P : F A \cong F B$, and: $$F\ \mathsf{Refl}_A = \mathsf{Refl}_{F A} \\ F (P \cdot Q) = F P \cdot F Q$$ This is essentially the direction of homotopy type theory, where these properties are internalized (and the 'dimension' is not limited to just groupoids).
The second functoriality property is already in the other answer. The "identity extension lemma" is a functoriality property where categories are relaxed to reflextive graphs (rather than tightened to groupoids). Again, type formation operations are able to be functorial because reflexive graphs do not have operations where 'direction' matters. However, this time it is because edges are not assumed to be composible.
So, the identity extension lemma says that every relation $R : A \Leftrightarrow B$ induces a relation $FR : FA \Leftrightarrow FB$ where:
$$F\ \mathsf{Refl}_A = \mathsf{Refl}_{F A}$$
And that's all there is to being a "relator" of reflexive graphs. There are also type systems that can talk about this sort of thing internally, possibly even with homotopy type theory features, like here.
Now, The first approach doesn't give you 'normal' functoriality for all type formations because not every map $f : A → B$ is an isomorphism. And of course, if we do $F A = A → A$, that's not going to extend to $(A → A) → (B → B)$ nor the other direction, without also having some map in the other direction. However, given an isomorphism, it induces $(A → A) \cong (B → B)$
In the second approach, a map $f : A → B$ induces a relation $\mathsf{gr} f : A \Leftrightarrow B$ given by $(x, f\ x)$. However, although we could compose the maps, there is no notion of composition of relations to talk about, and relate back to the composed functions. Considering the same type construction:
$$FR(m,n)\quad \Longleftrightarrow \quad R(x,y) ⇒ R(m\ x, n\ y)$$
So:
$$F(\mathsf{gr}\ f)(m,n)\quad \Longleftrightarrow\quad f \circ m = n \circ f$$
If you try to apply this to composed maps, then you know:
$$f \circ m = n \circ f \\ g \circ m = n \circ g$$
so $$f \circ g \circ m = f \circ n \circ g$$
but then there's nothing to do further.
You can read more about this angle in this paper, which tries to apply parametricity to a wider mathematical scope. A counter-question that the paper kind of motivates is: why do you care specifically about category functoriality? The original intuitive specification of "naturality" sounds very much like the intuitive specification of "parametricity," but the former was eventually formalized in terms of directed maps, rather than undirected relations. However, there is nothing inherently more legitimate about directed maps vs. relations or isomorphisms, and some things work out more appropriately for the latter than the former. Sometimes even in category theory it it necessary to shift into the 'undirected' perspective to make easier sense of something. See for instance here.
On a final note, you can have a type theory that keeps track of category theoretic functoriality of things. Here is early work, and here is something closer to homotopy type theory. The former tracks functoriality of everything explicitly, and is of course significantly more complicated for it. The latter allows functoriality to be an internally definable property, similar to the 'dimension' in homotopy type theory. But in neither would every type expression be necessarily functorial with respect to directed maps, because that would require limiting what one is able to write.
In a specific lambda-calculus, e.g., in System F, you can just write the type and see whether it is covariant in its free type parameters. Each function arrow creates a contravariant position to the left of it and a covariant position to the right of it. So, for example, F a b = (a -> a -> b) -> a is covariant in a and contravariant in b.
The morphism parts of the functor follow automatically from the type.
There is a parametricity result that a covariant type constructor has a unique fmap method that satisfies the parametricity law. It will then follow that the fmap method also satisfies the functor laws.
