coq - "Non strictly positive occurrence of ..."

Question

我尝试定义以下类型

Inductive t : Type -> Type :=
  | I : t nat
  | F : forall A, (t nat -> t A) -> t A.

我收到以下错误:

Non strictly positive occurrence of "t" in "forall A : Type, (t nat -> t A) -> t A".

这个错误是什么意思？

有没有办法“修复”定义以使其有效？

我在哪里可以了解更多相关信息？

谢谢!

Answer 1

您可以在 Coq 引用手册中查找常见错误消息:https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html?highlight=positive#coq:exn.non-strictly-positive-occurrence-of-ident-in-type
本质上，如果构造函数包含函数(例如 t nat -> t A )，则它们不能提及被定义为参数一部分的归纳类型( t nat )。

        vvvvvvvvvvvvvv argument
F : ... (t nat -> t A)               -> t A
                  ^ OK ("positive occurence")
         ^ Not OK ("negative occurence")

具有依赖类型的认证编程 (CPDT) 中的这一部分通过一个简化示例解释了该问题: http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30
如果你可以定义类型

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

然后你可以定义函数

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

和 uhoh (Abs uhoh)会发散。