如何理解 Coq 类型构造函数 var(t:T)答案

【问题标题】：How to understand Coq type constructor var (t: T)如何理解 Coq 类型构造函数 var(t:T)
【发布时间】：2018-04-08 14:11:06
【问题描述】：

我正在阅读 Coq http://www.cs.cmu.edu/~iliano/projects/metaCLF2/inc/dl/papers/lsfa17.pdf 和 https://github.com/brunofx86/LL 中关于线性逻辑的机械化，但我无法理解来自 https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v 的归纳类型 term 的类型构造函数：

Inductive term  :=
    |var (t: T) (* variables *)
    |cte (e:A) (* constants from the domain DT.A *)
    |fc1 (n:nat) (t: term) (* family of functions of 1 argument *)
    |fc2 (n:nat) (t1 t2: term). (* family of functions of 2 argument *)

关于这个样本我有两个问题（我正在阅读本文中的https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html）：

term 的（超）类型是什么？ Software Foundations 总是指定新类型的（超）类型，例如Inductive color : Type；
主要问题 - 如何理解类型构造函数var (t: T)？。 Software Foundation 在其第一章中只提供了两种类型的构造函数：常量white : color 和函数primary : rgb → color。但是var (t: T) 是一个非常奇怪的符号——它不是有效的函数类型定义，因为它没有明确的返回类型，也没有箭头。

【问题讨论】：

标签： functional-programming logic coq

【解决方案1】：

关于您的主要问题，定义构造函数时的语法var (t : T) 只是var : forall t : T, term 的一些替代（较短）语法，也可以写成var : T -> term（因为没有出现变量@987654325 @在term)。

其实你可以通过处理定义来检查这个，然后是下面的命令：

Print term.

(* and Coq displays the inductive type with the default syntax, that is:

  Inductive term : Type :=
    var : T -> term
  | cte : A -> term
  | fc1 : nat -> term -> term
  | fc2 : nat -> term -> term -> term
*)

接下来（如上面的 Coq 输出所示），数据类型term 的类型确实是Type。

我记得在 Coq 中，所有类型也都有一个类型，而后者总是Prop、Set 或Type。 “类型的类型”通常称为排序。（Prop 处理逻辑命题，而Set 和Type 处理所谓的“信息”类型。）

最后，可以注意到Type 不是指固定类型，而是指给定的Type_i，其中索引i >=0 由Coq 的内核自动确定和检查。有关此主题的更多信息，请参阅 Universes chapter of CPDT 的第一部分

【讨论】：