在下面的 Agda 代码中，我有一个基于 de Bruijn 索引的术语语言。我可以以通常的 de Bruijn 索引方式定义对术语的替换，使用重命名以允许替换在活页夹下进行。
module Temp where
data Type : Set where
unit : Type
_⇾_ : Type → Type → Type
-- A context is a snoc-list of types.
data Cxt : Set where
ε : Cxt
_∷_ : Cxt → Type → Cxt
-- Context membership.
data _∈_ (τ : Type) : Cxt → Set where
here : ∀ {Γ} → τ ∈ Γ ∷ τ
there : ∀ {Γ τ′} → τ ∈ Γ → τ ∈ Γ ∷ τ′
infix 3 _∈_
data Term (Γ : Cxt) : Type → Set where
var : ∀ {τ} → τ ∈ Γ → Term Γ τ
〈〉 : Term Γ unit
fun : ∀ {τ₁ τ₂} → Term (Γ ∷ τ₁) τ₂ → Term Γ (τ₁ ⇾ τ₂)
-- A renaming from Γ to Γ′.
Ren : Cxt → Cxt → Set
Ren Γ Γ′ = ∀ {τ} → τ ∈ Γ → τ ∈ Γ′
extend′ : ∀ {Γ Γ′ τ′} → Ren Γ Γ′ → Ren (Γ ∷ τ′) (Γ′ ∷ τ′)
extend′ f here = here
extend′ f (there x) = there (f x)
-- Apply a renaming to a term.
_*′_ : ∀ {Γ Γ′ : Cxt} {τ} → Ren Γ Γ′ → Term Γ τ → Term Γ′ τ
f *′ var x = var (f x)
f *′ 〈〉 = 〈〉
f *′ fun e = fun (extend′ f *′ e)
-- A substitution from Γ to Γ′.
Sub : Cxt → Cxt → Set
Sub Γ Γ′ = ∀ {τ} → τ ∈ Γ → Term Γ′ τ
extend : ∀ {Γ Γ′ τ} → Sub Γ Γ′ → Sub (Γ ∷ τ) (Γ′ ∷ τ)
extend θ here = var here
extend θ (there x) = there *′ θ x
-- Apply a substitution to a term.
_*_ : ∀ {Γ Γ′ : Cxt} {τ} → Sub Γ Γ′ → Term Γ τ → Term Γ′ τ
θ * var x = θ x
θ * 〈〉 = 〈〉
θ * fun a = fun (extend θ * a)
我现在想做的是将类型泛化Term为多态变体，这样我就可以定义一个单子〉〉=操作并使用它来表达替换。这是天真的尝试：
data Term (A : Cxt → Type → Set) (Γ : Cxt) : Type → Set where
var : ∀ {τ} → A Γ τ → Term A Γ τ
〈〉 : Term A Γ unit
fun : ∀ {τ₁ τ₂} → Term A (Γ ∷ τ₁) τ₂ → Term A Γ (τ₁ ⇾ τ₂)
Sub : (Cxt → Type → Set) → Cxt → Cxt → Set
Sub A Γ Γ′ = ∀ {τ} → A Γ τ → Term A Γ′ τ
extend : ∀ {A : Cxt → Type → Set} {Γ Γ′ τ} → Sub A Γ Γ′ → Sub A (Γ ∷ τ) (Γ′ ∷ τ)
extend θ = {!!}
_〉〉=_ : ∀ {A : Cxt → Type → Set} {Γ Γ′ : Cxt} {τ} →
Term A Γ τ → Sub A Γ Γ′ → Term A Γ′ τ
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)
这里的问题是我不再知道如何定义extend（这将替换转换为更深的上下文），因为替换是一个更抽象的野兽。
根据Bernardy 和 Pouillard的论文Names for Free ，这里有更接近的内容：
module Temp2 where
open import Data.Unit
data _▹_ (A : Set) (V : Set) : Set where
here : V → A ▹ V
there : A → A ▹ V
data Term (A : Set) : Set where
var : A → Term A
〈〉 : Term A
fun : Term (A ▹ ⊤) → Term A
Ren : Set → Set → Set
Ren Γ Γ′ = Γ → Γ′
extend′ : ∀ {Γ Γ′ V : Set} → Ren Γ Γ′ → Ren (Γ ▹ V) (Γ′ ▹ V)
extend′ f (here x) = here x
extend′ f (there x) = there (f x)
Sub : Set → Set → Set
Sub Γ Γ′ = Γ → Term Γ′
_<$>_ : ∀ {Γ Γ′ : Set} → Ren Γ Γ′ → Term Γ → Term Γ′
f <$> var x = var (f x)
f <$> 〈〉 = 〈〉
f <$> fun e = fun (extend′ f <$> e)
extend : ∀ {Γ Γ′ V : Set} → Sub Γ Γ′ → Sub (Γ ▹ V) (Γ′ ▹ V)
extend θ (here x) = var (here x)
extend θ (there x) = there <$> θ x
_〉〉=_ : ∀ {Γ Γ′ : Set} → Term Γ → Sub Γ Γ′ → Term Γ′
var x 〉〉= θ = θ x
〈〉 〉〉= θ = 〈〉
fun a 〉〉= θ = fun (a 〉〉= extend θ)
The idea here is to model the idea of context extension in an explicitly abstract way, allowing extend to be defined for renamings and substitutions even in the polymorphic setting.
Unfortunately, I seem to be too stupid to understand how to extend this approach so that terms are parameterised by a Type, as they are in my first attempt above. I would like to end up with 〉〉= having (approximately) the following type:
_〉〉=_ : ∀ {Γ Γ′ : Set} {τ} → Term Γ τ → (Sub Γ Γ′) → Term Γ′ τ
Can anyone point me in the right direction?