用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

在样式这里中，我希望能够像

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

哪里

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

将vt替换为ct。注意，我希望将值类型替换为计算类型。我能够使用标准库将VTypes替换为VTypes，而不能将VTypes替换为CTypes，如上面所示。我这样做，使用Data.Fin.Substitution (请参阅这里)：

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

您可以在Application的情况下打开CType，而不是打开看起来不合适的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 σ

整个代码。

要理解标准库中的内容，您需要阅读保持类型的重命名和替换论文。不过，stdlib中的代码更抽象。

顺便说一下，您可以使用保序嵌入来定义重命名，也可以使用重命名来定义替换。把洞填好这里。