“非严格正发生......”

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

你可以看一下常见的错误消息在勒柯克参考手册：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)的差异会增大。