The Coq mailing list

[Pierre.Casteran AT labri.u-bordeaux.fr (Pierre CASTERAN)]

Hello,

  I'm looking for some references about the Coq type system,
in particular the rules which give the type of a type,
for instance what is the type of (x:A)B, and how these rules give some
loops as:

Set -> Set:Type_Set.

Set->Type_Set:Type_set.

and so on .


Thanks in advance.
Pierre



[Response:   The type system which is implemented in Coq is slightly
more complicated than it first seems when using the system. The sorts
are actually the following: 

Prop, Type(1), Type(2), Type(3), ..... etc
Set, Type_Set(1), Type_Set(2), Type_Set(3), .... etc.

They are related by the following axioms:

Prop:Type(1),  Type(i):Type(i+1) for all i,
and the same with respectively Set and Type_Set.

The hierarchies Type(1), Type(2), ... Type(i),... and
Type_Set(1), Type_Set(2), ...    are called universes.

There is also a so-called cumulativity rule stating that if
T:Type(i), then one also has T:Type(i+p)  (so for example, Prop admits
all the Type(i) as types), the same for Set and Type_Set.

The implementation however hides the indices of the Type and Type_Set
constructs to the user. Furthermore, the system checks at every step,
that it is possible to put indices in every used instance of these
constructs in a way that is coherent with the typing rules. This
mechanism is sometimes called "floating universes" or "typical
ambiguity".

So when the system validates the statement Type:Type, it actually
means something like Type(1):Type(2). The reason for this is that the
rule Type:Type is known to lead to an incoherent system.

The reason to introduce this hierarchy of universes several years ago,
was that it was not clear whether one wanted to construct the programs
and data-types (like natural numbers) on the impredicative level (i.e.
having them of sort Set) of on the predicative level (of sort
Type/Typ_Set). This issue has already been discussed on this mailing
list. In most of the last developements, it is the first solution
which has been choosen. Therefore the floating universes are currently
not intensively used and might thus one day be dropped of the
implementation. I should however point out that it is still not clear
whether this is the "good" choice. Any comment on this point would
certainly be highly apreciated.