From 375df5c3c5e6c410287bd0a5f19b18c03522f376 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Fri, 11 Sep 2020 23:26:34 +0200 Subject: [PATCH 1/6] DeBruijn: introduce a version of #_ that depends on no postulate --- src/plfa/part2/DeBruijn.lagda.md | 56 ++++++++++++++++++++++---------- 1 file changed, 38 insertions(+), 18 deletions(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index 72bc236a..a84f0d1a 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -46,8 +46,9 @@ James Chapman, James McKinna, and many others. import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import Data.Empty using (⊥; ⊥-elim) -open import Data.Nat using (ℕ; zero; suc) +open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s) open import Relation.Nullary using (¬_) +open import Relation.Nullary.Decidable using (True; toWitness) ``` ## Introduction @@ -271,6 +272,16 @@ is a context with two variables in scope, where the outer bound one has type `` `ℕ ⇒ `ℕ ``, and the inner bound one has type `` `ℕ ``. +We define a helper function that computes the length of a context, +which will be useful later in making sure an index is within context +bounds: + +``` +length : Context → ℕ +length ∅ = zero +length (Γ , _) = suc (length Γ) +``` + ### Variables and the lookup judgment Intrinsically-typed variables correspond to the lookup judgment. @@ -414,33 +425,42 @@ The final term represents the Church numeral two. We can use a natural number to select a type from a context: ``` -lookup : Context → ℕ → Type -lookup (Γ , A) zero = A -lookup (Γ , _) (suc n) = lookup Γ n -lookup ∅ _ = ⊥-elim impossible - where postulate impossible : ⊥ +lookup : (Γ : Context) → (n : ℕ) → (p : n < length Γ) → Type +lookup (_ , A) zero (s≤s z≤n) = A +lookup (Γ , _) (suc n) (s≤s p) = lookup Γ n p ``` -We intend to apply the function only when the natural is -shorter than the length of the context, which we indicate by -postulating an `impossible` term, just as we did -[here]({{ site.baseurl }}/Lambda/#primed). +The function takes a proof `p` that the natural number is within the +context's bounds. This guarantees we will never try to select a type +at a non-existing position within the context. Strict inequality `n < +length Γ` holds whenever inequality `suc n ≤ length Γ` holds. When +recursing, proof `p` is pattern-matched via the `s≤s` constructor to a +proof for a context with the rightmost type removed. Given the above, we can convert a natural to a corresponding de Bruijn index, looking up its type in the context: ``` -count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n -count {Γ , _} zero = Z -count {Γ , _} (suc n) = S (count n) -count {∅} _ = ⊥-elim impossible - where postulate impossible : ⊥ +count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p +count {_ , _} zero (s≤s z≤n) = Z +count {Γ , _} (suc n) (s≤s p) = S (count n p) ``` -This requires the same trick as before. We can then introduce a convenient abbreviation for variables: ``` -#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n -# n = ` count n +#_ : ∀ {Γ} + → (n : ℕ) + → {p : True (suc n ≤? length Γ)} + -------------------------------- + → Γ ⊢ lookup Γ n (toWitness p) +#_ n {p} = ` count n (toWitness p) ``` +The type of function `#_` asks for clarification. The function takes +an implicit argument `p` that signals if there is evidence for `n` +to be within the context's bounds. If `n` is within the bounds, `p`'s +type `True (suc n ≤? length Γ)` will compute to `⊤`, the familiar unit +type with only one value. If `n` is not within the bounds, the type +will compute to `⊥`, which is an inhabited type and the call to `#_` +for such an `n` will fail to type-check. Finally, in the return type +`p` is converted to a witness that `n` is within the bounds. With this abbreviation, we can rewrite the Church numeral two more compactly: ``` From 318ff6f491ee1313c4580d540230e71a639841f2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 12 Sep 2020 23:00:35 +0200 Subject: [PATCH 2/6] Polishes an updated alternative formalisation of variables via de Bruijn indices --- src/plfa/part2/DeBruijn.lagda.md | 49 +++++++++++++++----------------- 1 file changed, 23 insertions(+), 26 deletions(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index a84f0d1a..b9ca447e 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -272,16 +272,6 @@ is a context with two variables in scope, where the outer bound one has type `` `ℕ ⇒ `ℕ ``, and the inner bound one has type `` `ℕ ``. -We define a helper function that computes the length of a context, -which will be useful later in making sure an index is within context -bounds: - -``` -length : Context → ℕ -length ∅ = zero -length (Γ , _) = suc (length Γ) -``` - ### Variables and the lookup judgment Intrinsically-typed variables correspond to the lookup judgment. @@ -423,11 +413,19 @@ The final term represents the Church numeral two. ### Abbreviating de Bruijn indices +We define a helper function that computes the length of a context, +which will be useful in making sure an index is within context bounds: +``` +length : Context → ℕ +length ∅ = zero +length (Γ , _) = suc (length Γ) +``` + We can use a natural number to select a type from a context: ``` -lookup : (Γ : Context) → (n : ℕ) → (p : n < length Γ) → Type -lookup (_ , A) zero (s≤s z≤n) = A -lookup (Γ , _) (suc n) (s≤s p) = lookup Γ n p +lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type +lookup {(_ , A)} {zero} (s≤s z≤n) = A +lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p ``` The function takes a proof `p` that the natural number is within the context's bounds. This guarantees we will never try to select a type @@ -439,28 +437,27 @@ proof for a context with the rightmost type removed. Given the above, we can convert a natural to a corresponding de Bruijn index, looking up its type in the context: ``` -count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p -count {_ , _} zero (s≤s z≤n) = Z -count {Γ , _} (suc n) (s≤s p) = S (count n p) +count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p +count {_ , _} {zero} (s≤s z≤n) = Z +count {Γ , _} {(suc n)} (s≤s p) = S (count p) ``` We can then introduce a convenient abbreviation for variables: ``` #_ : ∀ {Γ} → (n : ℕ) - → {p : True (suc n ≤? length Γ)} + → {n Date: Tue, 22 Sep 2020 07:51:29 +0200 Subject: [PATCH 3/6] DeBruijn: update a figure in the golden section to reflect a change in representation --- src/plfa/part2/DeBruijn.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index b9ca447e..ac9eacc4 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -1376,7 +1376,7 @@ number of lines of code is as follows: Lambda 216 Properties 235 - DeBruijn 275 + DeBruijn 276 The relation between the two approaches approximates the golden ratio: extrinsically-typed terms From ef3b3b00aac253644999d46c0e06bbd4748ccabc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Fri, 25 Sep 2020 12:18:56 +0200 Subject: [PATCH 4/6] Adds a missing closing parenthesis --- src/plfa/part2/DeBruijn.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index ac9eacc4..1161250e 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -454,7 +454,7 @@ We can then introduce a convenient abbreviation for variables: The type of function `#_` asks for clarification. The function takes an implicit argument `n Date: Thu, 1 Oct 2020 22:33:59 +0200 Subject: [PATCH 5/6] De Bruijn: implement feedback to PR #514 by Wadler and Kokke --- src/plfa/part2/DeBruijn.lagda.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index 1161250e..d1158fe6 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -451,13 +451,16 @@ We can then introduce a convenient abbreviation for variables: → Γ ⊢ lookup (toWitness n Date: Fri, 2 Oct 2020 14:18:37 +0200 Subject: [PATCH 6/6] De Bruijn: Implements Wadler's feedback to PR #514 --- src/plfa/part2/DeBruijn.lagda.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index d1158fe6..522f5457 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -451,9 +451,8 @@ We can then introduce a convenient abbreviation for variables: → Γ ⊢ lookup (toWitness n