使用Agda的標準庫的Data.Fin.Substitution處理替換相互定義的類型

Question

我想在Agda中使用isorecursive類型對push-value lambda演算進行編碼。因此，我用多達n個自由值類型變量（我只需要用等值遞歸類型替換值類型）來相互定義值類型和計算類型（這只是一個片段）。

data VType (n : ℕ) : Set where 
    vunit : VType n    -- unit type 
    var : Fin n → VType n  -- type variable 
    u  : CType n → VType n  -- thunk 
    μ : VType (1 + n) → VType n -- isorecursive type 

data CType (n : ℕ) : Set where 
    _⇒_ : VType n → CType n → CType n -- lambda abstraction 
    f : VType n → CType n   -- a value-producer 

在款式here，我希望能夠做到像換人

example : CType 0 
example = f (var (# 0)) C[/ vunit ] 

其中

_C[/_] : ∀ {n} → CType (1 + n) → VType n → CType n 
ct [/ vt ] = ? 

後的替代品vt到ct。注意我想將一個值類型替換爲一個計算類型。我可以使用標準庫將VType s代入VType s，但不能將VType s代入CType s，如上所述。我是這樣做的話，使用Data.Fin.Substitution（見here）：

module TypeSubst where 
    -- Following Data.Substitutions.Example 
    module TypeApp {T} (l : Lift T VType) where 
    open Lift l hiding (var) 

    -- Applies a substitution to a type 
    infixl 8 _/v_ 

    _/v_ : ∀ {m n} → VType m → Sub T m n → VType n 
    _/c_ : ∀ {m n} → CType m → Sub T m n → CType n 
    vunit /v ρ = vunit 
    (var x) /v ρ = lift (lookup x ρ) 
    (u σ) /v ρ = u (σ /c ρ) 
    (μ τ) /v ρ = μ (τ /v ρ ↑) 
    (σ ⇒ τ) /c ρ = σ /v ρ ⇒ τ /c ρ 
    f x /c ρ = f (x /v ρ) 

    open Application (record { _/_ = _/v_ }) using (_/✶_) 

    typeSubst : TermSubst VType 
    typeSubst = record { var = var; app = TypeApp._/v_ } 

    open TermSubst typeSubst public hiding (var) 

    weaken↑ : ∀ {n} → VType (1 + n) → VType (2 + n) 
    weaken↑ τ = τ/wk ↑ 

    infix 8 _[/_] 

    -- single type substitution 
    _[/_] : ∀ {n} → VType (1 + n) → VType n → VType n 
    τ [/ σ ] = τ/sub σ 

我試圖用一個新的數據類型Type工作：

data VorC : Set where 
    v : VorC 
    c : VorC 

data Type : VorC → ℕ → Set where 
    vtype : ∀ {n} → VType n → Type v n 
    ctype : ∀ {n} → CType n → Type c n 

我使用天然的解包功能從Type s到去嘗試到VType's或CType's，但這似乎不起作用或導致終止檢查問題，如果我嘗試模仿標準庫的模塊。

有誰知道是否可以使用標準庫中的Data.Fin.Substitution來完成這樣的事情？有人可以向我解釋這個模塊嗎？沒有關於這個的文檔......如果不可能爲此使用標準庫，任何關於如何解決這個問題的指針也是受歡迎的。謝謝！

Answer 1

您可以在CType的情況下打開Application而不是打開TermSubst，這看起來不合適（我不知道它有什麼問題）。這裏是相關部分：

typeSubst : TermSubst VType 
typeSubst = record { var = var; app = TypeApp._/v_ } 

open TermSubst typeSubst public hiding (var) 

module TypeSubst where 
    _[/v_] : ∀ {n} → VType (1 + n) → VType n → VType n 
    τ [/v σ ] = τ/sub σ 

open Application (record { _/_ = TypeApp._/c_ termLift }) renaming (_/_ to _/c_) using() 

_[/c_] : ∀ {n} → CType (1 + n) → VType n → CType n 
τ [/c σ ] = τ /c sub σ 

整個code。

要了解標準庫中發生了什麼，您需要閱讀Type-Preserving Renaming and Substitution論文。雖然，stdlib中的代碼更抽象。

順便說一句，您可以使用order preserving embeddings來定義重命名和重命名來定義替換。填充孔here。