<commit_before>---
title     : "TypedDB: Typed DeBruijn representation"
layout    : page
permalink : /TypedDB
---

## Imports

\begin{code}
module TypedDB where
\end{code}

\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Unit using (⊤; tt)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (map)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Nullary.Product using (_×-dec_)
\end{code}


## Syntax

\begin{code}
infixl 6 _,_
infix  4 _⊢_
infix  4 _∋_
infixr 5 _⇒_
infixl 5 _·_
infix  6 S_
infix  4 ƛ_

data Type : Set where
  o   : Type
  _⇒_ : Type → Type → Type

data Env : Set where
  ε   : Env
  _,_ : Env → Type → Env

data _∋_ : Env → Type → Set where

  Z : ∀ {Γ} {A} →
    ------------
    Γ , A ∋ A

  S_ : ∀ {Γ} {A B} →
    Γ ∋ A →
    -----------
    Γ , B ∋ A

data _⊢_ : Env → Type → Set where

  ⌊_⌋ : ∀ {Γ} {A} →
    Γ ∋ A →
    -------
    Γ ⊢ A

  ƛ_  :  ∀ {Γ} {A B} →
    Γ , A ⊢ B →
    ------------
    Γ ⊢ A ⇒ B

  _·_ : ∀ {Γ} {A B} →
    Γ ⊢ A ⇒ B →
    Γ ⊢ A →
    ------------
    Γ ⊢ B
\end{code}

## Decide whether environments and types are equal

\begin{code}
_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
o ≟T o = yes refl
o ≟T (A′ ⇒ B′) = no (λ())
(A ⇒ B) ≟T o = no (λ())
(A ⇒ B) ≟T (A′ ⇒ B′) = map (equivalence obv1 obv2) ((A ≟T A′) ×-dec (B ≟T B′))
  where
  obv1 : ∀ {A B A′ B′ : Type} → (A ≡ A′) × (B ≡ B′) → A ⇒ B ≡ A′ ⇒ B′
  obv1 ⟨ refl , refl ⟩ = refl
  obv2 : ∀ {A B A′ B′ : Type} → A ⇒ B ≡ A′ ⇒ B′ → (A ≡ A′) × (B ≡ B′)
  obv2 refl = ⟨ refl , refl ⟩

_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
ε ≟ ε = yes refl
ε ≟ (Γ , A) = no (λ())
(Γ , A) ≟ ε = no (λ())
(Γ , A) ≟ (Δ , B) = map (equivalence obv1 obv2) ((Γ ≟ Δ) ×-dec (A ≟T B))
  where
  obv1 : ∀ {Γ Δ A B} → (Γ ≡ Δ) × (A ≡ B) → (Γ , A) ≡ (Δ , B)
  obv1 ⟨ refl , refl ⟩ = refl
  obv2 : ∀ {Γ Δ A B} → (Γ , A) ≡ (Δ , B) → (Γ ≡ Δ) × (A ≡ B)
  obv2 refl = ⟨ refl , refl ⟩
\end{code}


## Writing variables as naturals

This turned out to be a lot harder than expected. Probably not a good idea.

\begin{code}
postulate
  impossible : ⊥

conv : ∀ {Γ} {A} → ℕ → Γ ∋ A
conv {ε} = ⊥-elim impossible
conv {Γ , B} (suc n) = S (conv n)
conv {Γ , A} {B} zero with A ≟T B
...                   | yes refl  =  Z
...                   | no  A≢B   =  ⊥-elim impossible

var : ∀ {Γ} {A} → ℕ → Γ ⊢ A
var n  =  ⌊ conv n ⌋
\end{code}

## Test examples

\begin{code}
Ch : Type
Ch = (o ⇒ o) ⇒ o ⇒ o

plus : ∀ {Γ} → Γ ⊢ Ch ⇒ Ch ⇒ Ch
plus = ƛ ƛ ƛ ƛ ⌊ S S S Z ⌋ · ⌊ S Z ⌋ · (⌊ S S Z ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋)

two : ∀ {Γ} → Γ ⊢ Ch
two = ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)

four : ∀ {Γ} → Γ ⊢ Ch
four = ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)))

