The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

Thanks for all your comments and hints. I am not yet sure if the CIC is not 
more complicated than necessary.

To the best of my understanding the main drivers for the type system of Coq 
are

- consistency
- strongly normalizing
- expressiveness

In order to be consistent only the top type of a type hierarchy can be 
impredicative. This requirement should be satisfied by using

- Prop < Set < Type(1) < Type(2) < …. (Subtype relation)

- Prop : Set : Type(1) : Type(2) : …. (Axioms)

where ‘Set’ is treated as a shorthand for ‘Type(0)'.

This is nearly the same as described in the reference manual except that the 
reference manual excludes ‘Prop: Set’ which has already been remarked by 
Matthieu. If ‘Prop: Set’ were valid then the type system would be simpler. We 
just have a linearly ordered type hierarchy both in the axioms and the 
subtype relation, the top type is impredicative and represents propositions 
and the second type represents programs.


Furthermore the product rules would be simpler and probably the template 
polymorphism rule would not be necessary because Type(0) already represents 
Set.

Inductive list (A:Type): Type := nil: list A | cons: forall (hd:A) (tl:list 
A), list A

with the consequence that list of propositions and all other types are well 
typed and that ‘list nat’ has type Set without any sort replacement.

Is this reasoning correct or have I overlooked something important?

Regards
Helmut