多态类型规范

Question

我创建了一个定义 (nat,bool) -> T 对的类型：

Definition pprod_nb : Set := forall T:Set, (nat -> bool -> T) -> T.

现在我想用 T = nat 专门化 pprod_nb :

(nat -> bool -> nat) -> nat

我的问题是：如何为所有 T:Set, ... 指定形式的类型？

Answer 1

首先，Coq 不接受您给出的定义：

The term "forall T : Set, (nat -> bool -> T) -> T" has type 
"Type" while it is expected to have type "Set" (universe inconsistency).

您确定这是您使用的定义吗？

为了回答我认为是您的实际问题，我认为您希望 T 作为参数：

Definition pprod_nb (T : Set) : Set := (nat -> bool -> T) -> T.

这样pprod_nb是Set -> Set类型的，所以可以应用到nat:

Definition pprod_nb_nat := pprod_nb nat.

这给出了您似乎想要的类型：

Eval compute in pprod_nb_nat.
      = (nat -> bool -> nat) -> nat
      : Set

Answer 2

首先，您的类型 pprod_nb 太大（它是一个函数类型）不能成为 Set，因此您需要将其设为 Type 否则您将收到 Universe 不一致错误：

Definition pprod_nb : Type := forall T:Set, (nat -> bool -> T) -> T.

如果我没理解错的话，你的意思是 "specialize" 而不是 "specify"。上面的类型不能专门化，因为它是 higher-order 或等级 2 类型（如果您使用适当的扩展名，如 Rank2Types，您会在 Haskell 中看到这个术语）。相反，它指的是适用于所有类型的函数 T；由于多态函数无法检查类型并且在 Coq 中对不同类型的行为不同（这方面的技术术语是参数多态性），因此无论它们产生什么结果类型，这些函数的行为都是一致的T。

这是您可以专门化的另一种 higher-order 类型（它本身不是一种类型，它是一种生成类型的函数）：

Definition pprod_nb' : Set -> Type := fun T:Set => (nat -> bool -> T) -> T.

Eval compute in (pprod_nb' nat).
(*
     = (nat -> bool -> nat) -> nat
     : Type
*)

(* check that these two definitions are indeed exactly the same *)
Theorem pprod_nb'_is_pprod_nb_forall :
  pprod_nb = forall T, pprod_nb' T.
Proof. reflexivity. Qed.

我写它的方式是为了突出与您的 pprod_nb 定义的相似性，但更自然地写成 Definition pprod_nb' T := (nat -> bool -> T) -> T.

多态类型规范

Polymorph type specification

lambda-calculus

coq