The Coq mailing list

[Lauri Alanko <la AT iki.fi>]

On Sun, Apr 15, 2007 at 08:10:17AM -0700, Adam Chlipala wrote:
> You can often get around this by turning on -impredicative-set and using 
> Set in place of Type.  You get the restrictions on elimination of large 
> inductive types, but often you can work around them.

Alas, I fear the restrictions are crucial.

The classical example is when trying to formalize category theory in
the Aczel-Huet-Saïbi style. We define a category:

        Structure Category : Type := {
          Ob : Type;
          Hom : Ob -> Ob -> Setoid;
          (* id, compose and proofs *)
        }.

and functors and their equivalence and build a setoid on them:

        Structure Functor (C D : Category) : Setoid := ... ;

and then we find out, wow, categories and functors form a category:

        Definition CAT : Category := Build_Category Category Functor ...;
        
and at this point we stumble into universe inconsistency.

Impredicative sets obviously won't help, since we want to be able to
extract the Ob type from a category.


To answer Pierre Courtieu's question, my understanding of universe
polymorphism is that it means that instead of each occurrence of Type
having a fixed universe, all terms are parameterized by a
universe. Currently, if I write:

Structure T : Type := { t : Type }.

The real internal types for the terms are (using OCaml's underscore
syntax for uninstantiated variables):

      T : Type (_u + 1)
Build_T : Type _u -> T
      t : T -> Type _u

So if I now try to type the term (Build_T T), the constraint 
(_u + 1 <= _u) fails, so there's no way to instantiate _u and we get
the universe inconsistency.

With universe polymorphism, my understand is that the universe
variables would get internally generalized:

      T : forall u, Type (u + 1)
Build_T : forall u, Type u -> T u
      t : forall u, T (u + 1) -> Type u

And (Build_T T) would be translated

fun u -> Build_T (u + 1) (T u) : forall u, T (u + 1)

Now the same constructions can be used in different universes,
something that's needed if we want to speak of "the category of all
categories" since we really mean "the u+1-category of all
u-categories".

This is just my hazy understanding of the situation, I have only
glanced at Harper and Pollack's paper where the idea originated.


Lauri