(value) 构造函数中的全量化类型变量不能按需要显式键入

Question

我有以下 GADT。

Inductive GADT : Type -> Type :=
| A : forall A, GADT A
| B : GADT bool.

并且以下数据类型具有一个构造函数和一个全限定类型变量。

Inductive Wrap A :=
| wrap : GADT A -> Wrap A
| unwrap : forall X, GADT X -> (X -> Wrap A) -> Wrap A.

然后我想定义一个使用unwrap内的函数的递归函数。

Fail Fixpoint wrappedGADT {A} (xs: Wrap A) : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | unwrap _ _ fx k => match fx with
                       | A _ => None
                       | B => wrappedGADT (k true)
                       end
end.

根据这个定义，我收到以下错误消息。

The term "true" has type "bool" while it is expected to have type "T".

我假设当我检查 fx 并获取案例 B 时，参数 fx 具有类型 GADT bool，因此，所有量化类型变量 X 也是 bool。这个假设是错误的吗？

接下来，我尝试如下显式键入 unwrap。

Fail Fixpoint wrappedGADT {A} (xs: Wrap A) : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | @nwrap _ bool fx k => match fx with
                           | A _ => None
                           | B => wrappedGADT (k true)
                           end
  end.

根据这个定义，我收到了一条非常奇怪的错误消息。

The term "true" has type "Datatypes.bool" while it is expected to have type "bool".

任何人都可以指出这个问题的根源吗？

Answer 1

不幸的是，Coq 中的原始匹配语句对于您在此处应用的推理类型并不总是很聪明。 "convoy pattern"（有关更多信息，请参阅 CPDT）通常是解决此类问题的答案。此处的直接应用程序如下所示：

Fail Fixpoint wrappedGADT {A} (xs: Wrap A) {struct xs} : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | unwrap _ _ fx k => match fx in (GADT T)
                       return ((T -> Wrap A) -> option (GADT A)) with
                       | A _ => fun k0 => None
                       | B => fun k0 => wrappedGADT (k0 true)
                       end k
end.

然而，这会遇到另一个问题，即 Coq 在通过 "convoy" 传递函数后无法验证终止条件。似乎要解决这个问题，首先定义对 k 的值进行递归调用的函数，然后转而护送它就足够了：

Fixpoint wrappedGADT {A} (xs: Wrap A) {struct xs} : option (GADT A) :=
  match xs with
  | wrap _ x => Some x
  | unwrap _ _ fx k => let r := fun x => wrappedGADT (k x) in
                       match fx in (GADT T)
                       return ((T -> option (GADT A)) -> option (GADT A)) with
                       | A _ => fun _ => None
                       | B => fun r' => r' true
                       end r
end.

对于你的第二次代码尝试，你正在创建一个局部变量 bool 来保存 unwrap 构造函数中名为 X 的类型，然后它会隐藏 Datatypes.bool 定义。通常，在 Coq 内核语言中没有办法只匹配一个特定类型（尽管类型类提供了一种在某种程度上模拟它的方法）。

Answer 2

这是另一种实现方式，它使用策略构造 wrappedGADT 的主体。它的优点之一是不需要用户手动 return 注释。整体结构与带有 match 表达式的原始代码非常相似。

在这里使用 induction xs 而不是 destruct xs 是至关重要的，因为 Wrap 类型是递归的。

Fixpoint wrappedGADT' {A} (xs: Wrap A) : option (GADT A).
  induction xs as [x | ? fx k r].
  - exact (Some x).
  - destruct fx as [T | ].
    + exact None.
    + exact (r true).
Defined.
Print wrappedGADT'.

这是两个实现在外延上相等的证明。

Goal forall (A : Type) (xs : Wrap A),
    wrappedGADT xs = wrappedGADT' xs.
Proof with auto.
  intros A xs.
  induction xs...
  destruct g...
  simpl; rewrite H; destruct (w true)...
Qed.

如果我们查看为 wrappedGADT' 生成的项（使用 Print wrappedGADT'.），我们将能够使用为 Wrap_rect 生成的归纳原理构造另一个解决方案=18=] 数据类型（我刚刚从 wrappedGADT' 中的 match 表达式中删除了未使用的变量 k）：

Definition wrappedGADT'' {A} (xs: Wrap A) : option (GADT A) :=
  Wrap_rect _
            _
            (fun t => Some t)
            (fun _ fx k r =>
               match fx in (GADT T)
               return ((T -> option (GADT A)) -> option (GADT A)) with
               | A _ => fun _ => None
               | B => fun r' => r' true
               end r)
            xs.

如果我们展开 Wrap_rect，这个解决方案可以导致解决方案 a-la ，实现为 Fixpoint 本身。

(value) 构造函数中的全量化类型变量不能按需要显式键入

All-quantified type variable in (value) constructor cannot be explicitly typed as wanted

coq