Another Example - Sorting a List of Integers

The problem is to define a function sort which take a list of numbers and returns a list of the same numbers but sorted in ascending order. For example sort [1,6,2,4,0,2,2,3] would give [0,1,2,2,2,3,4,6]. Again this problem is not fully specified. What about the empty list? It makes sense to define sort [ ] = [ ]. So now we are ready to tackle the problem. We can try:

sort: list num -> list num;
sort [ ] <= [ ] 
sort (x::m) <= ?

Again we must think recursively: The right hand side will probably have the expression sort (m). In other words the sorted tail of the list. The trick is to imagine that this expression sort (m) has correctly sorted the tail of list. So what do we have to do with the head x so that the whole list x::m is correctly sorted? We must insert it into the correct place in the sorted tail sort m. This gives us:

sort: list num -> list num;
sort [ ] <= [ ]; 
sort (x::m) <= insert(x,sort m);

So now we have reduced the sorting problem to a simpler inserting problem. How do we insert a number into the correct place in a already sorted list of numbers? Well form the expression insert(x,sort m) we can see the type of insert is num # list(num)-> list(num); So let's try:

insert: num # list num -> list num;
insert(y, []) <= [y]; 
insert(y, x::k) <= ?

If the list we are inserting into is empty then it's easy. We create a singleton list consisting of the number we are inserting. If the list we are inserting in is not empty then what do we do?

Don't forget that the list we are inserting into is sorted. So what we need to do is compare y with the head of the list x. If y <x then we must put y at the beginning of the result:

insert: num # list num -> list num;
insert(y, []) <= [y]; 
insert(y, x::k) <= if y <x
                   then y::(x::k)
                   else ?;

Well, if y is not less than x then we want to keep x as the head of the result. The tail of the result will be the achieved by inserting y into the tail k. To give:

insert: num # list num -> list num;
insert(y, []) <= [y]; 
insert(y, x::k) <= if y <x
                   then y::(x::k)
                   else x::insert(y,k);

So we now have our complete sorting program:

insert: num # list num -> list num;
insert(y, []) <= [y]; 
insert(y, x::k) <= if y <x
                   then y::(x::k)
                   else x::insert(y,k);

sort: list num -> list num;
sort [ ] <= [ ]; 
sort (x::m) <= insert(x,sort m);

Try it out!