logic - 在 Agda 中制定依赖类型系统

Question

如何在 Agda 中制定依赖类型的逻辑，而不是通过重新使用 Agda 类型系统本身来“作弊”？

我可以很容易地定义一个独立类型的逻辑:

infixr 5 _⇒_
data Type : Set where
    _⇒_ : Type → Type → Type

infix 4 _⊢_
data _⊢_ : List Type → Type → Set where
    var : {a : Type} → [ a ] ⊢ a
    λ'  : {a b : Type} {γ : _} → a ∷ γ ⊢ b → γ ⊢ a ⇒ b
    ply : {a b : Type} {γ δ : _} → γ ⊢ a ⇒ b → δ ⊢ a → γ ++ δ ⊢ b
    weak : {a b : Type} {γ : _} → γ ⊢ b → a ∷ γ ⊢ b
    cntr : {a b : Type} {γ : _} → a ∷ a ∷ γ ⊢ b → a ∷ γ ⊢ b
    xchg : {a : Type} {γ δ : _} → γ ↭ δ → γ ⊢ a → δ ⊢ a

我也可以大致按照LambdaPi Haskell 中依赖类型 λ 演算的教程实现。但它是隐式类型的，不像我的 Agda 代码，我什至不知道从哪里开始修改我的代码，因为到目前为止想到的路径导致无限倒退:

data _⊢_ : List (? ⊢ ?) → (? ⊢ ?) → Set where ...

Google 搜索“embedding dependent types in Agda”之类的内容只会返回 in Agda 中的依赖类型编程的匹配项...

Answer 1

我们在 Type Theory 中的 Type Theory 论文中已经做到了这一点，它实际上在 Agda 中进行了形式化。基本思想是您将上下文、类型、术语和替换定义为互归纳定义。我们只定义有类型的对象，所以我们永远不必定义无类型的东西或类型判断。类型是通过依赖定义的，例如类型依赖于上下文，术语依赖于类型和上下文。为了制定定义平等，我们使用同伦类型理论的思想并允许平等构造函数。这意味着我们必须公理化更高归纳类型的实例，或者成为精确的商归纳归纳类型。这应该很快就会在立方体 Agda 中开箱即用。

http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf

@article{altenkirch2016type,
  title={Type theory in type theory using quotient inductive types},
  author={Altenkirch, Thorsten and Kaposi, Ambrus},
  journal={ACM SIGPLAN Notices},
  volume={51},
  number={1},
  pages={18--29},
  year={2016},
  publisher={ACM}
}