HoTT
Feature Request: Supporting explicit universe level variables
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?
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
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.
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 *) }
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).
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).
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!
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.