Coq 中的箭头是通用量化的别名吗？

Question

我正在阅读 chapter 4 of the reference manual of Coq。根据参考文献描述的打字规则，术语 fun x: nat => x 的类型是 forall x: nat, nat.

Assume that E is [nat: Set].

              ...                                 ...
------------------------------ Prod-Set  ------------------- Var
E[] ⊢ forall x: nat, nat : Set           E[x: nat] ⊢ x : nat
------------------------------------------------------------ Lam
        E[] ⊢ fun x: nat => x : forall x: nat, nat

然而，当我Check Coq 这个术语时，它被输入nat -> nat。

Welcome to Coq 8.5pl2 (July 2016)

Coq < Check fun x: nat => x.
fun x : nat => x
     : nat -> nat

这两种是同一种吗？如果是这样，箭头是否隐藏了绑定变量的名称？

Answer 1

fun x: nat => x 的实际类型是 nat -> nat 因为它们没有类型依赖性。箭头是 forall _:nat, nat 的语法糖：正文的类型不依赖于 x 的值，只有正文本身使用 x。类型依赖的一个例子是 vector.

vector A n 是长度为 n 的列表类型，其中包含 A 类型的元素。让我们考虑连接两个向量的 concat 函数：

concat : forall n m: nat, vector n A -> vector m A -> vector (n + m) A

它以两个整数 n 和 m 作为输入，两个大小分别为 n 和 m 的向量并将它们连接起来。这次，concat 的 type 取决于 n 和 m 的值，所以你必须命名它们并使用 forall 而不是 ->。如果您尝试编写 nat -> nat -> vector n A -> ...，变量 n 将不会被正确限制。

Answer 2

正如其他人所说，箭头确实是一种符号。请参阅 Coq 来源中的 theories/Init/Logic.v#L13：

Notation "A -> B" := (forall (_ : A), B) : type_scope.

这个文件是Prelude加载的，你可以用-noinit.

来避免它

Coq 中的箭头是通用量化的别名吗？

Are arrows in Coq aliases of universal quantifications?

coq