The Coq mailing list

[Petter Urkedal <paurkedal AT gmail.com>]

On Sat, Oct 6, 2012 at 1:51 PM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> Le Sat, 6 Oct 2012 10:19:39 +0200,
> Petter Urkedal 
> <paurkedal AT gmail.com>
>  a écrit :
>> I can see the point of using Type in a parameter positions of general
>> purpose modules, and this seems to be the general design of the
>> standard library.  So, is the idea that one should just switch to Type
>> whenever these are mixed into ones own data structures, even if they
>> could have been in Set from a logical point of view?  I don't see a
>> problem with it if extraction works, it seems a bit radical to lift
>> whole developments to an unspecific universe.
>
> The extraction does not make difference between Set and Type. After
> all, OCaml, Haskell and Scheme do not care about universe
> inconsistencies (which is mainly why we have Set and Type in Coq).
> I would recommend to always use Type, and never Set. Or always use Set
> and never Type (for very simple developpements which could allow it).
> Mixing both is hardly ever a good idea. The only good points of using
> Set vs Type is to make coq perform less computations to solve universe
> constraints. But this part of the computation is often neglictable in
> regards to the other computations.

That's precisely what I needed to hear!

> Of course, it is okay to play with it and allows you to have a better
> of the mechanics. But once you know how it works, chose between make
> Coq do all computations (stick only to type) or make him do none (stick
> with Set, and if needed define some universe: Definition U1 := Type.
> Definition U2 := (Type : U1). and so on, which you will use instead of
> Type)

Nice tip, though I don't worry about leaving the inequalities to Coq.

Thanks,
Petter