2
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.