Why is `map insertionsort` not to equal to`map mergesort`?

Question

In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as higher order functions as arguments to a third function, i.e. map insertionsort does not have to equal map mergesort.

He explains this by "because you don't know that, as functions, insertionsort and mergesort are equal" but I still don't get it.

Why is this the case? A counter example would be great!

Answer 1

It has to do with the axiom of extensionality, i.e. whether you accept it for functions or not.

The statement of this axiom with regard to functions is $$\forall f,g:A \to B,\ ((\forall x:A ,\ f\ x = g\ x) \Leftrightarrow f = g).$$ Informally it means that if two functions are equal point-wise, then we consider them equal.

Syntactically merge-sort and insertion-sort are not equal, but if we don't care about their time and memory complexities (I mean if care only about their results) we can accept the axiom of extensionality and consider them equal. That means we can substitute one for another in every expression under consideration without actually changing anything. In this case $\text{map}\ f = \text{map}\ g$.

On the contrary, if we reject the aforementioned axiom, then we can only prove a statement like this: $$(\forall x:A,\ f\ x = g\ x) \implies \forall xs:\text{list}\ A,\ \text{map}\ f\ xs = \text{map}\ g\ xs.$$ Notice that the conclusion is not the same as $\text{map}\ f = \text{map}\ g$.

• Drathier: I want to upvote this again.