如何创建多态 "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 ident binders {struct ident}? : type? := term

— 显然，在 binders 和 type 上绑定类型变量的量词在语法中没有任何位置。我尝试通过猜测在这里和那里放置 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 被绑定为常规变量：在 Coq 中，类型和术语之间没有区别，并且这些声明导致 Coq 将它们的类型推断为 Type.定义不需要 forall 量词。

Answer 2

您可以在函数名称后列出所有参数，包括类型参数。您将把任何依赖于其他参数的参数放在它们所依赖的参数之后。

Fixpoint map (A B: Type) (xs: list A) (f: A -> B): list B :=
[...]

如果您更喜欢 foralls，您只需要将所有内容（递归参数及其依赖的任何参数除外）移动到 :.

之后

Fixpoint map (A B: Type) (xs: list A): forall (f: A -> B), list B :=
[...]

这里有两点需要注意。由于 f 之后没有任何内容依赖于 f，您可以使用 -> 表示法。这纯粹是符号，没有任何语义差异。

Fixpoint map (A B: Type) (xs: list A): (A -> B) -> list B :=
[...]

另外要注意的是，当参数像这样在:之后时，我们必须定义一个函数，而不仅仅是list B.

中的东西

Fixpoint map (A B: Type) (xs: list A): (A -> B) -> list B :=
fun f => [...]

这就是您收到错误 The term "nil" has type "list ?A" while it is expected to have type "(nat -> T) -> list T". 的原因。我们需要一个函数，而不仅仅是 list B 类型的东西，这就是 nil。

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

How can I create a polymorphic "map xs f" function?

coq

parametric-polymorphism

问题的陈述。

我的努力。

那么，可以做什么？