An implementation of “each name is its own scope” de Bruijn indices

NamedDeBruijn.agda

{-# OPTIONS --safe --without-K --postfix-projections #-}

module NamedDeBruijn where

  open import Data.Bool
  open import Data.Product
  open import Function.Base using (id)
  open import Relation.Binary using (DecidableEquality)
  open import Relation.Binary.PropositionalEquality
  open import Relation.Nullary

  infixr 5 _→ᵗ_
  infix 5 _∙_
  infix 4 _∋_

  data Tree (A : Set) : Set where
    [_] : A → Tree A
    ε : Tree A
    _∙_ : (s t : Tree A) → Tree A

  data _∋_ {A} : Tree A → A → Set where
    here : ∀ {x} → [ x ] ∋ x
    ↙ : ∀ {s t x} → s ∋ x → s ∙ t ∋ x
    ↘ : ∀ {s t x} → t ∋ x → s ∙ t ∋ x

  data Ty (X : Set) : Set where
    base : X → Ty X
    _→ᵗ_ : (A B : Ty X) → Ty X

  private
    variable
      X Y : Set
      A B : Ty _

  module Names (N : Set) (_≟_ : DecidableEquality N) where

    Ctx : Set → Set
    Ctx X = N → Tree (Ty X)

    [] : Ctx X
    [] _ = ε

    record Var (Γ : Ctx X) (A : Ty X) : Set where
      constructor _#_
      field
        name : N
        index : Γ name ∋ A
    open Var public

    infixl 5 _-,_

    _-,_ : Ctx X → N × Ty X → Ctx X
    (Γ -, (n , A)) m = if does (m ≟ n) then Γ m ∙ [ A ] else Γ m

    module _ (Const : Ty X → Set) where

      data Tm (Γ : Ctx X) : Ty X → Set where
        const : (c : Const A) → Tm Γ A
        var : (v : Var Γ A) → Tm Γ A
        lam : (n : N) (M : Tm (Γ -, (n , A)) B) → Tm Γ (A →ᵗ B)
        app : (M : Tm Γ (A →ᵗ B)) (N : Tm Γ A) → Tm Γ B

      record Kit (T : Ctx X → Ty X → Set) : Set where
        field
          wk : ∀ {Γ n A B} → T Γ B → T (Γ -, (n , A)) B
          vr : ∀ {Γ A} → Var Γ A → T Γ A
          tm : ∀ {Γ A} → T Γ A → Tm Γ A

        Env : (Γ Δ : Ctx X) → Set
        Env Γ Δ = ∀ {A} → Var {X} Δ A → T Γ A

        bind : ∀ {Γ Δ} → Env Γ Δ → ∀ {n A} → Env (Γ -, (n , A)) (Δ -, (n , A))
        bind ρ {n} (m # i) with does (m ≟ n) | inspect does (m ≟ n)
        ... | false | _ = wk (ρ (m # i))
        bind ρ {n} (m # ↙ i) | true | _ = wk (ρ (m # i))
        bind {Γ} ρ {n} {A} {B} (m # ↘ i) | true | [ eq ] = vr (m # ↘i)
          where
          ↘i : (Γ -, (n , A)) m ∋ B
          ↘i rewrite eq = ↘ i

        trav : ∀ {Γ Δ} → Env Γ Δ → (∀ {A} → Tm Δ A → Tm Γ A)
        trav ρ (const c) = const c
        trav ρ (var v) = tm (ρ v)
        trav ρ (lam n M) = lam n (trav (bind ρ) M)
        trav ρ (app M N) = app (trav ρ M) (trav ρ N)

        infixl 5 _-e,_

        _-e,_ : ∀ {Γ Δ n A} → Env Γ Δ → T Γ A → Env Γ (Δ -, (n , A))
        _-e,_ {n = n} ρ N (m # i) with does (m ≟ n)
        ... | false = ρ (m # i)
        _-e,_ {n = n} ρ N (m # ↙ i) | true = ρ (m # i)
        _-e,_ {n = n} ρ N (m # ↘ here) | true = N

      wkVar : ∀ {Γ : Ctx X} {n A B} → Var Γ B → Var (Γ -, (n , A)) B
      wkVar v .name = v .name
      wkVar {n = n} (m # i) .index with does (m ≟ n)
      ... | false = i
      ... | true = ↙ i

      module _ where
        open Kit

        kitVar : Kit Var
        kitVar .wk = wkVar
        kitVar .vr = id
        kitVar .tm = var

        kitTm : Kit Tm
        kitTm .wk = trav kitVar wkVar
        kitTm .vr = var
        kitTm .tm = id

      singleSubst : ∀ {Γ n A B} → Tm (Γ -, (n , A)) B → Tm Γ A → Tm Γ B
      singleSubst M N = trav (vr -e, N) M
        where open Kit kitTm

      -- Refer to the latest-bound x.
      pattern var# x = var (x # ↘ here)

  module Examples {O} (Const : Ty O → Set) where

    open import Data.String as Str
    open Names String Str._≟_

    K : ∀ {X Y} → Tm Const [] (base X →ᵗ base Y →ᵗ base X)
    K = lam "x" (lam "y" (var# "x"))

    silly : ∀ {X Y} →
            Tm Const [] (((base X →ᵗ base X) →ᵗ base Y) →ᵗ base Y)
    silly = lam "x" (app (var# "x") (lam "x" (var# "x")))