From e5d6f95e77ed9a3777e069603e26b3f6ad84b4b7 Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 5 Feb 2018 17:58:51 -0400 Subject: [PATCH] started text for Lists --- src/Lists.lagda | 188 ++++++++++++++++++++++++++++++++++++------- src/Properties.lagda | 2 +- 2 files changed, 158 insertions(+), 32 deletions(-) diff --git a/src/Lists.lagda b/src/Lists.lagda index 37cd30b0..5f3eb229 100644 --- a/src/Lists.lagda +++ b/src/Lists.lagda @@ -7,8 +7,6 @@ permalink : /Lists This chapter gives examples of other data types in Agda, as well as introducing polymorphic types and functions. -[This is a test.] - ## Imports \begin{code} @@ -28,17 +26,61 @@ data List (A : Set) : Set where infixr 5 _∷_ \end{code} +Let's unpack this definition. The phrase + List (A : Set) : Set -Here +tells us that `List` is a function from a `Set` to a `Set`. +We write `A` consistently for the argument of `List` throughout +the declaration. The next two lines tell us that `[]` (pronounced *nil*) +is the empty list of type `A`, and that `_∷_` (pronounced *cons*, +short for *constructor*) takes a value of type `A` and a `List A` and +returns a `List A`. Operator `_∷_` has precedence level 5 and associates +to the right. +For example, +\begin{code} +ex₀ : List ℕ +ex₀ = 0 ∷ 1 ∷ 2 ∷ [] +\end{code} +denotes the list of the first three natural numbers. Since `_::_` +associates to the right, the term above parses as `0 ∷ (1 ∷ (2 ∷ []))`. +Here `0` is the first element of the list, called the *head*, +and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the +*tail*. Lists are a rather strange beast: a head and a tail, +nothing in between, and the tail is itself another list! + +The definition of lists could also be written as follows. +\begin{code} +data List′ : Set → Set where + []′ : ∀ {A : Set} → List′ A + _∷′_ : ∀ {A : Set} → A → List′ A → List′ A +\end{code} +This is essentially equivalent to the previous definition, +and lets us see that constructors `[]` and `_∷_` each act as +if they take an implicit argument, the type of the list. + +The previous form is preferred because it is more compact +and easier to read; using it also improves Agda's ability to +reason about when a function definition based on pattern matching +is well defined. An important difference is that in the previous +form we must write `List A` consistently everywhere, whereas in +the second form it would be permitted to replace an occurrence +of `List A` by `List ℕ`, say. + +Including the lines \begin{code} {-# BUILTIN LIST List #-} {-# BUILTIN NIL [] #-} {-# BUILTIN CONS _∷_ #-} \end{code} +tells Agda that the type `List` corresponds to the Haskell type +list, and the constructors `[]` and `_∷_` correspond to nil and +cons respectively, allowing a more efficient representation of lists. -List abbreviations. +## List syntax + +We can write lists more conveniently be introducing the following definitions. \begin{code} infix 5 [_ infixr 6 _,_ @@ -54,22 +96,132 @@ _] : ∀ {A : Set} → A → List A x ] = x ∷ [] \end{code} +These permit lists to be written in traditional notation. \begin{code} -ex₁ : [ 1 , 2 , 3 ] ≡ 1 ∷ 2 ∷ 3 ∷ [] +ex₁ : [ 0 , 1 , 2 ] ≡ 0 ∷ 1 ∷ 2 ∷ [] ex₁ = refl \end{code} +The precedences mean that `[ 0 , 1 , 2 ]` parses as +`[ (0 , (1 , (2 ])))`, which evaluates to `0 ∷ 1 ∷ 2 ∷ []`, +as desired. +Note our syntactic trick only applies to non-empty lists. +The empty list must be written `[]`. Writing `[ ]` fails +to parse. + + +## Sections + +Richard Bird introduced a convenient notation for partially applied binary +operators, called *sections*. If `_⊕_` is an arbitrary binary operator, we +write `(x ⊕)` for the function which applied to `y` returns `x ⊕ y`, and +we write `(⊕ y)` for the function which applied to `x` also returns `x ⊕ y`. + +For example, here are definitions of the sections for cons. +\begin{code} +_∷ : ∀ {A : Set} → A → List A → List A +(x ∷) xs = x ∷ xs + +∷_ : ∀ {A : Set} → List A → A → List A +(∷ xs) x = x ∷ xs +\end{code} +We will make use of the first of these in the next section. + + +## Append + +Our first function on lists is written `_++_` and pronounced +*append*. \begin{code} infixr 5 _++_ _++_ : ∀ {A : Set} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) +\end{code} +The type `A` is an implicit argument to append. +The empty list appended to a list `ys` is the same as `ys`. +A list with head `x` and tail `xs` appended to a list `ys` +yields a list with head `x` and with tail consisting of +`xs` appended to `ys`. +Here is an example, showing how to compute the result +of appending the list `[ 0 , 1 , 2 ]` to the list `[ 3 , 4 ]`. +\begin{code} +ex₂ : [ 0 , 1 , 2 ] ++ [ 3 , 4 ] ≡ [ 0 , 1 , 2 , 3 , 4 ] +ex₂ = + begin + [ 0 , 1 , 2 ] ++ [ 3 , 4 ] + ≡⟨⟩ + 0 ∷ 1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ [] + ≡⟨⟩ + 0 ∷ (1 ∷ 2 ∷ [] ++ 3 ∷ 4 ∷ []) + ≡⟨⟩ + 0 ∷ 1 ∷ (2 ∷ [] ++ 3 ∷ 4 ∷ []) + ≡⟨⟩ + 0 ∷ 1 ∷ 2 ∷ ([] ++ 3 ∷ 4 ∷ []) + ≡⟨⟩ + 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [] + ∎ +\end{code} + + +## Reasoning about append + +We can reason about lists in much the same way that we reason +about numbers. Here is the proof that append is associative. +\begin{code} +++-assoc : ∀ {A : Set} (xs ys zs : List A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs +++-assoc [] ys zs = + begin + [] ++ (ys ++ zs) + ≡⟨⟩ + ys ++ zs + ≡⟨⟩ + ([] ++ ys) ++ zs + ∎ +++-assoc (x ∷ xs) ys zs = + begin + (x ∷ xs) ++ (ys ++ zs) + ≡⟨⟩ + x ∷ (xs ++ (ys ++ zs)) + ≡⟨ cong (x ∷) (++-assoc xs ys zs) ⟩ + x ∷ ((xs ++ ys) ++ zs) + ≡⟨⟩ + ((x ∷ xs) ++ ys) ++ zs + ∎ +\end{code} +The proof is by induction. The base case instantiates the +first argument to `[]`, and follows by straightforward computation. +The inductive case instantiates the first argument to `x ∷ xs`, +and follows by straightforward computation combined with the +inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive +invocation of the proof, in this case `++-assoc xs ys zs`. +Applying the congruence `cong (x ∷)` promotes the inductive hypothesis + + xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs + +to the equivalence needed in the proof + + x ∷ (xs ++ (ys ++ zs)) ≡ x ∷ ((xs ++ ys) ++ zs) + +The section notation `(x ∷)` makes it convenient to invoke the congruence. + +## Length + +\begin{code} length : ∀ {A : Set} → List A → ℕ length [] = zero length (x ∷ xs) = suc (length xs) +\end{code} +## Reverse + +## Map + +## Fold + +\begin{code} map : ∀ {A B : Set} → (A → B) → List A → List B map f [] = [] map f (x ∷ xs) = f x ∷ map f xs @@ -78,9 +230,6 @@ foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B foldr c n [] = n foldr c n (x ∷ xs) = c x (foldr c n xs) -ex₂ : [ 1 , 2 , 3 ] ++ [ 4 , 5 ] ≡ [ 1 , 2 , 3 , 4 , 5 ] -ex₂ = refl - ex₃ : length ([ 1 , 2 , 3 ]) ≡ 3 ex₃ = refl @@ -95,29 +244,6 @@ ex₆ = refl \end{code} \begin{code} -_∷ : ∀ {A : Set} → A → List A → List A -x ∷ = λ xs → x ∷ xs - -assoc-++ : ∀ {A : Set} (xs ys zs : List A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs -assoc-++ [] ys zs = - begin - [] ++ (ys ++ zs) - ≡⟨⟩ - ys ++ zs - ≡⟨⟩ - ([] ++ ys) ++ zs - ∎ -assoc-++ (x ∷ xs) ys zs = - begin - (x ∷ xs) ++ (ys ++ zs) - ≡⟨⟩ - x ∷ (xs ++ (ys ++ zs)) - ≡⟨ cong (x ∷) (assoc-++ xs ys zs) ⟩ - x ∷ ((xs ++ ys) ++ zs) - ≡⟨⟩ - ((x ∷ xs) ++ ys) ++ zs - ∎ - length-++ : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys length-++ {A} [] ys = begin diff --git a/src/Properties.lagda b/src/Properties.lagda index 838b1980..3a218dae 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -257,7 +257,7 @@ becomes: The proof that a term is equal to itself is written `refl`. -The inductive case corresponds to instantiating `m` by `suc zero`, +The inductive case corresponds to instantiating `m` by `suc m`, so what we are required to prove is: (suc m + n) + p ≡ suc m + (n + p)