没有显式类型的 Coq 多态函数

Question

我有一个用 Coq 术语语言编写的 "enumerate" 函数（它叫什么？）。这个函数使用起来有点烦人，因为它要求在使用 enumerate 函数时显式提供 A（列表 l 中元素的类型）。有没有办法避免需要显式传递 A 作为参数？

(* [a, b] -> [(0,a), (1,b)] *)
Fixpoint enumerate (A : Type) (l : list A) : list (nat * A) :=
  let empty : (list (nat * A)) := nil in
  let incr_pair xy := match xy with 
   | (x, y) => ((S x), y)
  end in 
  match l with
  | nil => empty
  | (x :: xs) => (O, x) :: (map incr_pair (enumerate A xs))
  end.

我希望能够写出类似

的东西

Fixpoint enumerate (l : list A) : list (nat * A) := ...

可能使用一些额外的语法来识别 A 到底是什么。

Answer 1

将参数放在方括号中，使它们默认为隐式（参见第 2.7.4 节 here）。此外，您可能应该使用 nat 累加器以非二次方式编写此函数。

Require Import Lists.List.
Import ListNotations.

Fixpoint enumerate_from {A : Type} (n : nat) (l : list A) : list (nat * A) :=
  match l with
  | [] => []
  | x :: xs => (n, x) :: enumerate_from (S n) xs
  end.

Definition enumerate {A} l : list (nat * A) := enumerate_from 0 l.

Compute (enumerate [3; 4; 5]). (* prints [(0, 3); (1, 4); (2, 5)] *)

没有显式类型的 Coq 多态函数

Coq polymorphic function without explicit type

coq