The Coq mailing list

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

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.

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
>