Mengapa `map insertionsort` tidak sama dengan`map mergesort`?

Dalam teori jenis podcast ep. 3 , Dan Licata mengklaim bahwa fakta bahwa untuk setiap input, insertionsort dan mergesort memberikan hasil yang sama tidak menyiratkan bahwa hasilnya akan sama ketika digunakan sebagai fungsi urutan yang lebih tinggi sebagai argumen ke fungsi ketiga, yaitu map insertionsorttidak harus sama map mergesort.

Dia menjelaskan hal ini dengan "karena Anda tidak tahu bahwa, karena fungsinya, insertionsort dan mergesort adalah sama" tetapi saya masih belum mengerti.

Mengapa demikian? Contoh balasan akan sangat bagus!

Ini ada hubungannya dengan aksioma ekstensionalitas , yaitu apakah Anda menerimanya untuk fungsi atau tidak.

Pernyataan aksioma ini berkaitan dengan fungsi adalah Secara informal itu berarti bahwa jika dua fungsi sama-sama bijaksana, maka kami menganggapnya sama.

$$\forall f,g:A \to B,\ ((\forall x:A ,\ f\ x = g\ x) \Leftrightarrow f = g).$$

Jenis penggabungan dan penyisipan secara sintaksis tidak sama, tetapi jika kita tidak peduli dengan kompleksitas waktu dan ingatan mereka (maksud saya jika hanya peduli tentang hasilnya), kita dapat menerima aksioma ekstensionalitas dan menganggapnya sama. Itu berarti kita dapat mengganti satu sama lain dalam setiap ekspresi yang dipertimbangkan tanpa benar-benar mengubah apa pun. Dalam hal ini .$\text{map}\ f = \text{map}\ g$

Sebaliknya, jika kita menolak aksioma yang disebutkan di atas, maka kita hanya dapat membuktikan pernyataan seperti ini: Perhatikan bahwa kesimpulannya tidak sama dengan .

$$(\forall x:A,\ f\ x = g\ x) \implies \forall xs:\text{list}\ A,\ \text{map}\ f\ xs = \text{map}\ g\ xs.$$ $\text{map}\ f = \text{map}\ g$