2

我已经完成了精益教程的前 3 章，并且已经完成了一些命题逻辑的证明。

现在我试着回过头来问自己一些愚蠢的问题。

我的理解是：

  1. 术语可以有类型：constant A : Type. A是一个术语，Type是 的类型A。
  2. 术语可以变成类型：constant a : A.
  3. 一个术语的类型可以取决于另一个术语的类型constant B : A -> Type：constant B' : Π (a : A), Type

但是这种理解显然是错误的，因为这段代码没有进行类型检查：

constant A : Type

constant a : A

constant B : A -> Type

constant B' : Π (a : A), Type

constant C : Π (b : B), Type

constant C' : Π (B : A), (Π (b : B), Type)

constant C'' : B -> Type

开头的所有行constant C，即第 9、11 和 13 行都会抛出错误error: type expected at B

为什么？我怀疑并非所有术语都可以成为类型。我怀疑类型依赖于其他类型的术语不能成为 types。为什么？

4

1 回答 1

1

第一类错误

第一个类型错误的问题

constant C : Π (b : B), Type

是你不能说b : B，因为B是类型的函数（没有定义）A -> Type，即B是一个值，而不是一个类型。b : 1提出类似orb : "xyz"或的声明是没有意义的b : (λ a : A, Type)。

例如，以下将起作用，因为B a : Type：

constant C : Π (b : B a), Type

第二种错误

第二种类型的错误

constant C' : Π (B : A), (Π (b : B), Type)

源于不知道这B是一个类型的事实，我们所知道B的只是它是类型的某个值（居民）A。为了能够使用B这种方式，你需要这样的东西：

constant C' : Π (B : Type), (Π (b : B), Type)

即我们明确地说B是一种类型。

第三类错误

constant C'' : B -> Type

无法进行类型检查的原因与第一种情况相同。B是一个函数值，而我们在这里需要一个类型——这就是constant B : A -> Type有效的原因。

于 2016-12-08T10:09:01.793 回答