The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

Le 07/12/2016 à 08:32, Ralf Jung a écrit :

Hi,

As I understand it, any record declared with the [Record] vernacular
whose projections can be defined, which has at least one projection,
automatically gets eta.  That is, the following records do not enjoy eta:
  Set Primitive Projections.
  Record unit := tt {}.
  Record inhabited (A : Type) : Prop := inhabits { inhabited_val : A }.
  Record unnamed_inhabitant (A : Type) := { _ : A }.
  Inductive prod A B := pair { fst : A ; snd : B }.
and all records which do not suffer from any of these "problems" will
automatically get eta conversion when primitive projections are turned
on.   Someone else (Matthieu?) can correct me if I've missed anything.

I see; in our case, we used 'Inductive' instead of 'Record' so we did
not get eta.  Thanks!  That's kind of a surprising difference between
these vernaculars, at the very least, it should be documented.

Well, I think it is:

"The option Set Primitive Projections turns on the use of primitive projections when defining subsequent records."

Kind regards,
Ralf

On Tue, Dec 6, 2016 at 3:57 PM Ralf Jung <jung AT mpi-sws.org
<mailto:jung AT mpi-sws.org>> wrote:

    Hi all,

    We started to play around with primitive projections a little in our
    development, and if they work (which unfortunately still is a rather big
    if), we could achieve some fairly significant performance improvements:
    Coq 8.6 got >7% faster (that's total compilation time!) by switching the
    record we use for sealing some of our core definitions to primitive
    projections. That's pretty impressive!

    One thing we couldn't figure out though is when we get eta conversion
    for primitive projections.  The aforementioned record used for sealing
    does not have eta (according to About), while other records do.  Are the
    rules for when a primitive record gets eta written down anywhere?  All I
    could find in the documentation is the two paragraphs in
    <https://coq.inria.fr/distrib/8.6beta1/refman/Reference-Manual004.html>,
    which don't even mention that primitive projections have anything to do
    with eta conversion.

    Kind regards,
    Ralf

Attachment: signature.asc
Description: OpenPGP digital signature