The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

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

The 'Inductive' *is* a record with primitive projections.  It just
doesn't get eta.  I do not see a way to interpret that into the
documentation.

Kind regards,
Ralf

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