在 Agda 中制定依赖类型系统

Question

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

\n\n

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

\n\n

infixr 5 _\xe2\x87\x92_\ndata Type : Set where\n    _\xe2\x87\x92_ : Type \xe2\x86\x92 Type \xe2\x86\x92 Type\n\ninfix 4 _\xe2\x8a\xa2_\ndata _\xe2\x8a\xa2_ : List Type \xe2\x86\x92 Type \xe2\x86\x92 Set where\n    var : {a : Type} \xe2\x86\x92 [ a ] \xe2\x8a\xa2 a\n    \xce\xbb\'  : {a b : Type} {\xce\xb3 : _} \xe2\x86\x92 a \xe2\x88\xb7 \xce\xb3 \xe2\x8a\xa2 b \xe2\x86\x92 \xce\xb3 \xe2\x8a\xa2 a \xe2\x87\x92 b\n    ply : {a b : Type} {\xce\xb3 \xce\xb4 : _} \xe2\x86\x92 \xce\xb3 \xe2\x8a\xa2 a \xe2\x87\x92 b \xe2\x86\x92 \xce\xb4 \xe2\x8a\xa2 a \xe2\x86\x92 \xce\xb3 ++ \xce\xb4 \xe2\x8a\xa2 b\n    weak : {a b : Type} {\xce\xb3 : _} \xe2\x86\x92 \xce\xb3 \xe2\x8a\xa2 b \xe2\x86\x92 a \xe2\x88\xb7 \xce\xb3 \xe2\x8a\xa2 b\n    cntr : {a b : Type} {\xce\xb3 : _} \xe2\x86\x92 a \xe2\x88\xb7 a \xe2\x88\xb7 \xce\xb3 \xe2\x8a\xa2 b \xe2\x86\x92 a \xe2\x88\xb7 \xce\xb3 \xe2\x8a\xa2 b\n    xchg : {a : Type} {\xce\xb3 \xce\xb4 : _} \xe2\x86\x92 \xce\xb3 \xe2\x86\xad \xce\xb4 \xe2\x86\x92 \xce\xb3 \xe2\x8a\xa2 a \xe2\x86\x92 \xce\xb4 \xe2\x8a\xa2 a\n

\n\n

我还可以大致遵循Haskell 中依赖类型 \xce\xbb-calculus 的LambdaPi教程实现。但它是隐式类型的，与我的 Agda 代码不同，而且我不确定从哪里开始修改我的代码，因为到目前为止想到的路径导致了无限倒退：

\n\n

data _\xe2\x8a\xa2_ : List (? \xe2\x8a\xa2 ?) \xe2\x86\x92 (? \xe2\x8a\xa2 ?) \xe2\x86\x92 Set where ...\n

\n\n

Google 搜索“在 Agda 中嵌入依赖类型”等仅返回 Agda中依赖类型编程的结果...

\n

Answer 1

我们在类型理论中的类型理论论文中已经做到了这一点，该论文实际上是在 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}
}