`Set` 类型的具体示例是什么？`Set` 的含义是什么？

我一直试图理解什么Set除了在 Adam Chlipala 的书中遇到它之后SO中的这个精彩讨论 https://stackoverflow.com/questions/39601502/what-exactly-is-a-set-in-coq。他的第一个示例定义二进制操作使用Set:

Inductive binop : Set := Plus | Times.

在那本书中他说：

Second, there is the : Set fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs.

这让我很困惑。亚当在这里的意思是什么？

另外，我认为一些额外的具体例子将有助于我的理解。我不是 Coq 专家，所以我不确定什么类型的示例会有所帮助，但一些简单且非常具体/基础的示例可能会很有用。

注意，我已经看到了Set是类型层次结构中的第一个“类型集”，例如Set = Type(0) <= Type = Type(1) <= Type(2) <= ... 。我想这在直觉上是有道理的，就像我假设的那样nat \in Type以及所有常见的编程类型都在其中，但不确定其中会包含什么Type那不会是在Set。也许是递归类型？不确定这是否是正确的例子，但我试图理解这个概念的含义以及它的概念（和实践）有用性。

Though Set and TypeCoq 中有所不同，这主要是由于历史原因。如今，大多数发展并不依赖于Set不同于Type。特别是，如果您替换，亚当的评论也有意义Set by Type到处。要点是，当您想要定义一个可以在执行期间计算的数据类型（例如数字）时，您需要将其放入Set or Type 而不是 Prop。这是因为生活在其中的事物Prop当你从 Coq 中提取程序时会被删除，所以在Prop最终不会计算任何东西。

至于你的第二个问题：Set是生活在其中的东西Type，但不在Set，如以下代码片段所示。

Check Set : Type. (* This works *)
Fail Check Set : Set.
(* The command has indeed failed with message: *)
(* The term "Set" has type "Type" while it is expected to have type  *)
(* "Set" (universe inconsistency: Cannot enforce Set+1 <= Set). *)

这一限制是为了防止理论中出现悖论。这几乎是您看到的唯一区别Set and Type默认情况下。您还可以通过使用以下命令调用 Coq 来使它们更加不同-impredicative-set option:

(* Needs -impredicative-set; otherwise, the first line will also fail.*)
Check (forall A : Set, A -> A) : Set.
Universe u.
Fail Check (forall A : Type@{u}, A -> A) : Type@{u}.
(* The command has indeed failed with message: *)
(* The term "forall A : Type, A -> A" has type "Type@{u+1}" *)
(* while it is expected to have type "Type@{u}" (universe inconsistency: Cannot enforce *)
(* u < u because u = u). *)

请注意，我必须添加Universe u.声明强制两次出现Type处于同一水平。如果没有这个声明，Coq 会默默地把这两个Type处于不同的宇宙层次，命令都会被接受。 （这并不意味着Type会有相同的行为Set在这个例子中，因为Type@{u} and Type@{v}是不同的事情，当u and v是不同的！）

如果您想知道为什么此功能很有用，那么这并非偶然。绝大多数 Coq 开发并不依赖它。它默认是关闭的，因为它与一些通常被认为在 Coq 开发中更有用的公理不兼容，例如强排中律：

forall A : Prop, {A} + {~ A}

With -impredicative-set打开时，这个公理会产生一个悖论，而默认情况下使用它是安全的。