您是否需要将模板类型传递给Coq中接受模板对象的函数?

Question

我正在尝试使用Coq中的列表:

Inductive list (A : Type) : Type := 
| empty : list A 
| cons (n : A) (l : list A).
Arguments empty {A}.
Arguments cons {A} n l.

底部的Arguments语句(除了一些Notation语句)允许我写[1;2;3]，让解释器计算出应该填充A的类型，而不是指定A应该是nat。

然而，当我为我的list对象编写length函数时，我的方法抛出错误:

Fixpoint length (l : list A) : nat :=
match l with 
| empty => 0
| cons n cdr => 1 + (length cdr)
end.

它期望传入的列表实际上是A类型的列表，而不是将A识别为模板类型。

标准库采用这种方法:

Definition length (A : Type) : list A -> nat :=
  fix length l :=
  match l with
   | nil => O
   | _ :: l' => S (length l')
  end.

，在这里您需要传递列表的类型，如下所示:

Compute length nat [1;2;3]. (* 3 *)

这似乎是一个严重的缺点。我似乎不能像以前那样定义一个解决这个问题的Argument语句。真的没有别的办法了吗?

Answer 1

首先，list的Arguments语句不负责让您编写[1;2;3]。这是一个单独的Notation。此外，如果参数是显式的，您可以为它传递表达式_，以请求Coq填充它。(即Notation[x; ...; z]可以使用或不使用Arguments来定义)

Inductive mylist (A : Type) : Type := mynil | mycons (x : A) (xs : mylist A).
Notation "[[ ]]" := (mynil _). (* note that I *can* pass in the explicit type argument without actually knowing it *)
Notation "[[ x ; .. ; y ]]" := (mycons _ x .. (mycons _ y [[]]) .. ).
Check [[]].
Check [[1;2;3]].

理解了这一点，可以使显式地传递类型的length实际上并没有那么糟糕。

Fixpoint mylength (A : Type) (xs : mylist A) : nat :=
match xs with
| mynil _ => 0
| mycons _ _ xs => S (mylength A xs)
end.
Compute (mylength _ [[1; 2; 3]]). (* Coq solves for [_ := nat] itself *)

撇开这些不谈，你可以通过把参数放在大括号里来声明它是隐式的，不然呢?对于像mylength这样的定义，它最初是用显式参数定义的，Arguments可以改变它:

Arguments mylength {A} xs.
Compute (mylength [[1; 2; 3]]).
(* Indeed, the standard library has Arguments length [A] xs, which is similar to using {A} (read the documentation!) and lets you say *)
Compute (length [1; 2; 3]).

但是更常见的是从一开始就用隐式参数定义函数。

Fixpoint mylength2 {A : Type} (xs : mylist A) : nat := (* implicit A *)
match xs with
| mynil _ => 0
| mycons _ _ xs => S (mylength2 xs)
end.
Compute (mylength2 [[1; 2; 3]]).

(你不能不声明A作为mylength/mylength2的参数，因为参数类型mylist A需要A在作用域中才有意义)