Stream: Coq users

Topic: Universes


view this post on Zulip Yannick Zakowski (May 08 2020 at 15:35):

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)

view this post on Zulip Théo Zimmermann (May 08 2020 at 15:37):

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!

view this post on Zulip Théo Zimmermann (May 08 2020 at 15:42):

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

view this post on Zulip Yannick Zakowski (May 08 2020 at 15:44):

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

view this post on Zulip Gaëtan Gilbert (May 08 2020 at 20:14):

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.

view this post on Zulip Yannick Zakowski (May 08 2020 at 20:56):

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

view this post on Zulip Pierre Vial (May 29 2020 at 13:26):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:29):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:29):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:31):

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:

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:34):

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.

view this post on Zulip Pierre Vial (May 29 2020 at 13:36):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:36):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:36):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:36):

Oh yes, @(...) has nothing to do with @{ ... }

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:36):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:37):

In fact @(foo) doesn't exist @foo does but this is about implicit arguments.

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:37):

So the use of @ in this example just makes things more confusing.

view this post on Zulip Pierre Vial (May 29 2020 at 13:38):

Huh, my bad

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:38):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:38):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:38):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:39):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:40):

so, when you write Definition foo@{i} := Type@{i}, there are no names nor constraints generated

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:40):

locally to the definition, i is a bound variable

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:40):

introduced by the binder in foo@{i}

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:41):

meanwhile, everytime you see qux@{i} inside the body of foo, it's a call to that bound variable

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:41):

so, for instance, Type@{i} refers to that i variable introduced in the definition but doesn't bind anything in itself

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:42):

does this make sense so far?

view this post on Zulip Pierre Vial (May 29 2020 at 13:45):

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 ?

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:46):

if you're in polymorphic mode, yes

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:46):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:47):

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

view this post on Zulip Pierre Vial (May 29 2020 at 13:47):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:47):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:48):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:48):

so, id id will fail

view this post on Zulip Pierre Vial (May 29 2020 at 13:49):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:49):

Indeed.

view this post on Zulip Pierre Vial (May 29 2020 at 13:49):

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

view this post on Zulip Pierre Vial (May 29 2020 at 13:50):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:50):

Definitely.

view this post on Zulip Pierre Vial (May 29 2020 at 13:50):

Great! Thanks again :)

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:50):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:52):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:53):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:54):

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.

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:55):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:55):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:56):

I am not sure that the Set / Type distinction is very relevant.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:56):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:57):

What should we do about Set is indeed something I've been wondering

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:58):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:58):

The distinction only makes sense in set-impredicative Coq.

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:58):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:58):

Just not include Set at all?

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:58):

Yes.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:59):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 13:59):

Could it introduce any limitation if we were to deprecate Set except in -set-impredicative mode?

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:59):

but insisting so much on it is really counterproductive

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 13:59):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:00):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:00):

I think I remember that Thomas Braibant tried to remove Set once.

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:00):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:00):

Thomas Braibant did not have our current CI suite.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:01):

Replacing it is likely to create mayhem in unification though

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:01):

Both from the point of view of functionality and efficiency

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:02):

Disclaimer: I don't understand universe unification.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:02):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:03):

BTW, what do you think of this: Type@{Set} (this is Set), Type@{Prop} (this is Prop), Type@{SProp} (doesn't parse)?

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:03):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:03):

Catastrophic idea syntax-wise, but practical.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:04):

I'd rather have had Type@{set} and the like

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:04):

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.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:04):

to have a clear separation between sorts and universe variables

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:04):

Pierre-Marie Pédrot said:

I'd rather have had Type@{set} and the like

It might not be too late to change this.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:05):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:05):

Well syntax can help or hinder documentation.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:05):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:06):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:06):

That would require rewriting universe unification completely IIUC

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:07):

Essentially reimplementing a SAT-solver

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:07):

OK then forget it.

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:09):

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?

view this post on Zulip Pierre Vial (May 29 2020 at 14:09):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:10):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:11):

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.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:11):

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

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:12):

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

view this post on Zulip Pierre Vial (May 29 2020 at 14:12):

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

view this post on Zulip Pierre Vial (May 29 2020 at 14:14):

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

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:19):

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.

view this post on Zulip Pierre-Marie Pédrot (May 29 2020 at 14:20):

CIC + univpoly is a conservative extension of CIC actually

view this post on Zulip Théo Zimmermann (May 29 2020 at 14:21):

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.

view this post on Zulip Pierre Vial (May 29 2020 at 14:21):

A nuance that could be highlighted :)

view this post on Zulip Pierre Vial (May 29 2020 at 14:22):

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

view this post on Zulip Gaëtan Gilbert (May 29 2020 at 14:32):

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)

view this post on Zulip Gaëtan Gilbert (May 29 2020 at 14:34):

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

view this post on Zulip Pedro Abreu (Jun 18 2020 at 18:13):

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

view this post on Zulip Li-yao (Jun 18 2020 at 18:19):

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"

view this post on Zulip Pedro Abreu (Jun 18 2020 at 18:20):

Type -> Type is a type though

view this post on Zulip Li-yao (Jun 18 2020 at 18:20):

it's not

view this post on Zulip Li-yao (Jun 18 2020 at 18:21):

uh, I mean, that doesn't make A a type

view this post on Zulip Pedro Abreu (Jun 18 2020 at 18:22):

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

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 18:22):

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.

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 18:25):

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.

view this post on Zulip Pedro Abreu (Jun 18 2020 at 18:29):

Makes sense, are there other edges on the lambda cube that s and s' wouldn't need to be sorts?

view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 18:30):

@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

view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 18:32):

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.

view this post on Zulip Pedro Abreu (Jun 18 2020 at 18:32):

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

view this post on Zulip Paolo Giarrusso (Jun 18 2020 at 18:33):

(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: Feb 06 2023 at 11:03 UTC