Is it normal behavior that interactive processing seems to introduce universe variables while processing (quite normal) but not remove them when unprocessing? That is, if I do:

```
Set Printing Universes.
Check Type.
(* Type@{Foo.1}: Type@{Foo.1+1}*)
Check Type.
(* Type@{Foo.2}: Type@{Foo.2+1}*)
```

As expected, but if I now unprocess the file without killing coqtop, and reprocess the first Check, I get:

```
(* Type@{Foo.3}: Type@{Foo.3+1}*)
```

Not sure if it's an issue, but that surprised me.

(on 8.11.1)

(Also I'm discovering this whole Zulip thing, I hope creating a topic "Universes" in this stream is indeed the right way to go)

Yannick Zakowski said:

(Also I'm discovering this whole Zulip thing, I hope creating a topic "Universes" in this stream is indeed the right way to go)

Yep!

And to answer your question, AFAICT this is just the name process that doesn't get refreshed (it probably wouldn't take much to fix so that might be worth reporting) but the universe is not kept in the context, as shown by the command `Print Universes.`

Example:

```
$ rlwrap coqtop -noinit
Welcome to Coq 8.11.1 (January 1970)
Coq < Set Printing Universes.
Coq < Print Universes.
Prop < Set
Coq < Definition foo := Type.
foo is defined
Coq < Print Universes.
Prop < Set
Set < foo.u0
Coq < Reset foo.
Coq < Print Universes.
Prop < Set
```

I see, thanks for the answer! I'll create an issue later Today.

It's known behaviour.

It works that way because when universes get produced concurrently (`par:`

, vio, coqide async processing...) we need to avoid collisions, and the synchronization system doesn't have the ability to reset.

I have no clue how hard that would be to change, maybe STM people know more.

Oh I see. Is it still worth creating an issue to record the problem then or would it be just needless noise?

It is cosmetic, but does not help with debugging Universe issues

I'm trying to figure out how universes work in Coq, mainly about the notations Top.i, @ and the way Coq handles algebraic constraints on universes when one uses polymorphic functions.

I've found a couple of things in the documentation :

https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html

which seems to be a follow-up of this (I didn't find anything in-between):

https://coq.github.io/doc/master/refman/language/core/sorts.html

I'm considering the very beginning of the page on universe polymorphism, namely:

```
Definition identity {A : Type} (a : A) := a.
```

```
By default, constant declarations are monomorphic, hence the identity function declares a global universe (say Top.1) for its domain. Subsequently, if we try to self-apply the identity, we will get an error:
```

```
Fail Definition selfid := identity (@identity).
```

1) is there some sort of coercion on the universe annotation @ so that @{foo} takes the universe level of the term foo ?

2) What is a "global universe" Top.i ? Is it some sort of universe variable ?

3) Does Coq produce constraints along the way? For instance, with the identity function defined above, I guess that it is possible that, in the proof of Theorem Foo, Coq detects that identity lives in a higher universe than some function f. But if, just after, I prove another theorem, Theorem Bar, whose proof does not use Theorem Foo, may I use a proof term that would constrain f to live in a higher universe than identity, or will Coq be unhappy about that?

PS: I'm not sure if this question should be there or in the beginner thread. Please tell me if I should move it there

It's perfect like this! Thanks for asking about this @Pierre Vial.

I am far from being very knowledgeable about this stuff but I can still try to answer before the real experts come in.

But first, let me note that a lot of the syntax for manipulating universes was undocumented until recently (or only appeared here and there in examples). Sometimes, we've added the syntax, but not necessarily in the most appropriate location, or with the associated explanations, so there is still a big margin for progress and PRs are welcome :slight_smile:

From what I understand the `@{ }`

syntax can be quite confusing because depending on where it is used exactly, it doesn't take the same type of arguments.

Perhaps, I didn't find where the use of @(foo), instead of @{foo}, was described

`@{}`

has essentially two different uses: as a binder and as an application.

But in general, what you can find in there is not a term, rather a universe level. Cf. https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html#explicit-universes

Oh yes, `@(...)`

has nothing to do with `@{ ... }`

There is no @(foo) syntax for universes though...

In fact `@(foo)`

doesn't exist `@foo`

does but this is about implicit arguments.

So the use of `@`

in this example just makes things more confusing.

Huh, my bad

The Coq universe model is the following: first, you have a bunch of global names + contraints that floats around

everytime you write monomorphic code, you'll generate fresh names and constraints

