在Agda中构建一个依赖类型系统

Question

在Agda中构建一个依赖类型系统

4

如何在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 ...

谷歌搜索 "在Agda中嵌入依赖类型" 等相关内容，只会返回与Agda中的依赖类型编程相关的结果...

- M Farkas-Dyck

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Thorsten Altenkirch · Accepted Answer

我们在“类型论中的类型论”一文中完成了这项工作，其实际形式化是在Agda中进行的。基本思路是将上下文、类型、项和替换定义为相互归纳的定义。我们只定义了有类型的对象，因此永远不必定义无类型的东西或类型判断。通过依赖性来定义类型，例如类型依赖于上下文，而术语依赖于类型和上下文。为了制定定义性等式，我们使用了同伦类型理论的想法，并允许等式构造器。这意味着我们必须公设高阶归纳类型的实例，或者更准确地说是商标归纳归纳类型。在 cubical 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}
}