Variant of Parametric Higher-Order Abstract Syntax where each binder binds a type.

PHOAS.agda

{-# OPTIONS --overlapping-instances --instance-search-depth=10 #-}

module PHOAS where

open import Agda.Primitive

record Weakening1 {ℓ₁} {ℓ₂} (V : Set ℓ₁) (V' : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  field weaken : V → V'
record Weakening {ℓ₁} {ℓ₂} (V : Set ℓ₁) (V' : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  field weaken : V → V'

instance
  weakening0 : ∀ {ℓ} {V : Set ℓ} → Weakening V V
  weakening0 .Weakening.weaken v = v
  weakeningSuc : ∀ {ℓ₁} {ℓ₂} {ℓ₃} {V : Set ℓ₁} {V' : Set ℓ₂} {V'' : Set ℓ₃} → ⦃ Weakening1 V V' ⦄ → ⦃ Weakening V' V'' ⦄ → Weakening V V''
  weakeningSuc ⦃ weak1 ⦄ ⦃ weak ⦄ .Weakening.weaken v = weak .Weakening.weaken (weak1 .Weakening1.weaken v)

data Term {ℓ} (V : Set ℓ) : Set (lsuc ℓ) where
  Var : V → Term V
  App : Term V → Term V → Term V
  Lam : ({V' : Set ℓ} → ⦃ Weakening1 V V' ⦄ → V' → Term V') → Term V

var : ∀ {ℓ₁} {ℓ₂} {V : Set ℓ₁} {V' : Set ℓ₂} → ⦃ Weakening V V' ⦄ → V → Term V'
var ⦃ weak ⦄ v = Var (weak .Weakening.weaken v)

term-id : ∀ {ℓ} {V : Set ℓ} → Term V
term-id = Lam λ x → var x

map : ∀ {ℓ} {V : Set ℓ} {V' : Set ℓ} → (V → V') → Term V → Term V'
map g (Var x) = Var (g x)
map g (App f a) = App (map g f) (map g a)
map {ℓ} {V} {V'} g (Lam b) = Lam λ x → b x
  where instance
    weak' : {V'' : Set ℓ} → ⦃ Weakening1 V' V'' ⦄ → Weakening1 V V''
    weak' ⦃ weak ⦄ .Weakening1.weaken v = weak .Weakening1.weaken (g v)

collapse : ∀ {ℓ} {V : Set ℓ} → Term (Term V) → Term V
collapse (Var t) = t
collapse (App f a) = App (collapse f) (collapse a)
collapse {ℓ} {V} (Lam b) = Lam λ x → collapse (b (Var x))
  where instance
    weak' : {V' : Set ℓ} → ⦃ Weakening1 V V' ⦄ → Weakening1 (Term V) (Term V')
    weak' ⦃ weak ⦄ .Weakening1.weaken = map (weak .Weakening1.weaken)

data Extend {ℓ} (V : Set ℓ) : Set ℓ where
  here : Extend V
  later : V → Extend V
data TermIdx {ℓ} (V : Set ℓ) : Set ℓ where
  VarIdx : V → TermIdx V
  AppIdx : TermIdx V → TermIdx V → TermIdx V
  LamIdx : TermIdx (Extend V) → TermIdx V

mapIdx : ∀ {ℓ ℓ'} {V : Set ℓ} {V' : Set ℓ'} → (V → V') → TermIdx V → TermIdx V'
mapIdx g (VarIdx x) = VarIdx (g x)
mapIdx g (AppIdx f a) = AppIdx (mapIdx g f) (mapIdx g a)
mapIdx g (LamIdx b) = LamIdx (mapIdx (λ{
    here → here;
    (later x) → later (g x)
  }) b)

toIdx : ∀ {ℓ} {V : Set ℓ} → Term V → TermIdx V
toIdx (Var x) = VarIdx x
toIdx (App f a) = AppIdx (toIdx f) (toIdx a)
toIdx {V = V} (Lam b) = LamIdx (toIdx (b here))
  where instance
    weak' : Weakening1 V (Extend V)
    weak' .Weakening1.weaken = later

fromIdx : ∀ {ℓ} {V : Set ℓ} → TermIdx V → Term V
fromIdx (VarIdx x) = Var x
fromIdx (AppIdx f a) = App (fromIdx f) (fromIdx a)
fromIdx (LamIdx b) = Lam λ ⦃ weak ⦄ x → map (λ{
    here → x;
    (later y) → weak .Weakening1.weaken y
  }) (fromIdx b)

record Lift {ℓ} ℓ' (A : Set ℓ) : Set (ℓ ⊔ ℓ') where
  field elem : A
lift-Term : ∀ {ℓ} ℓ' {V : Set ℓ} → Term V → Term (Lift ℓ' V)
lift-Term ℓ' t = fromIdx (mapIdx (λ v → record { elem = v }) (toIdx t))

beta : ∀ {ℓ} {V : Set ℓ} → Term V → Term V
beta (Var x) = Var x
beta {ℓ} {V} (App f a) with (lift-Term (lsuc ℓ) f)
... | Lam b = collapse (b a)
  where instance
    weak' : Weakening1 (Lift (lsuc ℓ) V) (Term V)
    weak' .Weakening1.weaken x = Var (x .Lift.elem)
... | _ = App (beta f) (beta a)
beta (Lam b) = Lam λ x → beta (b x)

introIdx : ∀ {ℓ} {V : Set ℓ} → ({V' : Set ℓ} → ⦃ Weakening1 V V' ⦄ → V' → TermIdx V') → TermIdx (Extend V)
introIdx {V = V} b = b here
  where instance
    weak' : Weakening1 V (Extend V)
    weak' .Weakening1.weaken = later

openIdx : ∀ {ℓ ℓ'} {V : Set ℓ} → TermIdx (Extend V) → {V' : Set ℓ'} → ⦃ Weakening1 V V' ⦄ → V' → TermIdx V'
openIdx {ℓ} {ℓ'} {V} t {V'} ⦃ weak ⦄ x = mapIdx (λ{
    here → x;
    (later y) → weak .Weakening1.weaken y
  }) t

{-# TERMINATING #-}
collapseIdx : ∀ {ℓ} {V : Set ℓ} → TermIdx (TermIdx V) → TermIdx V
collapseIdx (VarIdx t) = t
collapseIdx (AppIdx f a) = AppIdx (collapseIdx f) (collapseIdx a)
collapseIdx (LamIdx b) = LamIdx (collapseIdx (mapIdx (λ{
    here → VarIdx here;
    (later t) → mapIdx later t
  }) b))

betaIdx : ∀ {ℓ} {V : Set ℓ} → TermIdx V → TermIdx V
betaIdx (VarIdx x) = VarIdx x
betaIdx {V = V} (AppIdx (LamIdx b) a) = collapseIdx (openIdx b a)
  where instance
    weak' : Weakening1 V (TermIdx V)
    weak' .Weakening1.weaken = VarIdx
betaIdx (AppIdx f a) = AppIdx (betaIdx f) (betaIdx a)
betaIdx (LamIdx b) = LamIdx (betaIdx b)