Skip to content

Instantly share code, notes, and snippets.

@yangzhixuan

yangzhixuan/EasierIndices.agda

Created September 28, 2025 13:47
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save yangzhixuan/e5ddf138f073d4ea76706ccfa130a8b9 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save yangzhixuan/e5ddf138f073d4ea76706ccfa130a8b9 to your computer and use it in GitHub Desktop.
Download ZIP
Making working with de Brujin indices easier
Raw
EasierIndices.agda
{-
This file demonstrates a technique for making working with de Bruijn-indexed
terms easier that I learnt from the paper /The Linearity Monad/ by Jennifer
Paykin and Steve Zdancewic. After defining well-typed terms `Γ ⊢ τ` using de Bruijn
indices, we define an auxiliary function `lam` that takes in the variable term explicitly:
> lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V}
> → (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ)
> → (Γ , τ) ⊢ σ)
> → Γ ⊢ τ ⇒ σ
where `IsExt Δ (Γ , τ)` is a typeclass saying `Δ` is an extension of the context
`Γ , τ`, which can be automated resolved for instances such as `IsExt (Γ , τ) (Γ , τ)`,
`IsExt (Γ , τ , σ) (Γ , τ)`, etc.
With `lam`, we can build terms in a way similar to HOAS:
> K₁ : Γ ⊢ τ ⇒ (σ ⇒ τ)
> K₁ = lam (λ a → lam (λ b → a))
In the original, the embedded language is a linear one, but this technique is
very flexible and works with structural contexts too as shown here.
(Also, courtesy of Liang-Ting Chen for putting a formalisation of STLC
[online](https://flolac.iis.sinica.edu.tw/2022/Lambda-sol.agda), from which I
copied some basic definitions.)
-}
{-# OPTIONS --no-import-sorts #-}
open import Agda.Primitive
renaming (Set to Type; Setω to Typeω)
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
variable
A B C : Type
------------------------------------------------------------------------------
-- List over A
data List (A : Type) : Type where
[]
--------
: List A
_∷_
: (x : A) (xs : List A)
→ ---------------------
List A
infixr 5 _∷_
_,_ : List A → A → List A
xs , x = x ∷ xs
------------------------------------------------------------------------------
-- The memberhsip relation
variable
x y : A
xs ys : List A
data _∋_ {A : Type} : List A → A → Type where
zero
---------------------
: (x ∷ xs) ∋ x
suc
: xs ∋ x
→ -----------------------
(y ∷ xs) ∋ x
infix 4 _∋_
------------------------------------------------------------------------------
-- Types for STLC
data Ty (V : Type) : Type where
`_
: V
→ ---
Ty V
_⇒_
: (τ : Ty V) (σ : Ty V)
→ ---------------------
Ty V
-- Convention: τ₁ ⇒ τ₂ ⇒ ... τₙ ≡ τ₁ ⇒ (τ₂ ⇒ (... ⇒ τₙ))
infixr 7 _⇒_
------------------------------------------------------------------------------
-- Context in STLC
Cxt : Type → Type
Cxt V = List (Ty V)
variable
V : Type
τ σ : Ty V
Γ Δ : Cxt V
------------------------------------------------------------------------------
-- Intrinsically-typed de Bruijn representation of STLC
--
infix 4 _⊢_
data _⊢_ {V : Type} : Cxt V → Ty V → Type where
`_
: Γ ∋ τ
→ Γ ⊢ τ
-- \cdot
_·_
: Γ ⊢ (τ ⇒ σ)
→ Γ ⊢ τ
→ -------------
Γ ⊢ σ
-- \Gl-
ƛ_
: (Γ , τ) ⊢ σ
→ Γ ⊢ τ ⇒ σ
infixl 6 _·_ -- \cdot
infixr 5 ƛ_ -- \Gl
Ren : {V : Type} → Cxt V → Cxt V → Type
Ren {V} Γ Δ = {τ : Ty V} → Γ ∋ τ → Δ ∋ τ
ext : Ren Γ Δ → Ren (Γ , τ) (Δ , τ)
ext ρ zero = zero
ext ρ (suc x) = suc (ρ x)
rename
: {V : Type} {Γ Δ : Cxt V}
→ ({τ : Ty V} → Γ ∋ τ → Δ ∋ τ)
→ {τ : Ty V}
→ Γ ⊢ τ → Δ ⊢ τ
rename ρ (` x) = ` ρ x
rename ρ (M · N) = rename ρ M · rename ρ N
rename ρ (ƛ M) = ƛ rename (ext ρ) M
inc : Ren Γ (Γ , σ)
inc x = suc x
weaken : Γ ⊢ τ → (Γ , σ) ⊢ τ
weaken M = rename suc M
-- HOAS-like smart constructor for lambda abstraction
record IsExt {V : Type} (Δ Γ : Cxt V) : Type₁ where
field
applySub : {τ : Ty V} → Γ ⊢ τ → Δ ⊢ τ
open IsExt {{...}} public
instance
idExt : {V : Type} {Γ : Cxt V} → IsExt Γ Γ
idExt .applySub t = t
wkExt : {V : Type} {Γ : Cxt V} {τ : Ty V} → IsExt (Γ , τ) Γ
wkExt .applySub t = weaken t
lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V}
→ (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ)
→ (Γ , τ) ⊢ σ)
→ Γ ⊢ τ ⇒ σ
lam body = ƛ (body (applySub (` zero)))
syntax lam (λ x → t) = λ[ x ] t
-- Example terms
_ : Γ ⊢ τ ⇒ (σ ⇒ τ)
_ = lam (λ a → lam (λ b → a))
K₁ : Γ ⊢ τ ⇒ (σ ⇒ τ)
K₁ = λ[ a ] λ[ b ] a
I : Γ ⊢ τ ⇒ τ
I = λ[ x ] x
c₂ : Γ ⊢ (τ ⇒ τ) ⇒ τ ⇒ τ
c₂ = λ[ f ] λ[ x ] (f · (f · x))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment