Ssreflect Users Discussion List

[Robbert Krebbers <>]

Dear Assia,

thank you very much for the answer. Since this seems to be a recurring 
question, it may be nice to add this as a comment to eqtype.v (where 
this idiom occurs first).

Best,

Robbert

On 02/21/2016 07:04 PM, Assia Mahboubi wrote:
> Hello Robbert,
>
>    sorry, we hit again the issue of the archives of the list not being 
> indexed by
> search engines...
>
> Christian Doczkal asked the very same question a while ago:
> https://sympa.inria.fr/sympa/arc/ssreflect/2013-11/msg00010.html
>
> and the thread includes answers by Laurent Théry and Georges Gonthier.
>
> In short, all the instances built to inhabit `type` pack a redundant copy on
> their first argument (sort) as their third (for the anonymous field).
>
> The reason is that in Coq, several strategies can be applied to compare terms
> that are constants applied to some arguments. Some (type inference, 
> unification)
> compare arguments left-to-right, and others (kernel) right-to-left.
>
> So the anonymous field is here to ensure that whatever strategy is applied,
> sorts are compared first when comparing two instances of a same structure.
>
> Indeed the strategy can otherwise make a dramatic difference, as instances of
> classes (the argument in the middle) can be huge terms. In the case when the 
> two
> sorts are easily seen as distinct, the failure might take a much longer time 
> to
> happen if you compare the classes first.
>
> Hope this helps,
>
> assia
>
> Le 21/02/2016 18:29, Robbert Krebbers a écrit :
> > Hello list,
> >
> > In structure declarations like eqType:
> >
> >    Structure type := Pack {sort; _ : class_of sort; _ : Type}.
> >
> > What is the purpose of the third anonymous field "_ : Type"? Such a field 
> > seems
> > to occur in all algebraic structures in the mathcomp hierarchy and also 
> > appears
> > in the Zmodule example at page 7 of [1] but does not seem to be explained in
> > that paper.
> >
> > Best,
> >
> > Robbert
> >
> > [1] Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau.
> > Packaging Mathematical Structures. 2009.