3
在下面的Agda代碼中，我有一個基於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 θ)
這裏的想法是上下文擴展的想法模型在明確抽象的方式，讓extend爲的重命名加以界定和即使在多態環境中也是如此。
不幸的是，我似乎太愚蠢，無法理解如何擴展這種方法，以便通過Type對條款進行參數化，因爲它們在我上面的第一次嘗試中。我想最後>> =有（大約）以下類型：
_〉〉=_ : ∀ {Γ Γ′ : Set} {τ} → Term Γ τ → (Sub Γ Γ′) → Term Γ′ τ
任何人都可以指出我在正確的方向嗎？
幾秒鐘後，我以爲我迷失在數學。 –
''當你使用甚至你的瀏覽器無法顯示的字符時，你知道什麼是錯的... –
我以前有過這個問題，不幸的是我的瀏覽器似乎能夠顯示所有的字符！你在哪裏看到丟失的字符？ – Roly