类型`Set`的具体示例是什么?`Set`的含义是什么? [英] What is a concrete example of the type `Set` and what is the meaning of `Set`?
问题描述
除了this great discussion in SO之外,我还在Adam Chlipala的书中遇到了Set
,我一直在试图理解Set
是什么。他的第一个示例使用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
是类型层次结构中的第一个&Quot;类型set";,例如Set = Type(0) <= Type = Type(1) <= Type(2) <= ...
。我想这是有道理的,就像我假设nat in Type
和所有常见的编程类型都在其中一样,但不确定Type
中有什么不会在Set
中。也许是递归类型?我不确定这是否是正确的例子,但我正在努力理解这个概念的含义以及它在概念上(和实践中)的用处。
推荐答案
虽然Set
和Type
在CoQ中有所不同,但这主要是由于历史原因。如今,大多数开发并不依赖于Set
不同于Type
。特别是,如果到处将Set
替换为Type
,那么Adam的评论也是有意义的。要点是,当您想要定义在执行期间可以用来计算的数据类型(例如数字)时,您希望将其放入Set
或Type
而不是Prop
。这是因为当您从Coq中提取程序时,Prop
中的内容将被擦除,因此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
和Type
之间看到的唯一区别。您还可以通过使用-impredicative-set
选项调用CoQ:
(* 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
具有相同的行为,因为当u
和v
不同时,Type@{u}
和Type@{v}
是不同的东西!)
如果您想知道为什么这个特性很有用,这不是偶然的。绝大多数CoQ开发并不依赖于它。默认情况下,它被关闭,因为它与一些通常被认为在Coq开发中更有用的公理不兼容,例如排除中间的强大定律:
forall A : Prop, {A} + {~ A}
打开-impredicative-set
时,此公理产生悖论,但默认情况下使用它是安全的。
这篇关于类型`Set`的具体示例是什么?`Set`的含义是什么?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!