Спецификация типа полиморфа

Question

Я создал тип, который определяет (nat,bool) -> T пары:

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

Теперь я хочу специализировать pprod_nb с T = nat:

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

Мой вопрос: как указать тип формы для T:Set, ...?

Answer 1

Прежде всего, ваш тип pprod_nb слишком большой (это тип функции), чтобы быть Setтак что вам нужно сделать это Type или вы получите ошибку несоответствия юниверса:

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

Если я правильно понимаю, вы имеете в виду "специализироваться", а не "уточнять". Приведенный выше тип не может быть специализированным, так как это тип более высокого порядка или ранга 2 (термин, который вы увидите в Haskell, если вы используете соответствующее расширение, например Rank2Types). Вместо этого, это относится к функциям, которые работают для всех типов T; так как полиморфные функции не могут проверять типы и ведут себя по-разному для разных типов в Coq (технический термин для этого - параметрический полиморфизм), такие функции ведут себя одинаково независимо от того, какой тип результата T они производят.

Вот еще один тип более высокого порядка (это не тип сам по себе, а функция, производящая тип), который вы можете специализировать:

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.

Answer 2

Прежде всего, ваше определение как данное не принимается 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