four′ : ∀ {Γ} → Γ ⊢ Ch
four′ = plus · two · two
\end{code}

# Denotational semantics

\begin{code}
⟦_⟧ᵀ : Type → Set
⟦ o ⟧ᵀ      =  ℕ
⟦ A ⇒ B ⟧ᵀ  =  ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ

⟦_⟧ᴱ : Env → Set
⟦ ε ⟧ᴱ      =  ⊤
⟦ Γ , A ⟧ᴱ  =  ⟦ Γ ⟧ᴱ × ⟦ A ⟧ᵀ

⟦_⟧ⱽ : ∀ {Γ : Env} {A : Type} → Γ ∋ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
⟦ Z ⟧ⱽ   ⟨ ρ , v ⟩ = v
⟦ S n ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ n ⟧ⱽ ρ

⟦_⟧ : ∀ {Γ : Env} {A : Type} → Γ ⊢ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
⟦ ⌊ n ⌋ ⟧ ρ  =  ⟦ n ⟧ⱽ ρ
⟦ ƛ N   ⟧ ρ  =  λ{ v → ⟦ N ⟧ ⟨ ρ , v ⟩ }
⟦ L · M ⟧ ρ  =  (⟦ L ⟧ ρ) (⟦ M ⟧ ρ)

_ : ⟦ four ⟧ tt ≡ ⟦ four′ ⟧ tt
_ = refl

_ : ⟦ four ⟧ tt suc zero ≡ 4
_ = refl
\end{code}

## Operational semantics - with simultaneous substitution, a la McBride

## Renaming

\begin{code}
ext∋ : ∀ {Γ Δ} {B} → (∀ {A} → Γ ∋ A → Δ ∋ A) → Δ ∋ B → (∀ {A} → Γ , B ∋ A → Δ ∋ A)
ext∋ ρ j Z      =  j
ext∋ ρ j (S k)  =  ρ k

rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (⌊ n ⌋)  =  ⌊ ρ n ⌋
rename ρ (ƛ N)    =  ƛ (rename (ext∋ (S_ ∘ ρ) Z) N)
rename ρ (L · M)  =  (rename ρ L) · (rename ρ M)
\end{code}

## Substitution

\begin{code}
ext⊢ : ∀ {Γ Δ} {B} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → Δ ⊢ B → (∀ {A} → Γ , B ∋ A → Δ ⊢ A)
ext⊢ ρ M Z      =  M
ext⊢ ρ M (S k)  =  ρ k

subst : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
subst ρ (⌊ n ⌋)  =  ρ n
subst ρ (ƛ N)    =  ƛ (subst (ext⊢ (rename S_ ∘ ρ) ⌊ Z ⌋) N)
subst ρ (L · M)  =  (subst ρ L) · (subst ρ M)

substitute : ∀ {Γ} {A B} → Γ , A ⊢ B → Γ ⊢ A → Γ ⊢ B
substitute N M =  subst (ext⊢ ⌊_⌋ M) N 
\end{code}

## Normal

\begin{code}
data Normal  : ∀ {Γ} {A} → Γ ⊢ A → Set
data Neutral : ∀ {Γ} {A} → Γ ⊢ A → Set

data Normal where
  ƛ_  : ∀ {Γ} {A B} {N : Γ , A ⊢ B} → Normal N → Normal (ƛ N)
  ⌈_⌉ : ∀ {Γ} {A} {M : Γ ⊢ A} → Neutral M → Normal M

data Neutral where
  ⌊_⌋   : ∀ {Γ} {A} → (n : Γ ∋ A) → Neutral ⌊ n ⌋
  _·_  : ∀ {Γ} {A B} → {L : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} → Neutral L → Normal M → Neutral (L · M)
\end{code}

## Reduction step

\begin{code}
infix 2 _⟶_

data _⟶_ : ∀ {Γ} {A} → Γ ⊢ A → Γ ⊢ A → Set where
<commit_msg>got rid of ext in TypedDB<commit_after>---
title     : "TypedDB: Typed DeBruijn representation"
layout    : page
permalink : /TypedDB
---

## Imports

\begin{code}
module TypedDB where
\end{code}

\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Unit using (⊤; tt)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (map)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Nullary.Product using (_×-dec_)
\end{code}


