Ssreflect Users Discussion List

[Assia Mahboubi <>]

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