The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

David Leduc wrote:
> The lack of support for universe polymorphism is already present with
> very simple examples (no need to consider the category of categories):
>
>   Inductive T : Type := t : Type -> T.
>
> Check t T  raises a universe inconsistency error.  But it should be
> accepted by Coq because when I define the inductive type T'
> (isomorphic to T) by
>
>   Inductive T' : Type := t' : Type -> T'.
>
> Check t T'  is OK!
>
>   
Are you saying you would expect "Check t T" to answer T ? Seriously ?
The problem is that it would strongly suggest that T can be embedded
inside an inhabitant of T, which is the same as having Type:Type. And
this exactly to avoid this that universes were introduced.

If we want to remain consistent, when checking whether T is convertible
with T, one has to know how the universes were instantiated in both
cases, and check whether they are compatible. In some cases (like the
one you gave), you'll be told that T is not the same as T!

This means that the surface syntax "T" would hide universe levels just
like "Type" already does. Many people already suggested that this is not
desirable and prefer to explicitly name their Types like Vladimir did in
the original thread.

Having to write "t T' : T" is indeed a good way to warn that the
argument of constructor t and its type cannot be the same! (The
duplication of definitions is the downside, of course).


>> Every few months, someone asks this question on coq-club. :)
>>     
>
> This is a pity that, in spite of the many requests, universe
> polymorphism is not considered seriously by Coq developers. (Please
> someone, tell me I am wrong).
>
>   
In fact, Coq already supports a limited form of universe polymorphism.
The levels of inductive parameters of type Type (or any arity ending
with Type) are generalized. For instance, list meets this condition, so
the universe of "list A" follows that of A.
In this situation, list does not need to carry explicitely the universe
instantiation because it is derived from the value of the parameters.
"list A" and "list B" are the same if A and B are convertible.



>>  there is no way to mention universe levels explicitly in source code
>>     
>
> Even with that you would need to duplicate definitions. If you define
> categories at level 0 and 1, then you have to duplicate 4 times the
> definition of functors (depending on the levels of source and target
> categories), 16 times the definition of natural transformation, and I
> do not count the duplications for composition of functors and natural
> transformations!!
>
>   
What you need is universe variables you can instantiate several times.
Coq provides universe variables, but they are monomorphic (except for
parameters).

They are many options to implement universe polymorphism, and we don't
know exactly what would be a good solution. You obviously don't want to
write universe instantiations everywhere. Do we want generalization to
happen at the level of constants (every time we write a constant a fresh
instance is created) or at the level of modules (it's the functor
application that creates fresh copies) ?
In the first case, this may slow down type-checking a lot. In the second
case, this is very close to copying T as T', but the module system does
it for you.

Implementing these alternatives is not so complicated, but convincing
yourself that it's correct is by far the hardest bit, believe me. (Which
variables can be generalized and which ones have to be fixed...)
We (mainly Hugo) already had a lot of trouble to get the parameter
polymorphism as it is, and I'm not even sure it is correct.

Bruno Barras.