diff --git a/_config.yml b/_config.yml index 3825eaa3..6fc43245 100644 --- a/_config.yml +++ b/_config.yml @@ -1,4 +1,4 @@ -title: Software Foundations in Agda +title: Programming Language Theory in Agda # the author field should not be used in the template author: Wen Kokke @@ -14,7 +14,7 @@ contributors: twitter_username: philipwadler description: > - Software Foundations in Agda. + Programming Language Theory in Agda. # include disqus to allow comments e.d. disqus: diff --git a/src/Connectives.lagda b/src/Connectives.lagda index 0add5be7..f2d8be39 100644 --- a/src/Connectives.lagda +++ b/src/Connectives.lagda @@ -44,25 +44,31 @@ if both `A` holds and `B` holds. We formalise this idea by declaring a suitable inductive type. \begin{code} data _×_ : Set → Set → Set where - _,_ : ∀ {A B : Set} → A → B → A × B + ⟨_,_⟩ : ∀ {A B : Set} → A → B → A × B \end{code} Evidence that `A × B` holds is of the form -`(M , N)`, where `M` is evidence that `A` holds and -`N` is evidence that `B` holds. By convention, we -parenthesise pairs, even though `M , N` is also +`⟨ M , N ⟩`, where `M` provides evidence that `A` holds and +`N` provides evidence that `B` holds. In the standard library, +the pair constructor is `_,_`, but here we rename it to +`⟨_,_⟩` so that comma is available for other notations +(in particular, lists and environments). + + Given evidence that `A × B` holds, we can conclude that either `A` holds or `B` holds. \begin{code} proj₁ : ∀ {A B : Set} → A × B → A -proj₁ (x , y) = x +proj₁ ⟨ x , y ⟩ = x proj₂ : ∀ {A B : Set} → A × B → B -proj₂ (x , y) = y +proj₂ ⟨ x , y ⟩ = y \end{code} -If `L` is evidence that `A × B` holds, then `fst L` is evidence -that `A` holds, and `proj₂ L` is evidence that `B` holds. +If `L` provides evidence that `A × B` holds, then `proj₁ L` provides evidence +that `A` holds, and `proj₂ L` provides evidence that `B` holds. Equivalently, we could also declare conjunction as a record type. \begin{code} @@ -81,39 +87,41 @@ Here record construction corresponds to the term - ( M , N ) + ⟨ M , N ⟩ where `M` is a term of type `A` and `N` is a term of type `B`. -When `(_,_)` appears on the right-hand side of an equation we -refer to it as a *constructor*, and when it appears on the -left-hand side we refer to it as a *destructor*. We also refer -to `proj₁` and `proj₂` as destructors, since they play a similar role. -Other terminology refers to constructor as *introducing* a conjunction, -and to a destructor as *eliminating* a conjunction. -Indeed, `proj₁` and `proj₂` are sometimes given the names -`×-elim₁` and `×-elim₂`. +When `⟨_,_⟩` appears in a term on the right-hand side of an equation +we refer to it as a *constructor*, and when it appears in a pattern on +the left-hand side of an equation we refer to it as a *destructor*. +We also refer to `proj₁` and `proj₂` as destructors, since they play a +similar role. Other terminology refers to a constructor as +*introducing* a conjunction, and to a destructor as *eliminating* a +conjunction. Indeed, `proj₁` and `proj₂` are sometimes given the +names `×-elim₁` and `×-elim₂`. Applying each destructor and reassembling the results with the constructor is the identity over products. \begin{code} -η-× : ∀ {A B : Set} (w : A × B) → (proj₁ w , proj₂ w) ≡ w -η-× (x , y) = refl +η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w +η-× ⟨ x , y ⟩ = refl \end{code} The pattern matching on the left-hand side is essential, since -replacing `w` by `(x , y)` allows both sides of the equation to +replacing `w` by `⟨ x , y ⟩` allows both sides of the equation to simplify to the same term. We set the precedence of conjunction so that it binds less -tightly than anything save disjunction, and of the pairing -operator so that it binds less tightly than any arithmetic -operator. +tightly than anything save disjunction. \begin{code} infixr 2 _×_ -infixr 4 _,_ \end{code} -Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and +Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`. + + Given two types `A` and `B`, we refer to `A x B` as the *product* of `A` and `B`. In set theory, it is also sometimes @@ -136,19 +144,19 @@ data Tri : Set where \end{code} Then the type `Bool × Tri` has six members: - (true , aa) (true , bb) (true , cc) - (false , aa) (false , bb) (false , cc) + ⟨ true , aa ⟩ ⟨ true , bb ⟩ ⟨ true , cc ⟩ + ⟨ false , aa ⟩ ⟨ false , bb ⟩ ⟨ false , cc ⟩ For example, the following function enumerates all possible arguments of type `Bool × Tri`: \begin{code} ×-count : Bool × Tri → ℕ -×-count (true , aa) = 1 -×-count (true , bb) = 2 -×-count (true , cc) = 3 -×-count (false , aa) = 4 -×-count (false , bb) = 5 -×-count (false , cc) = 6 +×-count ⟨ true , aa ⟩ = 1 +×-count ⟨ true , bb ⟩ = 2 +×-count ⟨ true , cc ⟩ = 3 +×-count ⟨ false , aa ⟩ = 4 +×-count ⟨ false , bb ⟩ = 5 +×-count ⟨ false , cc ⟩ = 6 \end{code} Product on types also shares a property with product on numbers in @@ -162,13 +170,13 @@ Instantiating the patterns correctly in `from∘to` and `to∘from` is essential Replacing the definition of `from∘to` by `λ w → refl` will not work; and similarly for `to∘from`, which does the same (up to renaming). \begin{code} -×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A) +×-comm : ∀ {A B : Set} → A × B ≃ B × A ×-comm = record - { to = λ{ (x , y) → (y , x)} - ; from = λ{ (y , x) → (x , y)} - ; from∘to = λ{ (x , y) → refl } - ; to∘from = λ{ (y , x) → refl } + { to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ } + ; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ } + ; from∘to = λ{ ⟨ x , y ⟩ → refl } + ; to∘from = λ{ ⟨ y , x ⟩ → refl } } \end{code} @@ -191,13 +199,13 @@ taking `((x , y) , z)` to `(x , (y , z))`, and the `from` function does the inverse. Again, the evidence of left and right inverse requires matching against a suitable pattern to enable simplification. \begin{code} -×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C)) +×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C) ×-assoc = record - { to = λ{ ((x , y) , z) → (x , (y , z)) } - ; from = λ{ (x , (y , z)) → ((x , y) , z) } - ; from∘to = λ{ ((x , y) , z) → refl } - ; to∘from = λ{ (x , (y , z)) → refl } + { to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ } + ; from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ } + ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl } + ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl } } \end{code} @@ -250,12 +258,12 @@ identity, the `to` function takes `(tt , x)` to `x`, and the `from` function does the inverse. The evidence of left inverse requires matching against a suitable pattern to enable simplification. \begin{code} -⊤-identityˡ : ∀ {A : Set} → (⊤ × A) ≃ A +⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A ⊤-identityˡ = record - { to = λ{ (tt , x) → x } - ; from = λ{ x → (tt , x) } - ; from∘to = λ{ (tt , x) → refl } + { to = λ{ ⟨ tt , x ⟩ → x } + ; from = λ{ x → ⟨ tt , x ⟩ } + ; from∘to = λ{ ⟨ tt , x ⟩ → refl } ; to∘from = λ{ x → refl } } \end{code} @@ -300,8 +308,8 @@ data _⊎_ : Set → Set → Set where inj₂ : ∀ {A B : Set} → B → A ⊎ B \end{code} Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M` -is evidence that `A` holds, or `inj₂ N`, where `N` is evidence that -`B` holds. +provides evidence that `A` holds, or `inj₂ N`, where `N` provides +evidence that `B` holds. Given evidence that `A → C` and `B → C` both hold, then given evidence that `A ⊎ B` holds we can conclude that `C` holds. @@ -356,19 +364,19 @@ a type `Tri` with three members, as defined earlier. Then the type `Bool ⊎ Tri` has five members: - (inj₁ true) (inj₂ aa) - (inj₁ false) (inj₂ bb) - (inj₂ cc) + inj₁ true inj₂ aa + inj₁ false inj₂ bb + inj₂ cc For example, the following function enumerates all possible arguments of type `Bool ⊎ Tri`: \begin{code} ⊎-count : Bool ⊎ Tri → ℕ -⊎-count (inj₁ true) = 1 -⊎-count (inj₁ false) = 2 -⊎-count (inj₂ aa) = 3 -⊎-count (inj₂ bb) = 4 -⊎-count (inj₂ cc) = 5 +⊎-count (inj₁ true) = 1 +⊎-count (inj₁ false) = 2 +⊎-count (inj₂ aa) = 3 +⊎-count (inj₂ bb) = 4 +⊎-count (inj₂ cc) = 5 \end{code} Sum on types also shares a property with sum on numbers in that it is @@ -382,18 +390,18 @@ does the same (up to renaming). \begin{code} ⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A) ⊎-comm = record - { to = λ{ (inj₁ x) → (inj₂ x) - ; (inj₂ y) → (inj₁ y) - } - ; from = λ{ (inj₁ y) → (inj₂ y) - ; (inj₂ x) → (inj₁ x) - } - ; from∘to = λ{ (inj₁ x) → refl - ; (inj₂ y) → refl - } - ; to∘from = λ{ (inj₁ y) → refl - ; (inj₂ x) → refl - } + { to = λ{ (inj₁ x) → (inj₂ x) + ; (inj₂ y) → (inj₁ y) + } + ; from = λ{ (inj₁ y) → (inj₂ y) + ; (inj₂ x) → (inj₁ x) + } + ; from∘to = λ{ (inj₁ x) → refl + ; (inj₂ y) → refl + } + ; to∘from = λ{ (inj₁ y) → refl + ; (inj₂ x) → refl + } } \end{code} Being *commutative* is different from being *commutative up to @@ -413,24 +421,24 @@ For associativity, the `to` function reassociates, and the `from` function does the inverse. Again, the evidence of left and right inverse requires matching against a suitable pattern to enable simplification. \begin{code} -⊎-assoc : ∀ {A B C : Set} → ((A ⊎ B) ⊎ C) ≃ (A ⊎ (B ⊎ C)) +⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C) ⊎-assoc = record - { to = λ{ (inj₁ (inj₁ x)) → (inj₁ x) - ; (inj₁ (inj₂ y)) → (inj₂ (inj₁ y)) - ; (inj₂ z) → (inj₂ (inj₂ z)) - } - ; from = λ{ (inj₁ x) → (inj₁ (inj₁ x)) - ; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y)) - ; (inj₂ (inj₂ z)) → (inj₂ z) - } - ; from∘to = λ{ (inj₁ (inj₁ x)) → refl - ; (inj₁ (inj₂ y)) → refl - ; (inj₂ z) → refl - } - ; to∘from = λ{ (inj₁ x) → refl - ; (inj₂ (inj₁ y)) → refl - ; (inj₂ (inj₂ z)) → refl - } + { to = λ{ (inj₁ (inj₁ x)) → (inj₁ x) + ; (inj₁ (inj₂ y)) → (inj₂ (inj₁ y)) + ; (inj₂ z) → (inj₂ (inj₂ z)) + } + ; from = λ{ (inj₁ x) → (inj₁ (inj₁ x)) + ; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y)) + ; (inj₂ (inj₂ z)) → (inj₂ z) + } + ; from∘to = λ{ (inj₁ (inj₁ x)) → refl + ; (inj₁ (inj₂ y)) → refl + ; (inj₂ z) → refl + } + ; to∘from = λ{ (inj₁ x) → refl + ; (inj₂ (inj₁ y)) → refl + ; (inj₂ (inj₂ z)) → refl + } } \end{code} @@ -451,13 +459,12 @@ data ⊥ : Set where \end{code} There is no possible evidence that `⊥` holds. -Given evidence that `⊥` holds, we might conclude anything! Since -false never holds, knowing that it holds tells us we are in a -paradoxical situation. This is a basic principle of logic, -known in medieval times by the latin phrase *ex falso*, -and known to children through phrases such as -"if pigs had wings, then I'd be the Queen of Sheba". -We formalise it as follows. +Since false never holds, knowing that it holds tells us we are in a +paradoxical situation. Given evidence that `⊥` holds, we might +conclude anything! This is a basic principle of logic, known in +medieval times by the latin phrase *ex falso*, and known to children +through phrases such as "if pigs had wings, then I'd be the Queen of +Sheba". We formalise it as follows. \begin{code} ⊥-elim : ∀ {A : Set} → ⊥ → A ⊥-elim () @@ -473,8 +480,7 @@ is equal to any arbitrary function from `⊥`. uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w uniq-⊥ h () \end{code} -The pattern matching on the left-hand side is essential. Using -the absurd pattern asserts there are no possible values for `w`, +Using the absurd pattern asserts there are no possible values for `w`, so the equation holds trivially. We refer to `⊥` as *empty* type. And, indeed, @@ -497,16 +503,14 @@ a suitable pattern to enable simplification. ⊥-identityˡ : ∀ {A : Set} → (⊥ ⊎ A) ≃ A ⊥-identityˡ = record - { to = λ{ (inj₁ ()) - ; (inj₂ x) → x - } - ; from = λ{ x → inj₂ x - } - ; from∘to = λ{ (inj₁ ()) - ; (inj₂ x) → refl - } - ; to∘from = λ{ x → refl - } + { to = λ{ (inj₁ ()) + ; (inj₂ x) → x + } + ; from = λ{ x → inj₂ x } + ; from∘to = λ{ (inj₁ ()) + ; (inj₂ x) → refl + } + ; to∘from = λ{ x → refl } } \end{code} @@ -609,15 +613,15 @@ arguments of the type `Bool → Tri`: \begin{code} →-count : (Bool → Tri) → ℕ →-count f with f true | f false -... | aa | aa = 1 -... | aa | bb = 2 -... | aa | cc = 3 -... | bb | aa = 4 -... | bb | bb = 5 -... | bb | cc = 6 -... | cc | aa = 7 -... | cc | bb = 8 -... | cc | cc = 9 +... | aa | aa = 1 +... | aa | bb = 2 +... | aa | cc = 3 +... | bb | aa = 4 +... | bb | bb = 5 +... | bb | cc = 6 +... | cc | aa = 7 +... | cc | bb = 8 +... | cc | cc = 9 \end{code} Exponential on types also share a property with exponential on @@ -640,10 +644,10 @@ The proof of the right inverse requires extensionality. currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C) currying = record - { to = λ{ f → λ{ (x , y) → f x y }} - ; from = λ{ g → λ{ x → λ{ y → g (x , y) }}} + { to = λ{ f → λ{ ⟨ x , y ⟩ → f x y }} + ; from = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}} ; from∘to = λ{ f → refl } - ; to∘from = λ{ g → extensionality λ{ (x , y) → refl }} + ; to∘from = λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }} } \end{code} @@ -658,7 +662,7 @@ is isomorphic to a function that accepts a pair of arguments: _+′_ : (ℕ × ℕ) → ℕ Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`. -In a language optimised for pairing, we would take `2 +′ 3` as +In a language optimised for pairing, we would instead take `2 +′ 3` as an abbreviation for `_+′_ (2 , 3)`. Corresponding to the law @@ -676,10 +680,10 @@ is the same as the assertion that if `A` holds then `C` holds and if →-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C)) →-distrib-⊎ = record - { to = λ{ f → ( (λ{ x → f (inj₁ x) }) , (λ{ y → f (inj₂ y) }) ) } - ; from = λ{ (g , h) → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } } + { to = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ } + ; from = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } } ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } } - ; to∘from = λ{ (g , h) → refl } + ; to∘from = λ{ ⟨ g , h ⟩ → refl } } \end{code} @@ -699,10 +703,10 @@ and the rule `η-×` for products. →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C) →-distrib-× = record - { to = λ{ f → ( (λ{ x → proj₁ (f x) }) , (λ{ y → proj₂ (f y)}) ) } - ; from = λ{ (g , h) → λ{ x → (g x , h x) } } + { to = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ } + ; from = λ{ ⟨ g , h ⟩ → λ{ x → ⟨ g x , h x ⟩ } } ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } } - ; to∘from = λ{ (g , h) → refl } + ; to∘from = λ{ ⟨ g , h ⟩ → refl } } \end{code} @@ -715,17 +719,17 @@ this fact is similar in structure to our previous results. ×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C) ×-distrib-⊎ = record - { to = λ{ ((inj₁ x) , z) → (inj₁ (x , z)) - ; ((inj₂ y) , z) → (inj₂ (y , z)) + { to = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩) + ; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩) } - ; from = λ{ (inj₁ (x , z)) → ((inj₁ x) , z) - ; (inj₂ (y , z)) → ((inj₂ y) , z) + ; from = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩ + ; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩ } - ; from∘to = λ{ ((inj₁ x) , z) → refl - ; ((inj₂ y) , z) → refl + ; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl + ; ⟨ inj₂ y , z ⟩ → refl } - ; to∘from = λ{ (inj₁ (x , z)) → refl - ; (inj₂ (y , z)) → refl + ; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl + ; (inj₂ ⟨ y , z ⟩) → refl } } \end{code} @@ -735,21 +739,21 @@ Sums do not distribute over products up to isomorphism, but it is an embedding. ⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C) ⊎-distrib-× = record - { to = λ{ (inj₁ (x , y)) → (inj₁ x , inj₁ y) - ; (inj₂ z) → (inj₂ z , inj₂ z) + { to = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩ + ; (inj₂ z) → ⟨ inj₂ z , inj₂ z ⟩ } - ; from = λ{ (inj₁ x , inj₁ y) → (inj₁ (x , y)) - ; (inj₁ x , inj₂ z) → (inj₂ z) - ; (inj₂ z , _ ) → (inj₂ z) + ; from = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩) + ; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z) + ; ⟨ inj₂ z , _ ⟩ → (inj₂ z) } - ; from∘to = λ{ (inj₁ (x , y)) → refl - ; (inj₂ z) → refl + ; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl + ; (inj₂ z) → refl } } \end{code} Note that there is a choice in how we write the `from` function. -As given, it takes `(inj₂ z , inj₂ z′)` to `(inj₂ z)`, but it is -easy to write a variant that instead returns `(inj₂ z′)`. We have +As given, it takes `⟨ inj₂ z , inj₂ z′ ⟩` to `inj₂ z`, but it is +easy to write a variant that instead returns `inj₂ z′`. We have an embedding rather than an isomorphism because the `from` function must discard either `z` or `z′` in this case. @@ -796,7 +800,7 @@ Show that `A ⇔ B` is isomorphic to `(A → B) × (B → A)`. Definitions similar to those in this chapter can be found in the standard library. \begin{code} -import Data.Product using (_×_; _,_; proj₁; proj₂) +import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) import Data.Unit using (⊤; tt) import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to ⊎-elim) import Data.Empty using (⊥; ⊥-elim) diff --git a/src/Lists.lagda b/src/Lists.lagda index e7ab2b8f..d842372b 100644 --- a/src/Lists.lagda +++ b/src/Lists.lagda @@ -4,8 +4,8 @@ layout : page permalink : /Lists --- -This chapter discusses the list data type. It uses many of the techniques -developed for natural numbers in a different context, and provides +This chapter discusses the list data type. It gives further examples +of many of the techniques we have developed so far, and provides examples of polymorphic types and functions. ## Imports @@ -26,52 +26,44 @@ open import Isomorphism using (_≃_) Lists are defined in Agda as follows. \begin{code} data List (A : Set) : Set where - [] : List A + [] : List A _∷_ : A → List A → List A infixr 5 _∷_ \end{code} -Let's unpack this definition. The phrase - - List (A : Set) : Set - -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. +Let's unpack this definition. If `A` is a set, then `List A` is a set. +The next two lines tell us that `[]` (pronounced *nil*) is a list of +type `A` (often called the *empty* list), 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 ∷ [] +_ : List ℕ +_ = 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 ∷ []))`. +associates to the right, the term 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, +*tail*. Lists are a rather strange beast: they have 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. +As we've seen, parameterised types can be translated to +indexed types. The definition above is equivalent to the following. \begin{code} data List′ : Set → Set where - []′ : ∀ {A : Set} → List′ A + []′ : ∀ {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. +Each constructor takes the parameter as an implicit argument. +Thus, our example list could also be written +\begin{code} +_ : List ℕ +_ = _∷_ {ℕ} 0 (_∷_ {ℕ} 1 (_∷_ {ℕ} 2 ([] {ℕ}))) +\end{code} +where here we have made the implicit parameters explicit. Including the lines @@ -81,37 +73,25 @@ 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 syntax We can write lists more conveniently by introducing the following definitions. \begin{code} --- [_] : ∀ {A : Set} → A → List A --- pattern [ z ] = z ∷ [] pattern [_] z = z ∷ [] - --- [_,_] : ∀ {A : Set} → A → A → List A --- pattern [ y , z ] = y ∷ z ∷ [] pattern [_,_] y z = y ∷ z ∷ [] - --- [_,_,_] : ∀ {A : Set} → A → A → A → List A --- pattern [ x , y , z ] = x ∷ y ∷ z ∷ [] pattern [_,_,_] x y z = x ∷ y ∷ z ∷ [] - --- [_,_,_,_] : ∀ {A : Set} → A → A → A → A → List A --- pattern [ w , x , y , z ] = w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_] w x y z = w ∷ x ∷ y ∷ z ∷ [] - --- [_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → List A --- pattern [ v , w , x , y , z ] = v ∷ w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_,_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ [] - --- [_,_,_,_,_,_] : ∀ {A : Set} → A → A → A → A → A → A → List A --- pattern [ u , v , w , x , y , z ] = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ [] pattern [_,_,_,_,_,_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ [] \end{code} -Agda recognises that this is a bracketing notation, -and hence we can write things like `length [ 0 , 1 , 2 ]` -rather than `length ([ 0 , 1 , 2 ])`. +This is our first use of pattern declarations. For instance, +the third line tells us that `[ x , y , z ]` is equivalent to +`x ∷ y ∷ z ∷ []`, and permits the former to appear either in +a pattern on the left-hand side of an equation, or a term +on the right-hand side of an equation. +Agda recognises `[_,_,_]` as a bracketing notation, and hence `length +[ 0 , 1 , 2 ]` parses as `length ([ 0 , 1 , 2 ])`. ## Append diff --git a/src/Preface.lagda b/src/Preface.lagda index 14f26250..82a9ba58 100644 --- a/src/Preface.lagda +++ b/src/Preface.lagda @@ -13,15 +13,21 @@ March 2018. When that is done it will be announced here, and that would be an excellent time to comment on the first part. -## Personal remarks +## Personal remarks: From TAPL to PLTA -Since 2013, I teach a course on Types and Semantics for Programming -Languages to fourth-year undergraduates and masters students at the -University of Edinburgh. That course had been based on the textbook -[Software Foundations][sf], by Pierce and others, written in Coq. I -am convinced of Pierce's claim that basing a course around a proof -assistant aids learning, as summarised in his ICFP Keynote, [Lambda, -The Ultimate TA][ta]. +I, along with many others, am a fan of Peirce's [Types and Programming +Languages][tapl], known by the acronym TAPL. One of my best students +started writing his own systems with no help from me, trained by that +book. + +Since 2013, I have taught a course on Types and Semantics for +Programming Languages to fourth-year undergraduates and masters +students at the University of Edinburgh. That course is not based on +TAPL, but on Pierce's subsequent textbook, [Software Foundations], +written in collaboration with others and based on Coq. I am convinced +of Pierce's claim that basing a course around a proof assistant aids +learning, as summarised in his ICFP Keynote, [Lambda, The Ultimate +TA][ta]. However, after five years of experience, I have come to the conclusion that Coq may not be the best vehicle. Too much of the course needs to @@ -69,6 +75,7 @@ Most of the text was written during a sabbatical in the first half of 2018. -- Philip Wadler, Rio de Janeiro, January--June 2018 +[tapl]: http://www.cis.upenn.edu/~bcpierce/tapl/index.html [sf]: https://softwarefoundations.cis.upenn.edu/ [ta]: http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf [stump]: http://www.morganclaypoolpublishers.com/catalog_Orig/product_info.php?cPath=24&products_id=908 diff --git a/src/Relations.lagda b/src/Relations.lagda index 57d47b6c..cce5075f 100644 --- a/src/Relations.lagda +++ b/src/Relations.lagda @@ -271,48 +271,6 @@ given `suc m ≤ suc n` and `suc n ≤ suc m` and must show `suc m ≡ suc n`. The inductive hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal follows by congruence. - - - - - ## Total