The Coq mailing list

[roconnor AT theorem.ca]

I have an idea for change in coq that I wanted to run by coq-club before 
making a feature request in coq-bugs.

My idea would be to have the (Co)Fixpoint function automatically 
generalize the initial segment of parameters that are parametric in the 
body of the fixpoint.

For example consider the following Coq code:

Fixpoint map (A B: Type)(f:A -> B)(l:list A) :=
match l with
| nil  => nil
| cons x xs => cons (f x) (map A B f xs)
end.

which currently generates the definition

map =
fix map (A B : Type) (f : A -> B) (l : list A) {struct l} : list B :=
  match l with
  | nil => nil
  | x :: xs => f x :: map A B f xs
  end

would under my proposal instead generate:

map =
fun (A B : Type) (f : A -> B) =>
fix map (l : list A) : list B :=
  match l with
  | nil => nil
  | a :: t => f a :: map t
  end

The rational behind my proposal is that I think it is fairly common / 
natural to have parametric parameters in Fixpoint definitions because 
abstracting them out is somewhat annoying to do.  With parametric 
parameters abstracted out more beta reduction becomes possible for 
partially applied fixed point terms.  In particular nested fixpoint 
operations become easier to write because the nested fixpoint can a 
higher-order fixpoint defined elsewhere that takes the recursive call of 
the as a (parameteric) parameter.

That being said this would be a non-backwards compatable change (though I 
don't think too much would break in practice), nor do I know how easy it 
really is to recognise if a parameter is being used parametrically or not.

Prehaps this proposal has been considered in the past.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''