The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

I'm not so sure, that's a design choice I maybe didn't realize I was making.

Maybe Arnaud has an opinion on this, since he's the one who played

with this distinction initially.

-- Matthieu

On Wed, Dec 7, 2016 at 12:43 PM Maxime Dénès <mail AT maximedenes.fr> wrote:

Hi Matthieu,

Why does the "bifiniteness" info depend on the vernacular command rather
being inferred from the declaration?

Maxime.

On 12/07/16 11:07, Matthieu Sozeau wrote:
> Hi,
>
>   You're right, that's a bit weird. We must have removed or are missing
> a warning telling you that Inductive should rather not be used for a
> non-recursive record definition and that Record is the preferred way to
> define them. As soon as you write Inductive, eta is disabled (eta on
> recursive types is a quite different beast, see N. Ghani's thesis for
> example for a short exposition). This finiteness information you give
> (Variant/Record(bifinite) or Inductive(finite) or CoInductive(cofinite))
> is checked and used by the kernel now, in particular to decide if eta
> can be decided. All this information should be in the documentation indeed.
>
> Best regards,
> -- Matthieu
>
> On Wed, Dec 7, 2016 at 9:06 AM Ralf Jung <jung AT mpi-sws.org
> <mailto:jung AT mpi-sws.org>> wrote:
>
>     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>
>     >>> <mailto: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
>     >>>
>     >
>