From 43b46ef77541c837a11bfbe9a484443a5f57f79a Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 20 Jun 2017 14:20:47 +0100 Subject: [PATCH] updated Maps --- src/Maps.lagda | 230 +++++++++++++++++++++++++++---------------------- src/Stlc.lagda | 44 ++++++++-- 2 files changed, 165 insertions(+), 109 deletions(-) diff --git a/src/Maps.lagda b/src/Maps.lagda index 7a0924d8..941f7c1f 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -35,10 +35,11 @@ standard library, wherever they overlap. \begin{code} open import Function using (_∘_) open import Data.Bool using (Bool; true; false) +open import Data.Nat using (ℕ) open import Data.Empty using (⊥; ⊥-elim) open import Data.Maybe using (Maybe; just; nothing) -open import Data.Nat using (ℕ) -open import Relation.Nullary using (Dec; yes; no) +open import Data.String using (String) +open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Binary.PropositionalEquality \end{code} @@ -55,17 +56,29 @@ function for ids and its fundamental property. \begin{code} data Id : Set where - id : ℕ → Id + id : String → Id \end{code} \begin{code} _≟_ : (x y : Id) → Dec (x ≡ y) -id x ≟ id y with x Data.Nat.≟ y -id x ≟ id y | yes x=y rewrite x=y = yes refl -id x ≟ id y | no x≠y = no (x≠y ∘ id-inj) +id x ≟ id y with x Data.String.≟ y +id x ≟ id y | yes refl = yes refl +id x ≟ id y | no x≠y = no (x≠y ∘ id-inj) where id-inj : ∀ {x y} → id x ≡ id y → x ≡ y - id-inj refl = refl + id-inj refl = refl + +-- contrapositive : ∀ {P Q} → (P → Q) → (¬ Q → ¬ P) +-- contrapositive p→q ¬q p = ¬q (p→q p) +\end{code} + +We define some identifiers for future use. + +\begin{code} +x y z : Id +x = id "x" +y = id "y" +z = id "z" \end{code} ## Total Maps @@ -105,31 +118,43 @@ applied to any id. \begin{code} empty : ∀ {A} → A → TotalMap A - empty x = λ _ → x + empty v x = v \end{code} -More interesting is the `update` function, which (as before) takes -a map $$m$$, a key $$x$$, and a value $$v$$ and returns a new map that -takes $$x$$ to $$v$$ and takes every other key to whatever $$m$$ does. +More interesting is the update function, which (as before) takes +a map $$ρ$$, a key $$x$$, and a value $$v$$ and returns a new map that +takes $$x$$ to $$v$$ and takes every other key to whatever $$ρ$$ does. \begin{code} - update : ∀ {A} → TotalMap A -> Id -> A -> TotalMap A - update m x v y with x ≟ y + _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A + (ρ , x ↦ v) y with x ≟ y ... | yes x=y = v - ... | no x≠y = m y + ... | no x≠y = ρ y \end{code} This definition is a nice example of higher-order programming. -The `update` function takes a _function_ $$m$$ and yields a new -function $$\lambda x'.\vdots$$ that behaves like the desired map. +The update function takes a _function_ $$ρ$$ and yields a new +function that behaves like the desired map. -For example, we can build a map taking ids to bools, where `id -3` is mapped to `true` and every other key is mapped to `false`, -like this: +We define handy abbreviations for updating a map two, three, or four times. \begin{code} - examplemap : TotalMap Bool - examplemap = update (update (empty false) (id 1) false) (id 3) true + _,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → TotalMap A + ρ , x₁ ↦ v₁ , x₂ ↦ v₂ = (ρ , x₁ ↦ v₁), x₂ ↦ v₂ + + _,_↦_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → Id → A → TotalMap A + ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃ = ((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃ + + _,_↦_,_↦_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → Id → A → Id → A → TotalMap A + ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃ , x₄ ↦ v₄ = (((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃), x₄ ↦ v₄ +\end{code} + +For example, we can build a map taking ids to naturals, where $$x$$ +maps to 42, $$y$$ maps to 69, and every other key maps to 0, as follows: + +\begin{code} + ρ₀ : TotalMap ℕ + ρ₀ = empty 0 , x ↦ 42 , y ↦ 69 \end{code} This completes the definition of total maps. Note that we don't @@ -137,57 +162,52 @@ need to define a `find` operation because it is just function application! \begin{code} - test_examplemap0 : examplemap (id 0) ≡ false - test_examplemap0 = refl + test₁ : ρ₀ x ≡ 42 + test₁ = refl - test_examplemap1 : examplemap (id 1) ≡ false - test_examplemap1 = refl + test₂ : ρ₀ y ≡ 69 + test₂ = refl - test_examplemap2 : examplemap (id 2) ≡ false - test_examplemap2 = refl - - test_examplemap3 : examplemap (id 3) ≡ true - test_examplemap3 = refl + test₃ : ρ₀ z ≡ 0 + test₃ = refl \end{code} To use maps in later chapters, we'll need several fundamental facts about how they behave. Even if you don't work the following -exercises, make sure you thoroughly understand the statements of -the lemmas! (Some of the proofs require the functional -extensionality axiom, which is discussed in the [Logic] -chapter and included in the Agda standard library.) +exercises, make sure you understand the statements of +the lemmas! #### Exercise: 1 star, optional (apply-empty) First, the empty map returns its default element for all keys: \begin{code} postulate - apply-empty : ∀ {A x v} → empty {A} v x ≡ v + apply-empty : ∀ {A} (v : A) (x : Id) → empty v x ≡ v \end{code} #### Exercise: 2 stars, optional (update-eq) -Next, if we update a map $$m$$ at a key $$x$$ with a new value $$v$$ -and then look up $$x$$ in the map resulting from the `update`, we get +Next, if we update a map $$ρ$$ at a key $$x$$ with a new value $$v$$ +and then look up $$x$$ in the map resulting from the update, we get back $$v$$: \begin{code} postulate - update-eq : ∀ {A v} (m : TotalMap A) (x : Id) - → (update m x v) x ≡ v + update-eq : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) + → (ρ , x ↦ v) x ≡ v \end{code}