如何指定forall T:Set形式的类型？Coq类型定义与特化问询

首先，你定义的pprod_nb其实是Church编码的(nat, bool)对偶类型，它通过全称量化T:Set来实现多态性——对任意类型T，只要能提供一个从nat和bool映射到T的函数，就能得到一个T值。

要特化它到T=nat，得到(nat -> bool -> nat) -> nat这个类型，其实非常直接，在Coq里有几种常用方式：

• 直接验证特化后的类型：用Check命令直接对pprod_nb应用具体类型参数nat，就能看到特化后的结果：

  Check pprod_nb nat.
  

  执行后Coq会输出：(nat -> bool -> nat) -> nat : Set，这正是你想要的类型。

• 给特化后的类型定义别名：如果需要反复使用这个特化类型，可以给它起一个更直观的名字：

  Definition pprod_nb_nat : Set := pprod_nb nat.
  

  之后你就可以用pprod_nb_nat来代替冗长的(nat -> bool -> nat) -> nat了。

• 补充：构造该类型的项：如果之后需要创建这个特化类型的实例（比如表示具体的(nat, bool)对偶），可以像这样写：

  (* 比如表示对偶(5, true) *)
  Definition example_pair : pprod_nb nat :=
    fun (f : nat -> bool -> nat) => f 5 true.
  

本质上，特化forall T:Set这类全称量化的类型，就是把量化的类型变量T替换成你需要的具体类型（这里是nat）——Coq的类型系统会自动处理这种参数替换。

内容的提问来源于stack exchange，提问作者L. Soret