## Syntax

\begin{code}
infixl 6 _,_
infix  4 _⊢_
infix  4 _∋_
infixr 5 _⇒_
infixl 5 _·_
infix  6 S_
infix  4 ƛ_

data Type : Set where
  o   : Type
  _⇒_ : Type → Type → Type

data Env : Set where
  ε   : Env
  _,_ : Env → Type → Env

data _∋_ : Env → Type → Set where

  Z : ∀ {Γ} {A} →
    ------------
    Γ , A ∋ A

  S_ : ∀ {Γ} {A B} →
    Γ ∋ B →
    -----------
    Γ , A ∋ B

data _⊢_ : Env → Type → Set where

  ⌊_⌋ : ∀ {Γ} {A} →
    Γ ∋ A →
    -------
    Γ ⊢ A

  ƛ_  :  ∀ {Γ} {A B} →
    Γ , A ⊢ B →
    ------------
    Γ ⊢ A ⇒ B

  _·_ : ∀ {Γ} {A B} →
    Γ ⊢ A ⇒ B →
    Γ ⊢ A →
    ------------
    Γ ⊢ B
\end{code}

## Decide whether environments and types are equal

\begin{code}
_≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
o ≟T o = yes refl
o ≟T (A′ ⇒ B′) = no (λ())
(A ⇒ B) ≟T o = no (λ())
(A ⇒ B) ≟T (A′ ⇒ B′) = map (equivalence obv1 obv2) ((A ≟T A′) ×-dec (B ≟T B′))
  where
  obv1 : ∀ {A B A′ B′ : Type} → (A ≡ A′) × (B ≡ B′) → A ⇒ B ≡ A′ ⇒ B′
  obv1 ⟨ refl , refl ⟩ = refl
  obv2 : ∀ {A B A′ B′ : Type} → A ⇒ B ≡ A′ ⇒ B′ → (A ≡ A′) × (B ≡ B′)
  obv2 refl = ⟨ refl , refl ⟩

_≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
ε ≟ ε = yes refl
ε ≟ (Γ , A) = no (λ())
(Γ , A) ≟ ε = no (λ())
(Γ , A) ≟ (Δ , B) = map (equivalence obv1 obv2) ((Γ ≟ Δ) ×-dec (A ≟T B))
  where
  obv1 : ∀ {Γ Δ A B} → (Γ ≡ Δ) × (A ≡ B) → (Γ , A) ≡ (Δ , B)
  obv1 ⟨ refl , refl ⟩ = refl
  obv2 : ∀ {Γ Δ A B} → (Γ , A) ≡ (Δ , B) → (Γ ≡ Δ) × (A ≡ B)
  obv2 refl = ⟨ refl , refl ⟩
\end{code}


## Writing variables as naturals

This turned out to be a lot harder than expected. Probably not a good idea.

\begin{code}
postulate
  impossible : ⊥

conv : ∀ {Γ} {A} → ℕ → Γ ∋ A
conv {ε} = ⊥-elim impossible
conv {Γ , B} (suc n) = S (conv n)
conv {Γ , A} {B} zero with A ≟T B
...                   | yes refl  =  Z
...                   | no  A≢B   =  ⊥-elim impossible

var : ∀ {Γ} {A} → ℕ → Γ ⊢ A
var n  =  ⌊ conv n ⌋
\end{code}

## Test examples

\begin{code}
Ch : Type
Ch = (o ⇒ o) ⇒ o ⇒ o

plus : ∀ {Γ} → Γ ⊢ Ch ⇒ Ch ⇒ Ch
plus = ƛ ƛ ƛ ƛ ⌊ S S S Z ⌋ · ⌊ S Z ⌋ · (⌊ S S Z ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋)

two : ∀ {Γ} → Γ ⊢ Ch
two = ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)

four : ∀ {Γ} → Γ ⊢ Ch
four = ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)))

four′ : ∀ {Γ} → Γ ⊢ Ch
four′ = plus · two · two
\end{code}

# Denotational semantics

\begin{code}
⟦_⟧ᵀ : Type → Set
⟦ o ⟧ᵀ      =  ℕ
⟦ A ⇒ B ⟧ᵀ  =  ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ

