我无法理解构造函数的原理及其工作原理。
例如，在 Coq 中，我们被教导这样定义自然数：
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
并且被告知S 是一个构造函数，但这究竟是什么意思？
如果我这样做：
Check (S (S (S (S O)))).
我知道它是4，类型为nat。
这是如何工作的，Coq 是如何知道(S (S (S (S O)))) 代表4？
我想这个问题的答案是 Coq 中一些非常聪明的背景魔法。
【问题讨论】：
(S (S (S (S O)))) 的漂亮打印为4 只是一种方便，您不应该让您分心。如果您想了解构造函数是什么，请使用构造函数Z（为零）和N（下一个）定义您自己的类型naturals。那么魔法就不会发生了。
标签： constructor coq
Inductive naturals : Type :=
| Z : naturals
| N : naturals -> naturals.
说了以下几点：
Z 是naturals 类型的术语
当e 是naturals 类型的术语时，N e 是naturals 类型的术语。
应用Z 或N 是创建自然的仅有的两种方法。当给定一个任意的自然时，您知道它是由一个或另一个制成的。
naturals 类型的两个项 e1 和 e2 相等当且仅当它们都是 Z 或者它们分别是 N t1 和 N t2 且 t1 等于t2。
您可以看到这些规则如何推广到任意归纳类型定义。一般来说，在t 类型的任意归纳类型定义中：
t 类型的术语；t 类型的任何术语都是应用与类型t 定义时关联的构造函数之一的结果；换句话说，给定一个t 类型的术语，可以假设它是应用t 的构造函数之一的结果；t 类型的两个术语只有在将相同的构造函数应用于相同的参数时才相等。(旁注：当类型定义用于Z和N形状的构造函数时，这些属性或多或少完全对应于自然数的Peano's axioms。这就是为什么名为nat的类型是在 Coq 中预定义了这些形状的构造函数，用于表示自然数。这种类型接受特殊处理，因为操作原始形式很快就会很累，但特殊处理只是为了方便。）
【讨论】：
在类型理论中，（类型）构造函数只是一种从现有类型（http://en.wikipedia.org/wiki/Type_constructor）构造新类型的方法。
在您对 nat 的归纳定义中，S 是一个构造函数，因为（如果您查看签名）它需要一个 nat 并产生另一个 nat。
例如，一对 nat 的类型构造函数将是：
Inductive pair : Type := P: nat->nat->pair.
Check P (S (O)) (S(S(O))).
【讨论】：
S 是构造函数这一事实并非由其类型决定。例如 plus 1 不是构造函数（即使它与 S 具有相同的类型，甚至 eta-reduces 为它）。 S 是一个构造函数，因为它是构建 nat 的“规范”方式之一。重要的是，类型的构造函数是构建该类型对象的唯一方法。