类型作为 coq 中的参数

【问题标题】：types as parameters in coq类型作为 coq 中的参数
【发布时间】：2020-03-11 22:46:15
【问题描述】：

我在stackexchange post 上找到了这段代码，但我对它的工作原理感到困惑。特别是，

Inductive Vector {A : Type} : nat -> Type :=
| nil : Vector 0
  | cons : forall n, A -> Vector n -> Vector (S n).

(* This works. *)
Check (let n := 0 in cons n 42 nil).

在检查中，42 是否绑定到 A？ A 不是必须是类型吗？我尝试将 42 替换为显然是类型的东西，比如“bool”或“Type”，这些也有效。这对我来说很有意义。但是 42 如何在那里进行类型检查？

【问题讨论】：

标签： polymorphism coq dependent-type parametric-polymorphism

【解决方案1】：

A 是Vector 的implicit argument，它（默认情况下）由构造函数cons 继承。这由 Inductive Vector {A : Type} : nat -> Type 中的 A : Type 周围的花括号表示。

因此，在cons n 42 nil 中，cons 应用于某些隐式类型?A、自然数n、?A 类型的元素42 和Vector 0nil。由于42 的类型为nat，因此?A 可以推断为nat。

【讨论】：