3

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

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

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

谷歌搜索“在 Agda 中嵌入依赖类型”等仅返回在Agda 中的依赖类型编程的命中...

4

1 回答 1

4

我们在类型理论中的类型理论的论文中已经做到了这一点，该论文实际上是在 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}
}
于 2019-02-27T06:52:30.587 回答