在Coq中为模板列表定义函数时是否必须传入模板类型？

你遇到的问题核心是没有给length函数的类型参数A设置隐式推断规则，以下两种方法可以解决：

方法一：直接在Fixpoint中声明隐式参数 #

把A作为隐式参数加入Fixpoint的参数列表，Coq会根据传入的列表自动推导A的类型：

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

此时直接调用无需指定类型：

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

方法二：给标准库风格的length添加Arguments声明 #

如果你偏好Definition结合fix的写法，只需给length添加隐式参数声明，和你给empty、cons设置的规则一致：

Definition length (A : Type) : list A -> nat :=
  fix length l :=
  match l with
   | empty => O
   | cons _ l' => S (length l')
  end.
Arguments length {A} l.

同样可以直接调用自动推断：

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

原理说明 #

这两种方法都是利用Coq的隐式参数机制，通过{A}标记该参数可由上下文（这里是列表l的类型）自动推导，无需手动传入类型实参，和你之前让[1;2;3]自动推断类型的逻辑完全一致。

内容的提问来源于stack exchange，提问作者Charles Averill