Feature Request: Supporting explicit universe level variables about coq HOT 7 OPEN

Le 15 janv. 2013 à 16:22, Jason Gross [email protected] a écrit :

Is there any plan to have explicit universe level variables in Coq? Alternatively, is there a way to get the following approach to "work"?

Set Implicit Arguments.

Set Printing Universes.

Set Printing All.

Section Cat.

Polymorphic Let typeof {T : Type} (_ : T) := T.

Polymorphic Record Category (i : Type) (j : Type) :=

{

Object :> typeof i;

Morphism : Object -> Object -> typeof j

}.

Check Category. (* Category (* Top.108
Top.109 )
: forall ( : Type (_ Top.108 )) ( : Type (_ Top.109 )),
Type ( max(Top.100, Top.108) *) *)

Check (@category nat). (* Category (* Set Top.111 ) nat
: forall _ : Type ( Top.111 ), Type ( max(Top.100, Set) *) *)

Check (@category nat nat). (* Category (* Set Set ) nat nat
: Type ( max(Top.100, Set) *) *)
End Cat.
In particular, where does the Top.100 come from, and are there any reasonable semantics that make Category nat nat land in Set?

Top.100 comes from the Let. Let's are not polymorphic, ever, it should be an error to write [Polymorphic Let](or Polymorphic Variable for that
matter). The fact that a Let/Variable is discharged in a polymorphic or monomorphic constant determines if it "is" polymorphic or not.

Only with impredicative Set could [Category nat nat] fall in [Set]: it contains a Type, the typeof nat which is Set itself.
-- Matthieu

from coq.

I'm not sure what you're trying to achieve here, so I don't know which approach should "work".
There is the possibility that in the future we'll add explicit polymorphism construct, in principle just the syntax is missing now. But it is possible that it is subsumed already using a mix of Monomorphic and Polymorphic definitions.

from coq.

Sorry, I meant Type (* (Set)+1 *), not Set. Currently, if I Print Category outside of the section (after Unset Printing All), I get

Polymorphic Record Category (i : Type (* Top.39 *)) 
(j : Type (* Top.40 *)) : Type (* max(Top.38, Top.39) *) := Build_Category
  { Object : (fun (T : Type (* Top.38 *)) (_ : T) => T) Type (* Top.39 *) i;
    Morphism : Object ->
               Object ->
               (fun (T : Type (* Top.38 *)) (_ : T) => T) Type (* Top.40 *) j }
(* Top.38
   Top.39
   Top.40 |= Top.39 < Top.38
              Top.40 < Top.38
               *)

I was hoping that there would be some way to get Coq to define a Category as something like

Polymorphic Record Category (i : Type (* Top.39 *)) 
(j : Type (* Top.40 *)) : Type (* max((Top.39)+1, (Top.40)+1) *) := Build_Category
  { Object : Type (* Top.39 *);
    Morphism : Object ->
               Object ->
               Type (* Top.40 *) }

where the types inside the record are polymorphically filled with the universe levels/types of the things I pass as parameters. So, for example, I would want Let NatCategory := Category nat nat to be roughly equivalent to

Record NatCategory : Type (* (Set)+1) *) := Build_Category
  { Object : Type (* Set *);
    Morphism : Object ->
               Object ->
               Type (* Set *) }

from coq.

And, in fact, it seems that the following basically does what I want (though I haven't tested it much):

Set Implicit Arguments.

Set Printing Universes.

Section Cat'.
  Let typeof {T : Type} (_ : T) := T.
  Variable i : Type.
  Variable j : Type.

  Let U := Eval hnf in typeof i.
  Let V := Eval hnf in typeof i.

  Polymorphic Record Category' :=
    {
      Dummyi := i;
      Dummyj := j;
      Object' :> U;
      Morphism' : Object' -> Object' -> V
    }.
End Cat'.
Check Category' nat nat. (* Category' (* Set Set *) nat nat
     : Type (* (Set)+1 *) *)

Now if only I could get rid of the Dummyi and Dummyj...

Well, it almost does what I want. I get

Polymorphic Definition CatCat i j k := Category' (Category' i j) k.
Print CatCat. (* Polymorphic CatCat =
fun (i : Type (* Top.141 *)) (j : Type (* Top.142 *))
  (k : Type (* Top.140 *)) =>
Category' (* Top.139 Top.140 *) (Category' (* Top.141 Top.142 *) i j) k
     : Type (* Top.141 *) ->
       Type (* Top.142 *) -> Type (* Top.140 *) -> Type (* (Top.139)+1 *)
(* Top.139
   Top.140
   Top.141
   Top.142 |= Top.139 < Top.94
               Top.141 < Top.94
               Top.141 < Top.139
                *) *)

where I was hoping for it to end up with type Type (* max((Top.140)+1, max((Top.141)+1, (Top.142)+1)+1) *) or something (that is, a type entirely in terms of the types of i, j, and k).

from coq.

It's in general not possible because we maintain the invariant that only universe levels and not general universe expressions appear in the term. Hence sometimes me must keep a variable around because it would be substituted by a max() in the term. We don't want that as it would generate disjunctive constraints which make complexity of constraint checking much higher. However, having +n could be useful, we only have +1 right now, +2 is encoded by having an intermediary universe (139 here I think).

from coq.

I just realized (from ) that this universe polymorphism is a lot more powerful than I thought; the following type-checks:

Record Category := { Ob :> Type; Hom : Ob -> Ob -> Type }.
Record Functor (C D : Category) := { F0 :> C -> D ; F1 : forall s d, Hom C s d -> Hom D (F0 s) (F0 d) }.
Definition Cat : Category := {| Ob := Category ; Hom := Functor |}.

whereas I thought that the biggest change was the polymorphic flag and (optionally) polymorphic Definitions. (I'm not sure why I thought that, given that you wouldn't need a whole new algorithm to do that...)

Anyway, I don't think this feature is terribly important anymore, given that. Great work!

from coq.

Indeed, that's the main feature, and polymorphic definitions are necessary to make the polymorphism "go through" transparently.

-- Matthieu

Le 21 juin 2013 à 06:23, Jason Gross [email protected] a écrit :

I just realized (from ) that this universe polymorphism is a lot more powerful than I thought; the following type-checks:

Record Category := { Ob :> Type; Hom : Ob -> Ob -> Type }.
Record Functor (C D : Category) := { F0 :> C -> D ; F1 : forall s d, Hom C s d -> Hom D (F0 s) (F0 d) }.
Definition Cat : Category := {| Ob := Category ; Hom := Functor |}.
whereas I thought that the biggest change was the polymorphic flag and (optionally) polymorphic Definitions. (I'm not sure why I thought that, given that you wouldn't need a whole new algorithm to do that...)

Anyway, I don't think this feature is terribly important anymore, given that. Great work!

—
Reply to this email directly or view it on GitHub.

from coq.