coq - 如何创建多态 "map xs f"函数？

Question

问题的陈述。

考虑 map 的定义:

Fixpoint map (xs: list nat): (nat -> nat) -> list nat := match xs with
| nil => fun _ => nil
| x::xs' => fun f => (f x) :: (map xs' f)
end.

它的工作原理如下:

Coq < Eval simpl in map (1::2::3::List.nil) (fun x => x + 1).
     = 2 :: 3 :: 4 :: nil
     : list nat

如何扩展它以适用于任何类型？

例如，在 Haskell 中我可以简单地写如下:

map :: forall a b. [a] -> (a -> b) -> [b]
map xs = case xs of
    [ ]     -> \_ -> [ ]
    (x:xs') -> \f -> f x: map xs' f

但是在 Coq 中，我不明白我可以把这个 forall 放在哪里量词。

我的努力。

The syntax reference解释 Fixpoint 的语法因此:

Fixpoint <em>ident</em> <em>binders</em> {struct <em>ident</em>}<sup>?</sup> : <em>type</em><sup>?</sup> := <em>term</em>

——显然，语法中没有位置可以在绑定(bind)器和类型上绑定(bind)类型变量的量词。我尝试放置 forall到处都是猜测，但我无法让它发挥作用。

我可以看到如何在函数参数的结果类型中使 type 部分成为多态，而无需触及 binders 部分:

Fixpoint map (xs: list nat): forall B, (nat -> B) -> list B := match xs with
| nil => fun _ => nil
| x::xs' => fun f => f x :: (map xs' f)
end.

- 但不幸的是，这也给出了一个错误，并且对我来说足够神秘:

In environment
map : list nat -> forall B : Type, (nat -> B) -> list B
xs : list nat
T : Type
The term "nil" has type "list ?A" while it is expected to have type
 "(nat -> T) -> list T".

所以，即使对于这个更简单的情况我也没有解决方案。

那么，可以做什么？

Answer 1

在 Coq 中，Fixpoint 命令只是对 fix 术语构造函数的包装，它允许我们定义匿名递归函数。 map 的直接定义如下:

Require Import Coq.Lists.List.
Import ListNotations.

Definition map_anon : forall A B, (A -> B) -> list A -> list B :=
  fix map A B (f : A -> B) (l : list A) : list B :=
    match l with
    | [] => []
    | x :: l => f x :: map A B f l
    end.

这在道德上等同于以下定义:

Fixpoint map A B (f : A -> B) (l : list A) : list B :=
  match l with
  | [] => []
  | x :: l => f x :: map A B f l
  end.

请注意，A 和 B 被绑定(bind)为常规变量:在 Coq 中，类型和术语之间没有区别，这些声明使 Coq 将它们的类型推断为是类型。定义不需要 forall 量词。