Will the possibility of adding sorts be part of Rocq 1 which , from what I understood should arrive around new years / mars ?
Will it be possible to add subtyping, like I add U + univalence and I declare Type_i <= U_i ?
*Rocq 9, not Rocq 1
There is no subsorting relation right now. Not sure if this is a good idea :)
I don't see the advantage of having two different axes for a universe level. Why not have a variable which represents the pair? In fact, isn't that exactly what Coq used to do?
certainly that would be a lot less notationally cumbersome
At least in the typing rules it makes a lot of sense to separate the two.
Say you have a predicative Prop
then I guess Prop i
lives in Type (i + 1)
so the separation is useful. Also the level of a dependent product depends only on the levels, but not the kinds of universes (or qualities, or sorts).
From a notational perspective, I see your point that it's quite verbose.
I mean, you can have a level that means Prop i
and a level that means Type (i+1)
and the first one is <
the second one; this doesn't stop you from having two universe hierarchies if you want
i.e. universes form a partial order and level variables quantify over the elements of this partial order
Sure. But I mean, there is a practicality in dissociating the two I think?
The only thing is that you may want to have restrictions that a sort is only of the form Type i
and not Prop
or vice versa, which is what is done in the current system by specifying the sort variable but not the level variable
You could also want to be polymorphic in the sort but not the level? Maybe. :sweat_smile:
you might want to have an arbitrary universe which is contained in a specified one, but that's basically already covered by level inequality constraints
to me it looks like coq belatedly getting something equivalent to lean's universe polymorphism, only worse because of path-dependent reasons
I will grant that having level 0 be special magic, and using the imax u v = if v = 0 then 0 else max u v
function to define pi types, is a bit weird, but doubling the number of universe variables in the average piece of code (which cares about none of them) seems worse
especially since coq is known for having issues keeping universe inference under control
Yeah, I agree that having Prop i = Prop j
is ok on the meta-theory maybe (?) but in practice you really want nothing. Somehow just having an order works, but it feels weird to me not to be able to factorise the max which is (almost) always going to be the same thing.
I'm asserting that you can have all the same things, just with less variables
If you want one Prop, you can have that, if you want a hierarchy you can have that too
you are just changing the domain of the quantification of the variables
if you had two hierarchies and wanted to say that u
is a Prop universe (which would normally show up as a use of Prop i
in the concrete syntax), this would be a variable u
plus a constraint isProp(u)
. This constraint is not an inequality constraint, it would be handled as its own thing
I agree, I just mean that the universe of a type is now less uniform? It has to rely on the rules of a PTS right?
in the case of Coq's actual universe hierarchy there is only one such constraint you need, namely isType(u)
What even is the universe of a pi type in 8.20 sort polymorphic world?
Whereas if you separate the two you can say forall (x : A), B
has type V (max i j)
where A : U i
and B : V j
.
as with lean, the way to encode this is to have a function on universe variables with the definition you want
we may as well have named imax
as theUniverseOfPi(u,v)
Admittedly this is my own perspective on the matter, and this might not reflect what is implemented in Coq currently.
I think we agree, I'm just saying it seems to be more specialised with the two. But maybe that doesn't help in any way, with a bigger cost as you suggest.
Mario Carneiro said:
as with lean, the way to encode this is to have a function on universe variables with the definition you want
with cumulativity the definition on ground univs is not the only thing that matters, you also need to be able to handle constraints
well imax
doesn't just work on ground univs, it has normalization rules for open terms too
but a lot of the time it is just an expression which doesn't reduce
the "definition" I gave of the imax
function is only in the semantics, in reality it is implemented as a bunch of normalization rules consistent with that interpretation
Mario Carneiro said:
I don't see the advantage of having two different axes for a universe level. Why not have a variable which represents the pair? In fact, isn't that exactly what Coq used to do?
The main usability issue in that case is when one wants to share universe levels but not sorts, i.e. you'd have to write constraints like:
foo@{u v | u.level = v.level) : (A : Type@{u}} {B : Type@{v}}, ...
. The advantage would be that (Prop|SProp).level could be set to 0 however.
Same problem when you want to share the sort but not the levels (the more common case).
The forall typing rule would be (forall (a : A : Type@{u}), B : Type@{v}) : Type@{(v.sort | max (u.level, v.level))}
with (Prop, _) = (Prop, 0) presumably
I tried to advocate for trying that presentation but in the end the notational burden seems worst for "packed" universes
Last updated: Oct 13 2024 at 01:02 UTC