(see also https://coq.github.io/doc/master/refman/addendum/universe-polymorphism.html#printing-universes to get the list of universes and constraints)

polymorphic definitions allow to make some code generic in the universes it creates

so, when you write `Definition foo@{i} := Type@{i}`

, there are no names nor constraints generated

locally to the definition, `i`

is a bound variable

introduced by the binder in `foo@{i}`

meanwhile, everytime you see `qux@{i}`

inside the body of `foo`

, it's a call to that bound variable

so, for instance, `Type@{i}`

refers to that `i`

variable introduced in the definition but doesn't bind anything in itself

does this make sense so far?

OK, so in my situation, Coq would be perfectly fine with the proofs of Theorems Foo and Bar, even if actually, the proof of Bar would use Foo ?

if you're in polymorphic mode, yes

in polymorphic mode, there is an ML-style implicit quantification occurring for universe variables

if you write `id`

as you described in polymorphic mode, set the printing of universes on, and `About id`

, you'll see it has a bound universe variable

and if I'm not in polymorphic mode ? (I would like to understand how it works before using universe polymorphism)

```
id@{Top.1} =
fun (A : Type@{Top.1}) (x : A) => x
: forall A : Type@{Top.1}, A -> A
(* Top.1 |= *)
```

if you're not in universe polymorphic mode, `id`

will have only one instance ever, so every time you add constraints to it they are present globally

so, `id id`

will fail

so that I wouldn't be able to prove Theorems Foo and Bar the way I suggested

Indeed.

Ok, it's what I wanted to understand. Thanks to you both!

Another related questions though: this means that, when I'm not in polymorphic mode, figuring out universe constraints is effectful ?

Definitely.

Great! Thanks again :)

This is why I believe that (barring unification) universe polymorphism is easier to understand.

Now, let me hijack this thread to ask what you both think would be the best way of presenting this stuff.

I agree that the syntax is very confusing, so this should be highlighted...

The Core language chapter introduces Sorts very early because this is the most central notion, but universes are only mentioned there and properly documented rather late.

Should there be more stuff in the section on Sorts? https://coq.github.io/doc/master/refman/language/core/sorts.html

Is it the right place to document the syntax of algebraic universes (currently the syntax is shown but it is barely explained).

I am not sure that the `Set / Type`

distinction is very relevant.

but I think it makes sense to have the syntax described here even if explained very lightly

What should we do about `Set`

is indeed something I've been wondering

The reason this is done this way is unfortunately purely historical...

The distinction only makes sense in set-impredicative Coq.

Yes, I know but how would you do it if you were to redo this from scratch?

Just not include `Set`

at all?

Yes.

Write in in the syntax, and mention *en passant* that this is a peculiarity

Could it introduce any limitation if we were to deprecate `Set`

except in `-set-impredicative`

mode?

but insisting so much on it is really counterproductive

there are quite a few people that use it to get a fixed universe level

Indeed! That was the kind of thing I was wondering about.

I think I remember that Thomas Braibant tried to remove `Set`

once.

But couldn't it be replaced by `Prop + 1`

?

Thomas Braibant did not have our current CI suite.

Replacing it is likely to create mayhem in unification though

Both from the point of view of functionality *and* efficiency

Disclaimer: I don't understand universe unification.

(I suspect that even @Matthieu Sozeau and @Gaëtan Gilbert only have a partial understanding of it)

BTW, what do you think of this: `Type@{Set}`

(this is `Set`

), `Type@{Prop}`

(this is `Prop`

), `Type@{SProp}`

