From 53702d6e67b47ab2dc4306d3e5d1e732154767f3 Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 18 Jun 2018 12:56:20 -0700 Subject: [PATCH] move lambda and extensionality to Isomorphism, fix links --- src/plta/Connectives.lagda | 12 +---- src/plta/Decidable.lagda | 13 +++--- src/plta/Equality.lagda | 82 +------------------------------- src/plta/Isomorphism.lagda | 96 +++++++++++++++++++++++++++++++++++++- src/plta/Lists.lagda | 8 ---- src/plta/Modules.lagda | 10 +--- src/plta/Preface.lagda | 2 +- src/plta/Quantifiers.lagda | 12 +---- 8 files changed, 107 insertions(+), 128 deletions(-) diff --git a/src/plta/Connectives.lagda b/src/plta/Connectives.lagda index 1ab9e5a4..7191bc92 100644 --- a/src/plta/Connectives.lagda +++ b/src/plta/Connectives.lagda @@ -26,20 +26,12 @@ import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong) open Eq.≡-Reasoning open import Data.Nat using (ℕ; zero; suc; _+_; _*_) -open import Data.Nat.Properties.Simple using (+-suc) +open import Data.Nat.Properties using (+-suc) open import Function using (_∘_) -open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_) +open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality) open plta.Isomorphism.≃-Reasoning \end{code} -We assume [extensionality][extensionality]. -\begin{code} -postulate - extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g -\end{code} - -[extensionality]: ../Equality/index.html#extensionality - ## Conjunction is product diff --git a/src/plta/Decidable.lagda b/src/plta/Decidable.lagda index ffef6298..07abe8a4 100644 --- a/src/plta/Decidable.lagda +++ b/src/plta/Decidable.lagda @@ -33,7 +33,9 @@ open import Function using (_∘_) ## Evidence vs Computation -Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %}) defined comparison an inductive datatype, which provides *evidence* that one number is less than or equal to another. +Recall that Chapter [Relations]({{ site.baseurl }}{% link out/plta/Relations.md %}) +defined comparison an inductive datatype, which provides *evidence* that one number +is less than or equal to another. \begin{code} infix 4 _≤_ @@ -62,11 +64,8 @@ data Bool : Set where true : Bool false : Bool \end{code} -We will use `true` to represent the case where a proposition holds, -and `false` to represent the case where a proposition fails to hold. - Given booleans, we can define a function of two numbers that -*computes* to true if the comparison holds, and false otherwise. +*computes* to `true` if the comparison holds and to `false` otherwise. \begin{code} infix 4 _≤ᵇ_ @@ -347,8 +346,8 @@ exactly when `m ≤ n` is inhabited. ≤→≤ᵇ′ = fromWitness \end{code} -In summary, it is usually best to eschew booleans and rely on decidables instead. If you -need booleans, they and their properties are easily derived from the +In summary, it is usually best to eschew booleans and rely on decidables instead. +If you need booleans, they and their properties are easily derived from the corresponding decidables. ## Logical connectives diff --git a/src/plta/Equality.lagda b/src/plta/Equality.lagda index 8bba8249..f96d2287 100644 --- a/src/plta/Equality.lagda +++ b/src/plta/Equality.lagda @@ -114,7 +114,7 @@ Again, a useful exercise is to carry out an interactive development, checking how Agda's knowledge changes as each of the two arguments is instantiated. -## Congruence and substitution +## Congruence and substitution {#cong} Equality satisfies *congruence*. If two terms are equal, they remain so after the same function is applied to both. @@ -404,86 +404,6 @@ Nonetheless, rewrite is a vital part of the Agda toolkit, as earlier examples have shown. -## Lambda expressions - -We pause for a moment to define *lambda expressions*, which provide a -compact way to define functions without naming them, and will prove -convenient in much of what follows. - -A term of the form - - λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ } - -is equivalent to a function `f` defined by the equations - - f P₁ = e₁ - ⋯ - f Pᵢ = eᵢ - -where the `Pᵢ` are patterns (left-hand sides of an equation) and the -`Nᵢ` are expressions (right-hand side of an equation). - -In the case that the pattern is a variable, we may also use the syntax - - λ x → N - -or - - λ (x : A) → N - -both of which are equivalent to `λ{ x → N }`. The latter allows one to -specify the domain of the function. - -Often using an anonymous lambda expression is more convenient than -using a named function: it avoids a lengthy type declaration; and the -definition appears exactly where the function is used, so there is no -need for the writer to remember to declare it in advance, or for the -reader to search for the definition elsewhere in the code. - - -## Extensionality {#extensionality} - -Extensionality asserts that the only way to distinguish functions is -by applying them; if two functions applied to the same argument always -yield the same result, then they are the same functions. It is the -converse of `cong-app`, introduced earlier. - -Agda does not presume extensionality, but we can postulate that it holds. -\begin{code} -postulate - extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g -\end{code} -Postulating extensionality does not lead to difficulties, as it is -known to be consistent with the theory that underlies Agda. - -As an example, consider that we need results from two libraries, -one where addition is defined as above, and one where it is -defined the other way around. -\begin{code} -_+′_ : ℕ → ℕ → ℕ -m +′ zero = m -m +′ suc n = suc (m +′ n) -\end{code} -Applying commutativity, it is easy to show that both operators always -return the same result given the same arguments. -\begin{code} -same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n -same-app m n rewrite +-comm m n = helper m n - where - helper : ∀ (m n : ℕ) → m +′ n ≡ n + m - helper m zero = refl - helper m (suc n) = cong suc (helper m n) -\end{code} -However, it might be convenient to assert that the two operators are -actually indistinguishable. This we can do via two applications of -extensionality. -\begin{code} -same : _+′_ ≡ _+_ -same = extensionality λ{m → extensionality λ{n → same-app m n}} -\end{code} -We will occasionally have need to postulate extensionality in what follows. - - ## Leibniz equality The form of asserting equivalence that we have used is due to Martin Löf, diff --git a/src/plta/Isomorphism.lagda b/src/plta/Isomorphism.lagda index 17498fc4..f5ce1828 100644 --- a/src/plta/Isomorphism.lagda +++ b/src/plta/Isomorphism.lagda @@ -21,8 +21,50 @@ distributivity. import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong; cong-app) open Eq.≡-Reasoning +open import Data.Nat using (ℕ; zero; suc; _+_) +open import Data.Nat.Properties using (+-comm) \end{code} + +## Lambda expressions + +The chapter begins with a few preliminaries that will be useful +here and elsewhere: lambda expressions, function composition, and +extensionality. + +*Lambda expressions* provide a compact way to define functions without +naming them. A term of the form + + λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ } + +is equivalent to a function `f` defined by the equations + + f P₁ = e₁ + ⋯ + f Pᵢ = eᵢ + +where the `Pᵢ` are patterns (left-hand sides of an equation) and the +`Nᵢ` are expressions (right-hand side of an equation). + +In the case that there is one equation and the pattern is a variable, +we may also use the syntax + + λ x → N + +or + + λ (x : A) → N + +both of which are equivalent to `λ{x → N}`. The latter allows one to +specify the domain of the function. + +Often using an anonymous lambda expression is more convenient than +using a named function: it avoids a lengthy type declaration; and the +definition appears exactly where the function is used, so there is no +need for the writer to remember to declare it in advance, or for the +reader to search for the definition elsewhere in the code. + + ## Function composition In what follows, we will make use of function composition. @@ -31,12 +73,62 @@ _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) (g ∘ f) x = g (f x) \end{code} Thus, `g ∘ f` is the function that first applies `f` and -then applies `g`. +then applies `g`. An equivalent definition, exploiting lambda +expressions, is as follows. +\begin{code} +_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) +g ∘′ f = λ x → g (f x) +\end{code} + + +## Extensionality {#extensionality} + +Extensionality asserts that the only way to distinguish functions is +by applying them; if two functions applied to the same argument always +yield the same result, then they are the same functions. It is the +converse of `cong-app`, as introduced +[earlier]({{ site.baseurl }}{% link out/plta/Equality.md %}/#cong). + +Agda does not presume extensionality, but we can postulate that it holds. +\begin{code} +postulate + extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g +\end{code} +Postulating extensionality does not lead to difficulties, as it is +known to be consistent with the theory that underlies Agda. + +As an example, consider that we need results from two libraries, +one where addition is defined as in +Chapter [Naturals]({{ site.baseurl }}{% link out/plta/Naturals.md %}) +and one where it is defined the other way around. +\begin{code} +_+′_ : ℕ → ℕ → ℕ +m +′ zero = m +m +′ suc n = suc (m +′ n) +\end{code} +Applying commutativity, it is easy to show that both operators always +return the same result given the same arguments. +\begin{code} +same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n +same-app m n rewrite +-comm m n = helper m n + where + helper : ∀ (m n : ℕ) → m +′ n ≡ n + m + helper m zero = refl + helper m (suc n) = cong suc (helper m n) +\end{code} +However, it might be convenient to assert that the two operators are +actually indistinguishable. This we can do via two applications of +extensionality. +\begin{code} +same : _+′_ ≡ _+_ +same = extensionality (λ m → extensionality (λ n → same-app m n)) +\end{code} +We will occasionally need to postulate extensionality in what follows. ## Isomorphism -In set theory, two sets are isomorphic if they are in one-to-one correspondence. +Two sets are isomorphic if they are in one-to-one correspondence. Here is a formal definition of isomorphism. \begin{code} infix 0 _≃_ diff --git a/src/plta/Lists.lagda b/src/plta/Lists.lagda index 10e195aa..d348af40 100644 --- a/src/plta/Lists.lagda +++ b/src/plta/Lists.lagda @@ -28,14 +28,6 @@ open import Level using (Level) open import plta.Isomorphism using (_≃_) \end{code} -We assume [extensionality][extensionality]. -\begin{code} -postulate - extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g -\end{code} - -[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality - ## Lists diff --git a/src/plta/Modules.lagda b/src/plta/Modules.lagda index 9855489e..1e6b6483 100644 --- a/src/plta/Modules.lagda +++ b/src/plta/Modules.lagda @@ -23,23 +23,15 @@ open Eq.≡-Reasoning open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n) open import Relation.Nullary using (¬_) open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩) -open import plta.Isomorphism using (_≃_) open import Function using (_∘_) open import Level using (Level) open import Data.Maybe using (Maybe; just; nothing) open import Data.List using (List; []; _∷_; _++_; map; foldr; downFrom) open import Data.List.All using (All; []; _∷_) open import Data.List.Any using (Any; here; there) +open import plta.Isomorphism using (_≃_; extensionality) \end{code} -We assume [extensionality][extensionality]. -\begin{code} -postulate - extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g -\end{code} - -[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality - ## Modules diff --git a/src/plta/Preface.lagda b/src/plta/Preface.lagda index 8cde949e..ce17c6aa 100644 --- a/src/plta/Preface.lagda +++ b/src/plta/Preface.lagda @@ -78,7 +78,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 +[tapl]: http://www.cis.upenn.edu/~bcpierce/tapl/ [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/plta/Quantifiers.lagda b/src/plta/Quantifiers.lagda index 5f9ba715..1b119d9a 100644 --- a/src/plta/Quantifiers.lagda +++ b/src/plta/Quantifiers.lagda @@ -22,17 +22,9 @@ open import Relation.Nullary using (¬_) open import Function using (_∘_) open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_) +open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality) \end{code} -We assume [extensionality][extensionality]. -\begin{code} -postulate - extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g -\end{code} - -[extensionality]: {{ site.baseurl }}{% link out/plta/Equality.md %}#extensionality - ## Universals @@ -217,7 +209,7 @@ The result can be viewed as a generalisation of currying. Indeed, the code to establish the isomorphism is identical to what we wrote when discussing [implication][implication]. -[implication]: {{ site.baseurl }}{% link out/plta/Connectives.md %}/index.html#implication +[implication]: {{ site.baseurl }}{% link out/plta/Connectives.md %}/#implication ### Exercise (`∃-distrib-⊎`)