The Coq mailing list

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

Hi Randy,

On Thu, Feb 15, 2001 at 06:56:26PM +0000, Randy Pollack wrote:
> In Lego, besides the anonymous Type there is also explicit syntax
> Type(0), Type(1), ...  If no anonymous Type is ever used (since the
> initial state) then the universe graph remains empty.  (But Lego's
> libraries do use anonymous Type.)  I find this very useful.
> 
> Lego also supports type level variables Type(name).  This is
> completely anonymous when first used, but all occurrences of
> Type(name) will be constrained to the same universe level.  I'm not
> sure this is very useful in practice.

I guess more and more people would like to have a better control on
universes. However, having both explicit universes and variables has
a cost, since the constraint verifier has a better complexity in the
case where you only have variables. But now it seems that the current
implementation has to be redesigned.

One interesting proposal is from Judicael Courant. He suggests that
all universes and constraints should be explicitely stated by the user
(and be included in modules). Maybe Judicael can comment better on this.

> Another thing to point out, that may be of use to Coq users, is that
> Coq's implementation of Universe polymorphism (as contrasted with
> typical ambiguity) is not complete.  Thus, when Coq says "Error:
> Universe Inconsistency", it is not necessarily true that your input
> cannot be typed.  Here is an example (in Coq V6.3.1).

I would not say that Coq implements the so-called universe polymorphism,
as Lego does. For each occurrence of Type in the term, a new variable is
created when typing a definition. But when the definition is used, there
is no creation of fresh universes, and the definition is not typechecked
again. So, I would say we only have typical ambiguity.

>  Reset Initial.
>  Definition I [T:Type; t:T] : T := t.
>  Check (I ((T:Type)T->T) I).   (* self application of I fails *)
> 
> Coq says
> 
>  Error during interpretation of command:
>  Check (I ((T:Type)T->T) I).
>  Error: Universe Inconsistency
> 
> Now enter 
> 
>  Definition J [T:Type; t:T] : T := t.
>  Check (I ((T:Type)T->T) J).   (* application of I to J succeeds *)
> 
> Coq accepts this
> 
>  (I (T:Type)T->T J)
>       : (T:Type)T->T
> 
> The definition J contains a new instance of Type, not constrained by
> occurrences in I.  (See my old paper with Bob Harper for details.)
> Such examples also occur with inductive definitions.

As far as I understand it, it is correct since we do not have
universe polymorphism, so you have to write two instances of the
identity.

> BTW, Coq 7.0beta does accept the self application of I above.  I
> haven't tried to discover how complete the new implementation is
> w.r.t.  universe polymorphism.  Can Jean-Christophe or Hugo answer
> this question?

Regarding the V7beta problem, this is because Check of Coq V7beta does
typecheck the term without checking the generated universe constraints
are compatible with the current environment. I consider this is a bug
and the behaviour of V6.3.1 should be restored.

Meanwhile, you'd better use Definition rather than Check:

Parameter K: (T:Type)T->T.
Definition y := (K ((T:Type)T->T) K).

raises
Error: Universe Inconsistency.

Cheers,

Bruno.

-- 
  Projet LogiCal - INRIA Rocquencourt
  tel : +33 1 39 63 53 16
  
mailto:Bruno.Barras AT inria.fr
  http://logical.inria.fr/~barras