13 Lists

Some of the material on Lists could have been done earlier. It is done earlier in SF, and I chose to use it in the Demo chapter at the very beginning. But covering it later allows PLFA to use more abstraction and ask more interesting questions. It also serves as a point of consolidation before we shift focus in the second part of PLFA (this being the last chapter in the first part). After this, we change gears, and start studying the foundations of programming languages, using the Agda tools and concepts that we have learned and developed.

The only differences between the definition of the list datatype that I used in the Demo chapter and the one in this chapter are syntactic (the syntax here matches that of the Agda standard library). Where I used empty as the constructor for the empty list, here we use []. My add constructor had two arguments, an element and a list, but here the constructor is infix _∷_. Between the underscores is not two colons (::), but a single Unicode character, which in Emacs is created with \::.

This operator is called "cons", for constructor, a name that dates back to the first version of LISP in 1959, where this was the fundamental datatype (the only recursive one). It’s common to hear "cons" used as a verb as well. This terminology is used for list constructors in many functional programming languages.

13.1 List syntax

The pattern synonyms using square brackets and commas to define short lists are specific to PLFA and are not defined in the Agda standard library. They are only used here to make example lists easier to read.

13.2 Append

In the Demo chapter, we saw the definition of the append function (here infix _++_, the proofs of the theorems for left and right identity, and for associativity. For completeness, here are the proofs from the Demo chapter again, but using the new syntax, and using rewrite instead of the equational reasoning that PLFA uses.

++-assoc : ∀ {A : Set} (xs ys zs : List A)
  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs rewrite ++-assoc xs ys zs = refl

++-identityˡ : ∀ {A : Set} (xs : List A) → [] ++ xs ≡ xs
++-identityˡ xs = refl

++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
++-identityʳ [] = refl
++-identityʳ (x ∷ xs) rewrite ++-identityʳ xs = refl

13.3 Reasoning about length

Here is the proof that the length of an append is the sum of the lengths of the arguments, using rewrite instead of equational reasoning.

length-++ : ∀ {A : Set} (xs ys : List A)
  → length (xs ++ ys) ≡ length xs + length ys
length-++ [] ys = refl
length-++ (x ∷ xs) ys rewrite length-++ xs ys = refl

It is as simple to derive as the theorems above, but this is in part due to the careful design of the length function. Had we instead written something like length (x ∷ xs) = length xs + 1, we would have had more work to do. But using suc (length xs) lets Agda make progress in reducing the right-hand side of the equation to be proved, to the point where the rewrite and refl work.

13.4 Faster reverse

Here are the proofs justifying faster reverse via the shunt function. The word "shunt" refers to moving a train or a segment of train cars onto a siding. It’s amusing to think about what sort of train manoeuvres are abstracted by this function.

shunt : ∀ {A : Set} → List A → List A → List A
shunt [] ys = ys
shunt (x ∷ xs) ys = shunt xs (x ∷ ys)

shunt-reverse : ∀ {A : Set} (xs ys : List A)
  → shunt xs ys ≡ reverse xs ++ ys
shunt-reverse [] ys = refl
shunt-reverse (x ∷ xs) ys
  rewrite ++-assoc (reverse xs) [ x ] ys
        | shunt-reverse xs (x ∷ ys)
    = refl

reverse′ : ∀ {A : Set} → List A → List A
reverse′ xs = shunt xs []

reverses : ∀ {A : Set} (xs : List A)
  → reverse′ xs ≡ reverse xs
reverses xs rewrite shunt-reverse xs []
  = ++-identityʳ (reverse xs)

13.5 Map

The map, filter, foldl, and foldr functions are standard in most functional programming languages. If you have previous experience with functional programming, you will certainly have encountered them (perhaps under different names, or with slightly altered functionality). If this is your first experience, it’s worth spending a little time thinking about how these might be used, and perhaps doing the optional PLFA exercises.

13.6 Monoids

With such powerful features for abstraction, it is natural to define datatypes that make good use of them. This is done a lot in the Agda standard library. Some of these definitions are more specific to a computational context (such as Decidable) and some come from mathematics, either classic or modern. Monoids come from abstract algebra, where they are sometimes called semigroups with identity ("semi" because the inverse operation may not be possible). They can be useful in computer science.

I have changed the handling of monoids in the 747 files as compared to PLFA, to spare you some notational inconvenience (this idea is due to David Darais). The mechanism is called "instance arguments", which is a way of defining type classes, declaring datatypes to be instances of those classes, and then writing generic code over those classes with instance arguments that can be automatically instantiated when the code is applied to specific instances. You don’t have to understand how the mechanism works; you only have to use it. The Agda documentation on instance arguments uses Monoid as its first example.

Even with this modification, the notation is still a bit noisy, but if you squint, you can see that the proofs are using techniques we’ve seen before, such as rewriting using the inductive hypothesis and algebraic manipulation.

13.7 All

The constructor names for All overload the constructor names for lists. This can be initially confusing while reading code, but one quickly gets used to it. Confusion can be avoided during development thanks to the type system. We will put this technique to good use in the next part of PLFA.

13.8 Any

The proof that an element is in a list cannot be derived automatically by refining, because it is never clear which constructor should be used. But the proof that an element is not in a list can be derived by splitting on the impossibility. Changes in Agda that let some absurd patterns be absent from the code are reflected in the brevity of the negative proofs in our files, as compared to those in PLFA, written with an earlier version of the software.

13.9 All and append

Here is the proof that All distributes over append, using co-patterns.

All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
  All P (xs ++ ys) ⇔ (All P xs × All P ys)
to (All-++-⇔ [] ys) apxs++ys = ⟨ [] , apxs++ys ⟩
to (All-++-⇔ (x ∷ xs) ys) (px ∷ apxs++ys)
 with _⇔_.to (All-++-⇔ xs ys) apxs++ys
... | ⟨ apxs , apys ⟩ = ⟨ (px ∷ apxs) , apys ⟩
from (All-++-⇔ [] ys) ⟨ apxs , apys ⟩ = apys
from (All-++-⇔ (x ∷ xs) ys) ⟨ px ∷ apxs , apys ⟩
  = px ∷ _⇔_.from (All-++-⇔ xs ys) ⟨ apxs , apys ⟩

I have left the All and Any exercises as optional, as I think by this point the ideas should be pretty clear and the solutions not difficult. The exercises All-∀ and Any-∃ are a bit more complicated, as they require a version of extensionality that works with dependent functions, such as the one given in PLFA Isomorphism.