⟦_⟧ᴱ : Env → Set
⟦ ε ⟧ᴱ      =  ⊤
⟦ Γ , A ⟧ᴱ  =  ⟦ Γ ⟧ᴱ × ⟦ A ⟧ᵀ

⟦_⟧ⱽ : ∀ {Γ : Env} {A : Type} → Γ ∋ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
⟦ Z ⟧ⱽ   ⟨ ρ , v ⟩ = v
⟦ S n ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ n ⟧ⱽ ρ

⟦_⟧ : ∀ {Γ : Env} {A : Type} → Γ ⊢ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
⟦ ⌊ n ⌋ ⟧ ρ  =  ⟦ n ⟧ⱽ ρ
⟦ ƛ N   ⟧ ρ  =  λ{ v → ⟦ N ⟧ ⟨ ρ , v ⟩ }
⟦ L · M ⟧ ρ  =  (⟦ L ⟧ ρ) (⟦ M ⟧ ρ)

_ : ⟦ four ⟧ tt ≡ ⟦ four′ ⟧ tt
_ = refl

_ : ⟦ four ⟧ tt suc zero ≡ 4
_ = refl
\end{code}

## Operational semantics - with simultaneous substitution, a la McBride

## Renaming

\begin{code}
rename : ∀ {Γ Δ} → (∀ {B} → Γ ∋ B → Δ ∋ B) → (∀ {B} → Γ ⊢ B → Δ ⊢ B)
rename ρ (⌊ n ⌋)                   =  ⌊ ρ n ⌋
rename {Γ} {Δ} ρ (ƛ_ {A = A} N)    =  ƛ (rename ρ′ N)
  where
  ρ′ : ∀ {B} → Γ , A ∋ B → Δ , A ∋ B
  ρ′ Z      =  Z
  ρ′ (S k)  =  S (ρ k)
rename ρ (L · M)                   =  (rename ρ L) · (rename ρ M)
\end{code}

## Substitution

\begin{code}
subst : ∀ {Γ Δ} → (∀ {B} → Γ ∋ B → Δ ⊢ B) → (∀ {B} → Γ ⊢ B → Δ ⊢ B)
subst ρ (⌊ k ⌋)                   =  ρ k
subst {Γ} {Δ} ρ (ƛ_ {A = A} N)    =  ƛ (subst ρ′ N)
  where
  ρ′ : ∀ {B} → Γ , A ∋ B → Δ , A ⊢ B
  ρ′ Z      =  ⌊ Z ⌋
  ρ′ (S k)  =  rename S_ (ρ k)
subst ρ (L · M)                   =  (subst ρ L) · (subst ρ M)

substitute : ∀ {Γ A B} → Γ , A ⊢ B → Γ ⊢ A → Γ ⊢ B
substitute {Γ} {A} {B} N M =  subst ρ N
  where
  ρ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
  ρ Z      =  M
  ρ (S k)  =  ⌊ k ⌋
\end{code}

## Normal

\begin{code}
data Normal  : ∀ {Γ} {A} → Γ ⊢ A → Set
data Neutral : ∀ {Γ} {A} → Γ ⊢ A → Set

data Normal where
  ƛ_  : ∀ {Γ} {A B} {N : Γ , A ⊢ B} → Normal N → Normal (ƛ N)
  ⌈_⌉ : ∀ {Γ} {A} {M : Γ ⊢ A} → Neutral M → Normal M

data Neutral where
  ⌊_⌋   : ∀ {Γ} {A} → (n : Γ ∋ A) → Neutral ⌊ n ⌋
  _·_  : ∀ {Γ} {A B} → {L : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} → Neutral L → Normal M → Neutral (L · M)
\end{code}

## Reduction step

\begin{code}
infix 2 _⟶_

data _⟶_ : ∀ {Γ} {A} → Γ ⊢ A → Γ ⊢ A → Set where

{'fraction_non_alphanumeric': 0.21194414182430424, 'fraction_numerical': 0.0041596513815984944, 'mean_word_length': 1.8509316770186335, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 35, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2438062', 'n_tokens_mistral': 6362, 'n_tokens_neox': 5965, 'n_words': 2320}