This post is the first of three that give an example of how to use DTP in Agda to enforce correctness using sorted lists. This post will focus on designing a data structure to capture the idea of "sortedness" that is also easy for other programmers to use, i.e. helps them avoid writing out proofs in simple cases. To follow along, you will need a version of Agda >= 2.4.2, as the technique we will use requires recursive instance search (discussed below).
So enough of the preamble - let's dig in! To keep things simple, let's decide to make our lists contain only numbers. We can always go back and parameterize our list over any element type with an ordering relation, but I think that might be too much overhead to start with for an introductory example.
With that out of the way, a simple representation of a list of sorted numbers would be a list in which, when you add an element to it, you also provide a proof that the element is "in order" relative to the rest of the list. We keep our list sorted in increasing order, which means that we will have a "snoc" list (cons to the right) whose last element is the upper bound of the list. When we snoc a new element, we also show that this new element is larger or equal to this list's upper bound to produce a new list with a new upper bound. The code for this is shown below.
We have a list of numbers, indexed by its upper bound. The upper bound of the empty list is 0; given xs a sorted list bounded by m and n a number, we can create a new sorted list bounded by n if m ≤ n.
So far so good, but we run into a problem fast when we try to create a SortList.
Ugh! Who wants to write code that looks like that? It's hard to see that this is a simple list of 1 2 3 with all those proof terms lying about. Here I used Agsy (C-c C-a) to fill in the proof terms for me, so it didn't require much writing, but it is still painful to read or use.
The fact that Agda could easily find these proof terms should lead you to think we can get Agda to do this automatically, invisible to the user. And you're right! Let's have our proof as an instance argument; this will have Agda search for constructors that match our proof obligation, as well as any functions declared in an instance block.
If we attempt to write out a very simple SortList, one containing only the element 3, we have no problems. That's because the constructor z≤n : ∀ {n} → 0 ≤ n can be found lying around in scope, and it will match the goal 0 ≤ 3.
However, we run into a problem when we try to use the same list as before.
Remember what I said before? Instance search looks for constructors that are lying around and (possibly recursive) functions declared in instance blocks. We know that z≤n doesn't apply here, because 1 != 0. But what about the other constructor, s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n ? Unfortunately, it is not an instance recursive constructor. What we'd like to see is this:
- Agda needs to find a term that will match 1 ≤ 2
- Agda looks at the two constructors for _≤_ and sees that s≤s will apply
- Agda applies s≤s, and searches for a suitable (m≤n : m ≤ n) (found in the constructor argument) that will satisfy the goal.
- Agda concludes that m≤n must have type 0 ≤ 1.
- Agda searches the constructors and sees that z≤n will apply, finishing the proof.
And because we can, let's finish up by prettying up our constructors, which we can now do because our proof obligation is invisible.
Doesn't that just give you the warm fuzzies? :)
