Alternative formalisation of variables via de Bruijn indices

[mdimjasevic]

In chapter "DeBruijn: Intrinsically-typed de Bruijn representation", there is a formalisation of variables #_ via de Bruijn indices:

lookup : Context → ℕ → Type
lookup (Γ , A) zero     =  A
lookup (Γ , _) (suc n)  =  lookup Γ n
lookup ∅       _        =  ⊥-elim impossible
  where postulate impossible : ⊥

count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
count {Γ , _} zero     =  Z
count {Γ , _} (suc n)  =  S (count n)
count {∅}     _        =  ⊥-elim impossible
  where postulate impossible : ⊥

#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
# n  =  ` count n

This formalisation relies on postulates to avoid handling the case when a de Bruijn index is out of context bounds. In my view, usage of postulates should be discouraged in the book as postulates in general open room for inconsistency.

Instead, I propose an alternative definition of the three functions above, lookup', count' and #'_, respectively, that uses no postulates, yet the alternative functions guarantee that a de Bruijn index is within the bounds. This development should require no further modifications to the formalisation in the rest of the chapter. At first I was planning to propose to make Context indexed by its size, but I gave up on that approach as it would require quite a few changes in the chapter.

Here is what is different compared to the formalisation from the book:

open import Data.Empty using (⊥)
open import Data.Nat as Nat using (ℕ; zero; suc; _<_; s≤s; z≤n)
open import Data.Nat.Properties using (≤-pred)
open import Data.Unit using (⊤; tt)


length : Context → ℕ
length ∅        =  zero
length (Γ , _)  =  suc (length Γ)

lookup' : (Γ : Context) → (n : ℕ) → (n < length Γ) → Type
lookup' (_ , A) zero _         =  A
lookup' (Γ , _) (suc n) ≤-suc  =  lookup' Γ n (≤-pred ≤-suc)

count' : ∀ {Γ} → (n : ℕ) → (s : n < length Γ) → Γ ∋ lookup' Γ n s
count' {_ , _} zero _         =  Z
count' {Γ , A} (suc n) ≤-suc  =  S (count' n (≤-pred ≤-suc))

_≤?_ : ∀ (m n : ℕ) → Set
zero  ≤? n      =  ⊤
suc m ≤? zero   =  ⊥
suc m ≤? suc n  =  m ≤? n

soundness-< : ∀(m n : ℕ) → suc m ≤? n → m < n
soundness-< zero    (suc n) tt    =  s≤s z≤n
soundness-< (suc m) (suc n) m≤?n  =  s≤s (soundness-< m n m≤?n)

#'_ : ∀ {Γ}
  → (n : ℕ)
  → {s : suc n ≤? length Γ}
    --------------------------------------------
  → Γ ⊢ lookup' Γ n (soundness-< n (length Γ) s)
#'_ {Γ} n {s}  =  ` count' n (soundness-< n (length Γ) s)

-- Church numeral two
_ : ∅ ⊢ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ
_ = ƛ ƛ (#' 1 · (#' 1 · #' 0))

[wenkokke]

Ahh! This was supposed to have been fixed as part of #409. With the changes in Decidable, this can be more succinctly expressed as:

#_ : ∀ {Γ}
   → (n : ℕ)
   → {p : True (suc n ≤? length Γ)}
     --------------------------------
   → Γ ⊢ lookup Γ n (toWitness p)
#_ n {p}  =  ` count n (toWitness p)

Using your definitions for length, lookup, and count, and True, toWitness, and ≤? from the chapter Decidable.

[mdimjasevic]

Oh, I forgot to check earlier chapters, but I had a feeling that useful helper functions were already defined! Thank you for pointing them out!

If you're OK with updating the definition of #_ according to this discussion here, I can make a pull request with the update to the de Bruijn chapter.

[wenkokke]

Updating the definition would require rewriting the text. Furthermore, I seem to recall @wadler specifically wanted to leave this in to have an example of using postulates to define partial functions when it's safe to do so. @wadler?

[wadler]

Wen, I thought we agreed that you would rewrite this along the lines you proposed? I think showing the right way to do it is probably more important than showing the "postulate" technique.

[wenkokke]

I believe you wanted to keep at least one occurance of the impossible postulate in a prominent position. However, it may well be that we agreed on a different section to keep impossible, and I've simply forgotten to update this one. If you agree, I'm happy to rewrite this section to eliminate the use of impossible.