A new syntax tree definition that writes like HOAS, but behaves like de Bruijn

main.agda

-- This construction comes from the paper
--  Contextual Embeddings: Implementing Bound Variables through Instance Resolution
-- https://dl.acm.org/doi/10.1145/3808269

-- I made some improvements specific to Agda.

module _ where
open import Data.Product using (Σ; proj₁; proj₂) renaming (_,_ to _&_)
open import Relation.Binary.PropositionalEquality

-- We define the simple types
data Ty : Set where
  𝕠 : Ty
  _⇒_ _×_ : Ty → Ty → Ty

infixl 5 _×_
infixr 4 _⇒_

variable
  σ τ : Ty

-- A context is a list of types, as usual
data Ctx : Set where
  ∅ : Ctx
  _,_ : Ctx → Ty → Ctx

infixl 3 _,_

variable
  Γ Γ' Δ : Ctx

-- A phantom variable: it carries no information except at type level
-- to provide Γ and τ to the instance resolution
record PhVar (Γ : Ctx) (τ : Ty) : Set where
  constructor ⋆

-- To compute the de Bruijn index, we simply need to
-- compare the lengths of the contexts at binding vs use site.
-- This is the computational data of Prefix
data Prefix : Ctx → Ctx → Set where
  instance id : Prefix Γ Γ
  _,_ : Prefix Γ Δ → (τ : Ty) → Prefix Γ (Δ , τ)
{-# OVERLAPPING id #-}

data _~_,_ : Ctx → Ctx → Ty → Set where
  instance obvie : (Δ , τ) ~ Δ , τ

-- This instance (instead of the _,_ constructor) is friendlier to
-- instance search, avoiding backtracking (because id is strictly more
-- specific than the cons instance, thus allowing overlap).
instance
  cons : ⦃ Prefix Γ Δ ⦄ → ⦃ Γ' ~ Δ , τ ⦄ → Prefix Γ Γ'
  cons ⦃ prfx ⦄ ⦃ obvie ⦄ = prfx , _

-- ! The definition of terms.
-- Stripping away the irrelevant PhVar types, this is simply de Bruijn indices.
-- But ignoring the instance arguments, this looks exactly like HOAS,
-- thus we reap the benefits of both.
data Term : Ctx → Ty → Set where
  var : Prefix (Γ , τ) Δ → PhVar Γ τ → Term Δ τ
  lam : (PhVar Γ τ → Term (Γ , τ) σ)
    → Term Γ (τ ⇒ σ)
  app : Term Γ (τ ⇒ σ) → Term Γ τ → Term Γ σ

#_ : ⦃ Prefix (Γ , τ) Δ ⦄ → PhVar Γ τ → Term Δ τ
#_ ⦃ prfx ⦄ v = var prfx v

syntax lam (λ x → t) = ƛ x ⇒ t
syntax app s t = s ∙ t
infixr 4 lam
infixl 5 app
infix 99 #_

-- For example, you can write this!
K : Term ∅ (τ ⇒ σ ⇒ τ)
K = ƛ x ⇒ ƛ y ⇒ # x
-- If you replace var x with var y, you get
--   σ !=< τ of type Ty
-- which is a very understandable error message!

twice : Term ∅ ((𝕠 ⇒ 𝕠) ⇒ (𝕠 ⇒ 𝕠))
twice = ƛ f ⇒ ƛ x ⇒ # f ∙ (# f ∙ # x)

-- We next define the traditional dbi syntax and prove isomorphism
data Var' : Ctx → Ty → Set where
  zero : Var' (Γ , τ) τ
  suc : Var' Γ τ → Var' (Γ , σ) τ

data Term' : Ctx → Ty → Set where
  var : Var' Γ τ → Term' Γ τ
  lam : Term' (Γ , τ) σ
    → Term' Γ (τ ⇒ σ)
  app : Term' Γ (τ ⇒ σ) → Term' Γ τ → Term' Γ σ

Prefix→Var' : Prefix (Γ , τ) Δ → Var' Δ τ
Prefix→Var' id = zero
Prefix→Var' (prfx , τ) = suc (Prefix→Var' prfx)

Var : Ctx → Ty → Set
Var Δ τ = Σ Ctx λ Γ → Prefix (Γ , τ) Δ

Var'→Var : Var' Γ τ → Var Γ τ
Var'→Var zero = _ & id
Var'→Var (suc i) = Var'→Var i .proj₁ & (Var'→Var i .proj₂ , _)

Var→Var'→Var : (v : Var Γ τ) → Var'→Var (Prefix→Var' (v .proj₂)) ≡ v
Var→Var'→Var (Δ & id) = refl
Var→Var'→Var (Δ & (prfx , τ)) rewrite Var→Var'→Var (Δ & prfx) = refl

Var'→Var→Var' : (v : Var' Γ τ) → Prefix→Var' (Var'→Var v .proj₂) ≡ v
Var'→Var→Var' zero = refl
Var'→Var→Var' (suc v) = cong suc (Var'→Var→Var' v)

Term→Term' : Term Γ τ → Term' Γ τ
Term→Term' (var prfx ⋆) = var (Prefix→Var' prfx)
Term→Term' (lam f) = lam (Term→Term' (f ⋆))
Term→Term' (app f t) = app (Term→Term' f) (Term→Term' t)

Term'→Term : Term' Γ τ → Term Γ τ
Term'→Term {Γ = Γ} (var x) = var (Var'→Var x .proj₂) _
Term'→Term (lam f) = lam λ _ → Term'→Term f
Term'→Term (app f t) = app (Term'→Term f) (Term'→Term t)

Term→Term'→Term : (t : Term Γ τ) → Term'→Term (Term→Term' t) ≡ t
Term→Term'→Term (var prfx ⋆) = cong
  (λ v → var {v .proj₁} (v .proj₂) ⋆)
  (Var→Var'→Var (_ & prfx))
Term→Term'→Term (lam f) = cong (λ u → lam λ _ → u) (Term→Term'→Term (f ⋆))
Term→Term'→Term (app f t) = cong₂ app (Term→Term'→Term f) (Term→Term'→Term t)

Term'→Term→Term' : (t : Term' Γ τ) → Term→Term' (Term'→Term t) ≡ t
Term'→Term→Term' (var i) = cong var ((Var'→Var→Var' i))
Term'→Term→Term' (lam f) = cong lam (Term'→Term→Term' f)
Term'→Term→Term' (app f t) = cong₂ app (Term'→Term→Term' f) (Term'→Term→Term' t)