Stream: Coq devs & plugin devs

Topic: Adding Sorts


view this post on Zulip Thomas Lamiaux (Sep 14 2024 at 14:13):

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 ?

view this post on Zulip Théo Zimmermann (Sep 16 2024 at 14:42):

*Rocq 9, not Rocq 1

view this post on Zulip Matthieu Sozeau (Sep 16 2024 at 14:49):

There is no subsorting relation right now. Not sure if this is a good idea :)

view this post on Zulip Mario Carneiro (Sep 16 2024 at 14:55):

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?

view this post on Zulip Mario Carneiro (Sep 16 2024 at 14:55):

certainly that would be a lot less notationally cumbersome

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:02):

At least in the typing rules it makes a lot of sense to separate the two.

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:02):

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).

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:03):

From a notational perspective, I see your point that it's quite verbose.

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:07):

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

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:07):

i.e. universes form a partial order and level variables quantify over the elements of this partial order

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:08):

Sure. But I mean, there is a practicality in dissociating the two I think?

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:09):

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

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:09):

You could also want to be polymorphic in the sort but not the level? Maybe. :sweat_smile:

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:10):

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

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:11):

to me it looks like coq belatedly getting something equivalent to lean's universe polymorphism, only worse because of path-dependent reasons

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:13):

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

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:14):

especially since coq is known for having issues keeping universe inference under control

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:17):

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.

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:20):

I'm asserting that you can have all the same things, just with less variables

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:20):

If you want one Prop, you can have that, if you want a hierarchy you can have that too

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:20):

you are just changing the domain of the quantification of the variables

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:22):

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

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:23):

I agree, I just mean that the universe of a Π\Pi type is now less uniform? It has to rely on the rules of a PTS right?

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:23):

in the case of Coq's actual universe hierarchy there is only one such constraint you need, namely isType(u)

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:24):

What even is the universe of a pi type in 8.20 sort polymorphic world?

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:24):

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.

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:24):

as with lean, the way to encode this is to have a function on universe variables with the definition you want

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:25):

we may as well have named imax as theUniverseOfPi(u,v)

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:25):

Admittedly this is my own perspective on the matter, and this might not reflect what is implemented in Coq currently.

view this post on Zulip Théo Winterhalter (Sep 16 2024 at 15:26):

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.

view this post on Zulip Gaëtan Gilbert (Sep 16 2024 at 15:27):

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

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:28):

well imax doesn't just work on ground univs, it has normalization rules for open terms too

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:29):

but a lot of the time it is just an expression which doesn't reduce

view this post on Zulip Mario Carneiro (Sep 16 2024 at 15:30):

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

view this post on Zulip Matthieu Sozeau (Sep 17 2024 at 09:36):

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

view this post on Zulip Matthieu Sozeau (Sep 17 2024 at 09:39):

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