The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Bas,

> I recently learned that the Coq sort hierarchy has changed. Prop is
> now a subsort of Set.
> 
> Could anyone tell me about the reasons for this change and its
> theoretical motivations?

The practical motivation of this change is to have that the sorts
assigned to sort-polymorphic inductive types are linearly ordered,
and, in particular that whenever a sort-polymorphic type is set at
some level Prop, predicative Set or Type(i), then it is also in all
levels above.

Before we had

    Prop : Type0 : Type1 : ...
    Set  : Type0 : Type1 : ...

with the inclusions

    Prop < Type0 < Type1 < ...
    Set  < Type0 < Type1 < ...

This meant that a sort-polymorphic inductive type on which no 
level constraints applied like

  Inductive unit := tt

could not be seen as a Set if placed in Prop as the absence of
constraints tells it should be.

With the new hierarchy, we have

    Prop : Type0 : Type1 : ...
    Set  : Type0 : Type1 : ...
    Prop < Set   < Type1 < Type2 < ...

which in fact is the same as

    Prop            : Type0 : Type1 : ...
           Type(-1) : Type0 : Type1 : ...
    Prop < Type(-1) < Type0 < Type1 < ...

if we interpret predicative Set as Type(-1), which, if we shift the
indices used to number the levels, is the same as

    Prop         : Type1 : Type2 : ...
           Type0 : Type1 : Type2 : ...
    Prop < Type0 < Type1 < Type2 < ...

which differs only from the original hierarchy by not using Set and by
enforcing the type of Prop to be Type1 instead of Type0, what at the
end corresponds to a subset of the former system.

With the new hierarchy, unit, while still put by default at level
Prop, can now freely be used as a Set, what is more convenient and in
my opinion more natural.

One may argue that it could be as simpler to interpret predicative Set
as Type0 (instead of a virtual Type(-1)) and to keep Prop of type
Type0. My point is that it is in practise not more complicated to
implement Prop of type Type1 than of Type0, and that this allows to
keep a sort guaranteed not to contain Prop.

I don't see any disavantage to this approach up to now, but comments
are welcome.

Hugo

PS: I followed the convention of the Reference Manual of Coq
(chapter 4) which numbers Type levels from 0 (what leads to introduce
a negative level to interpret Set as a distinct Type). By the way, I
just remarked that paragraph "Convertibility" in Section 4.3 of the
reference manual is not up to date (though paragraph
"Sort-polymorphism of inductive families" of Section 4.5.3 is).

PS2: An alternative could have been to introduce a new base sort, say
Singleton, to type the inductive types low enough to be put in Prop,
with the associated subtyping Singleton < pSet and Singleton < Prop. My
feeling was however that it would have made things more complicated
than just having Prop < pSet and I renounced to it.