Generaling parameteric Fixpoint parameters

[roconnor]

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

[Stéphane Lescuyer-3]

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

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

[roconnor]

On Wed, 28 Oct 2009, Stéphane Lescuyer wrote:

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

It would be better to (eventually) have it on by default because we want
to make avaiable fixpoints with higher order uniform parameters from
people who haven't even though about others reusing their work.

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

[Stéphane Lescuyer-3]

> It would be better to (eventually) have it on by default because we want to
> make avaiable fixpoints with higher order uniform parameters from people who
> haven't even though about others reusing their work.

Indeed, that's the idea. But even if its on by default it still
facilitates backward compatibility : you can have your own Compat82.v
file that just contains 'Automatic Generalization off' and you only
need to import it in your old projects.

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

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