使用 Agda 的标准库 Data.Fin.Substitution 处理相互定义类型的替换

Question

我正在尝试在 Agda 中使用等递归类型对按推值调用 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 ] = ?

post-将vt代入ct。请注意，我想将值类型替换为计算类型。我可以使用标准库将 VTypes 替换为 VTypes，但不能像上面那样将 VTypes 替换为 CTypes。我这样做，使用 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 转到 VType 或 CType，但这似乎不起作用或导致终止如果我尝试模仿标准库的模块，检查问题。

有谁知道是否可以使用标准库中的 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 to define renaming and renaming to define substitution. Fill the holes here.

使用 Agda 的标准库 Data.Fin.Substitution 处理相互定义类型的替换

Handling substitutions of mutually defined types with Agda's standard library's Data.Fin.Substitution

substitution

agda