dannypsnl · September 29, 2025 18:49 · Sep 28, 2025
diff --git a/EasierIndices.agda b/EasierIndices.agda
@@ -0,0 +1,187 @@
+{-
+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))