typeclass - 如何在定理类型中引用类型类多态变量？

Question

我写了一个 Haskell 风格的 Functor 类型类:

Class Functor (f: Type -> Type) := {
  map {a b: Type}: (a -> b) -> (f a -> f b);
  map_id: forall (a: Type) (x: f a), map id x = x
}

id 有明显的定义。

现在，我已经为 list 和函数类型证明了 Functor 的实例。但我想证明关于任何 仿函数的陈述。首先，我想证明什么本质上是重言式:重述任何仿函数的 map_id。

Theorem map_id_restatement: forall (F: Type -> Type), 
  Functor F -> forall T (x: F T), map id x = x.

为了证明这个定理，我会简单地应用 map_id。但是当我尝试开始证明这一点时出现错误:

Toplevel input, characters 88-91:
Error:

Could not find an instance for "Functor F" in environment:

F : Type -> Type
T : Type
x : F T

但是由于类型的假设，Functor F 实例应该已经在范围内。为什么不识别？

编辑:

好的，我发现我可以通过量化 Functor F 来让它工作:

Theorem map_id_restatement: forall (F: Type -> Type) (finst: Functor F),
  forall T (x: F T), map id x = x.
Proof. apply @map_id. Qed.

为什么这是必要的？有趣的是，如果我没有显式地为仿函数实例命名(即，如果我只是编写 (_: Functor F))，它不会工作。

Answer 1

我不知道这是否是一个错误，但请注意，当您编写类似 Functor F -> SomeType 的内容时，您是在隐含地说明 SomeType不依赖于 Functor 实例，这在您的情况下是不正确的:您的定理的完整类型，打印所有隐式参数，将类似于:

Theorem map_id_restatement: forall (F: Type -> Type) (finst: Functor F),
  forall T (x: F T), @map F fints T T (@id T) x = x.

如果将 finst 替换为 _，您会得到

Theorem map_id_restatement: forall (F: Type -> Type) (_: Functor F),
  forall T (x: F T), @map F _ T T (@id T) x = x.

这不能真正进行类型检查，因为 _ 实际上不是一个变量名。

请注意，如果您在冒号之前匿名绑定(bind) Functor F，Coq 会接受它:

Theorem map_id_restatement (F: Type -> Type) (_ : Functor F) :
  forall T (x: F T), map (@id T) x = x.
Proof. apply @map_id. Qed.

据推测，这里 Coq 以不同的方式处理 _，并用自动生成的名称替换它，而不是实际保留它未命名。您还可以使用以下形式，它既可以在 forall 下使用，也可以在冒号之前使用:

Theorem map_id_restatement (F: Type -> Type) : forall `(Functor F),
  forall T (x: F T), map (@id T) x = x.
Proof. apply @map_id. Qed.