Stream: Coq devs & plugin devs

Topic: Possible levels for qualities other than SProp, Prop, Set.


view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:05):

Matthieu gave at the Coq workshop examples of use of qualities (thanks!). If I understand correctly, when the quality is SProp, Prop or Set, as was asked, the levels are irrelevant. Would it then make sense to simplify the notation, such as, I don't know, being able to only write this:

Set Universe Polymorphism.
Definition id@{ s | u | } (A:Type@{s|u}) (x:A) := x.
Check id@{Prop}.

or that:

Check id@{Prop|}.

view this post on Zulip Gaëtan Gilbert (Sep 14 2024 at 14:06):

Set is not a quality
Type is a quality

view this post on Zulip Gaëtan Gilbert (Sep 14 2024 at 14:08):

Would it then make sense to simplify the notation, such as, I don't know, being able to only write this:

finding which levels are irrelevant when a quality is impredicative in general requires unfolding the definition
so I'm not sure what the precise meaning of such a notation would be

view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:08):

Set is a universe of the Type quality (at the bottom)?

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

Yep, Set = 0

view this post on Zulip Gaëtan Gilbert (Sep 14 2024 at 14:10):

Set is a universe level, which other levels are generally declared to be >= Set (except while checking template poly inductives)
Set is also a notation for Type@{Set}

view this post on Zulip Gaëtan Gilbert (Sep 14 2024 at 14:10):

probably we should rename the level to 0

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

Hugo Herbelin said:

Matthieu gave at the Coq workshop examples of use of qualities (thanks!). If I understand correctly, when the quality is SProp, Prop or Set, as was asked, the levels are irrelevant. Would it then make sense to simplify the notation, such as, I don't know, being able to only write this:

Set Universe Polymorphism.
Definition id@{ s | u | } (A:Type@{s|u}) (x:A) := x.
Check id@{Prop}.

or that:

Check id@{Prop|}.

That's also my main gripe with our handling of impredicative universes. It also shows up as "universe foo is unbound" during elaborations when one would have expected the universe to be set as 0 as you've been using Prop. However there does not seem to be an evident solution to that.

view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:13):

In the quality model, is there a place for subsingleton types, such as hProp or subsets of hProp such as (a predicative) Prop, i.e. a place where we can make a predicative form of Prop live (up to ensuring a truncation).

view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:16):

finding which levels are irrelevant when a quality is impredicative in general requires unfolding the definition

It can probably be an information attached to the universe signature of the constant?

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

You could analyse that u is only used with s, if all uses of u are linked with s = Prop | SProp, and u has no constraint, it could heuristically be set to 0, no?

view this post on Zulip Guillaume Melquiond (Sep 14 2024 at 14:20):

At the very least, _ could be accepted for an irrelevant level. (Or perhaps it already is?)

view this post on Zulip Guillaume Melquiond (Sep 14 2024 at 14:22):

And after testing, it actually is, which seems like a better style than writing foo everywhere.

view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:23):

In the quality model, is there a place for subsingleton types?

Maybe this is a wrong question as it is about h-level rather than size.

view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:31):

And after testing, it actually is, which seems like a better style than writing foo everywhere.

I tested too and it seems to generate a new universe at each new application.

view this post on Zulip Hugo Herbelin (Sep 14 2024 at 14:41):

In any cases, that was a very nice talk. I'll continue thinking about it offline.

view this post on Zulip Gaëtan Gilbert (Sep 14 2024 at 14:41):

_ is a hole regardless of if it's a term or a universe
leftover term holes produce an error ("cannot infer placeholder" etc)
leftover universe holes become new universes, except when using @{...} without + in which case they produce an error ("unbound universe")


Last updated: Oct 13 2024 at 01:02 UTC