Why are all polymorphic functions between functors natural transformations?

Question

Bartosz Milewski's Category Theory for Programmers says the following:

A parametrically polymorphic function between two functors (including the edge case of the Const functor) is always a natural transformation.

Why is this true?

Something along the lines of an informal proof would help me. It would also help to have an intuition about this. Milewski says that naturality can be thought of as "separation of concerns" and provides an eggy metaphor:

One [functor] moves the eggs, the other boils them.

How could ad-hoc polymorphism mix the concern of moving the eggs with the concern of boiling the eggs?

As you can see, I'm pretty fuzzy on this topic.

Answer 1

I think the easiest thing is to refer you to the famous Theorems for free! paper, which explains the intuition behind the use of the Reynolds parametricity theorem.

Intuitively, in System $\mathrm F$ a function $\alpha$ of type $\forall X. F\ X \rightarrow G\ X$, is so polymorphic, that $X$ can be instantiated by a morphism $f$ rather than just types. When one makes this precise, one sees that an arrow $F\ f\rightarrow G\ f$ can only be a commuting square, which exactly expresses the fact that $\alpha$ is a natural transformation.

The proof itself can be derived from Reynolds' classic result from Types, Abstraction and Parametric Polymorphism, which builds a model of System $\mathrm F$ where every type is interpreted by a relation over programs.