(doesn't parse)?

In particular, the fact that algebraic universes are restricted in the place they can appear is going to be problematic.

Catastrophic idea syntax-wise, but practical.

I'd rather have had `Type@{set}`

and the like

Pierre-Marie Pédrot said:

In particular, the fact that algebraic universes are restricted in the place they can appear is going to be problematic.

Is this the case because of an implementation limitation.

to have a clear separation between sorts and universe variables

Pierre-Marie Pédrot said:

I'd rather have had

`Type@{set}`

and the like

It might not be too late to change this.

That's a syntactic consideration, so irrelevant and open to bikeshedding

Well syntax can help or hinder documentation.

Regarding algebraic, the problem is that if you want them everywhere then you get at least NP-hardness

OK, I get it. Shouldn't it still be authorized, but with a warning? Maybe users would just not care about the warnings and developers would end up in a hell of performance debugging and heuristics though...

That would require rewriting universe unification completely IIUC

Essentially reimplementing a SAT-solver

OK then forget it.

Coming back to `Type@{Prop}`

(works) and `Type@{SProp}`

(doesn't), does this means that the sort `Prop`

corresponds to a particular universe but the sort `SProp`

doesn't?

My suggestion (from a shallow point of view) for the Universe Polymorphism section would be to start with explaining the Type@{i} are handled. Starting with the (failed) self-identify is very appropriated, but my impression is that it would be better not to make it follow an example with universe polymorphism (that is, selfpid.)

The selfidentity is very interesting, because it is the epitomy of something that is not allowed in a predicative setting. However, I found the explanations you gave me enlightening, especially the part about the effectfulness of monorphic universe level inference and the problems it may cause while proving different statements. So I think they should come before introducing selfpid and Top.i.

For instance, the phrase "global universe" pops in just at the beginning of the pag without context, and just a few lines below, one reads:

```
A universe polymorphic identity function binds its domain universe level at the definition level instead of making it global.
```

and I think the way universes are globally bound shoud be addressed before

@Théo Zimmermann looks more like an oversight to me, but there might be technical reasons I am not aware of

Thanks @Pierre Vial. Should this section be renamed into just "Universes" BTW? Especially, if it starts by explaining monomorphic universes better and then moves on to universe polymorphism.

@Pierre Vial this has nothing to do with impredicativity : it's just that you duplicate `id`

at every call

@Pierre-Marie Pédrot He did not say "impredicativity" but "predicative setting".

A possibility would be to put a small subsection presenting monomorphic universes just after the typing rules, completing

https://coq.github.io/doc/master/refman/language/core/sorts.html

but yes, this could probably be renamed universes, since it does not tackle only universe polymorphism currently.

He did not say "impredicativity" but "predicative setting".

My point is that this is orthogonal to impredicativity of Coq. Self-application *is* predicative in polymorphic mode, it's just that the two terms are not the same.

CIC + univpoly is a conservative extension of CIC actually

A possibility would be to put a small subsection presenting monomorphic universes just after the typing rules, completing

https://coq.github.io/doc/master/refman/language/core/sorts.html

Yes, basically I've been wondering whether universes should be explained early in the section on sorts or only quite late, and it seems like that would be too much if we explained everything early, but it seems relatively important the still sketch the basics.

A nuance that could be highlighted :)

You sure have to say something about sorts *before* giving the typing rules, but because of typical ambiguity, it seems to me useful to say more about universes after you have given them

Théo Zimmermann said:

But couldn't it be replaced by

`Prop + 1`

?

That's essentially what Lean does (at least if you consider that Set is the universe of bool/nat/etc)

Of course Lean doesn't have cumulativity so the universe problems they get are different (nothing to minimize for instance)

Théo Zimmermann said:

OK, I get it. Shouldn't it still be authorized, but with a warning? Maybe users would just not care about the warnings and developers would end up in a hell of performance debugging and heuristics though...

I think it may be a good idea to turn the "algebraic on the right" anomaly and any other algebraic anomaly into regular errors, that's basically "tolerating " algebraics in arbitrary positions

As PMP said having algebraics in arbitrary positions with a complete inference is NP harder

Why is this not allowed? I'm posting here because I'm assuming it is a positivity argument

```
Inductive d : Type :=
| C : forall (A : Type -> Type), A -> d.
(*
Error: In environment
d : Type
A : Type -> Type
The term "A" has type "Type -> Type"
which should be Set, Prop or Type.
*)
```

`A`

is not a type so it doesn't make sense to talk about "values of type `A`

" which would be arguments of a function "`A -> d`

"

`Type -> Type`

is a type though

~~it's not~~

uh, I mean, that doesn't make `A`

a type

right, but still it means that A are functions, why can't a constructor take take functions as arguments? I don't quite get it

Another way to say this is that for (A -> B) to typecheck you need `A : s`

and `B : s'`

where s and s' are sorts. `Type -> Type`

is not a sort.

However, `A X`

for any `X : Type`

is of type `Type`

, a sort. So you could have:

```
Inductive d : Type :=
| C : forall (A : Type -> Type), (forall X, A X) -> d.
or
Inductive d : Type :=
| C : forall (A : Type -> Type) (X : Type), A X -> d.
But not:
Inductive d : Type :=
| C : forall (A : Type -> Type), (fun x => A x) -> d.
```

Makes sense, are there other edges on the lambda cube that `s`

and `s'`

wouldn't need to be sorts?

@Pedro Abreu put yet another way, “A are functions” is not true in the way you’d need; if `A : Type → Type`

, it doesn’t mean that `x : A`

makes sense — an `A`

is a function that produces types, not a type

I also think that `s`

and `s’`

must always be sorts — vertexes of the lambda cube/PTSes change which are the sorts, or forbid sort combinations.

@Paolo G. Giarrusso I think that's what I was having trouble understanding. "Functions that produces types" are not types here. Very enlightening, thanks.

(Also, technically, modern Coq does not fit in the lambda cube — you need to generalize to PTSes, and that only lets you talk about the universe structure)

Last updated: Jun 23 2024 at 23:01 UTC