Rearranging function in 'Theorems for free'

Question

I'm reading Wadler's 'Theorems for free'. In section 3.5 he states that $m_{AA}(I_A)$ is a rearranging (i. e. injective) function. $I_A$ is the identity function on the type A. $$m : \forall X.\forall Y. (X \rightarrow Y) \rightarrow (X^* \rightarrow Y^*)$$ How does he use section 3.4 to prove this without any $\forall^{(=)}X$-types? Why can't $m_{AA}(I_A)$ e. g. drop a few elements in the list?

Answer 1

It can, as good evidence for it define m as something like

m f = map f . drop 2

And everything still typechecks. Here "rearranging" is supposed to refer to structural operation on the list without regards to the specific values of each element. This is captured by the free theorem at this type,

m (\x -> x) . map f = map f . m (\x -> x)

m (\x -> x) performs all the structural changes to the list and map f actually alters this element. This theorem implies that they are independent of each other.