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

Question

The statement of the problem.

Consider this definition of 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.

It works like this:

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

How can I extend it to work on any types?

For example, in Haskell I can simply write as follows:

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

But in Coq, I do not understand where I could place this forall quantifier.

My efforts.

The syntax reference explains the syntax of Fixpoint thusly:

Fixpoint ident binders {struct ident}? : type? := term

— So evidently there is no place in the syntax for a quantifier that binds a type variable over both binders and type. I tried placing forall here and there by guesswork but I could not make it work.

I can see how the type section could be made polymorphic in the result type of the function parameter without touching the binders section:

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.

— But unfortunately this also gives an error, and cryptic enough for me at that:

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".

So, even for this simpler case I have no solution.

So, what can be done?

Answer 1

In Coq, the Fixpoint command is just a wrapper around the fix term constructor, which allows us to define anonymous recursive functions. A direct definition of map could be given as follows:

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.

This is morally equivalent to the following definition:

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.

Notice that A and B are bound as regular variables: in Coq, there is no distinction between types and terms, and these declarations causes Coq to infer their types as being Type. No forall quantifier is needed for the definition.