If you build such a list by consing new elements to the front, then it's insertion sort. If you build the list from a balanced binary tree it's merge sort.

---

One important difference between this and quotient-inductive types is that there are examples of "types with equations" which cannot be expressed as a rewriting system, e.g., free groups.

It's a still a cool feature to have this built into the language.

> If you build the list from a balanced binary tree it's merge sort.

But in the example, the list is built by adding two lists. This means that in the example, it uses insertion sort which like bubble sort is O(n^2).

You're right and looking at the example again I was completely wrong (shouldn't post without coffee). You can implement merging by writing append (+) in the correct way. As written, the code will always insert a new element every time there is a cons (:).

One way of getting better performance "by default" is to construct lists with constructors for empty list, singletons and append and then adding equations to ensure that the resulting binary tree is balanced.

I.e., Mergesort?

Eliminates duplicates too