The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

I've thought about this as well and I agree this would be beneficial.
There have been questions on this list of users who have defined a
map-like function without generalizing the uniform parameters, and
then could not figure out why they couldn't use it in a nested
fixpoint.

To ensure easier backwards compatibility, we could have an "Automatic
Generalization on/off" vernacular to toggle the feature on or off.

Stéphane

On Wed, Oct 28, 2009 at 10:51 PM,  
<roconnor AT theorem.ca>
 wrote:
> 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.''
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06