Yannick Zakowski (May 08 2020 at 15:35): 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)
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!
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
I see, thanks for the answer! I'll create an issue later Today.
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.
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
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
Théo Zimmermann (May 29 2020 at 13:29):It's perfect like this! Thanks for asking about this @Pierre Vial.
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.
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:
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.
Pierre Vial (May 29 2020 at 13:36):Perhaps, I didn't find where the use of @(foo), instead of @{foo}, was described
Pierre-Marie Pédrot (May 29 2020 at 13:36):@{} has essentially two different uses: as a binder and as an application.
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
Théo Zimmermann (May 29 2020 at 13:36):Oh yes, @(...) has nothing to do with @{ ... }
Pierre-Marie Pédrot (May 29 2020 at 13:36):There is no @(foo) syntax for universes though...
Théo Zimmermann (May 29 2020 at 13:37):In fact @(foo) doesn't exist @foo does but this is about implicit arguments.
Théo Zimmermann (May 29 2020 at 13:37):So the use of @ in this example just makes things more confusing.
Pierre Vial (May 29 2020 at 13:38):Huh, my bad
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
Pierre-Marie Pédrot (May 29 2020 at 13:38):everytime you write monomorphic code, you'll generate fresh names and constraints
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)
Pierre-Marie Pédrot (May 29 2020 at 13:39):polymorphic definitions allow to make some code generic in the universes it creates
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
Pierre-Marie Pédrot (May 29 2020 at 13:40):locally to the definition, i is a bound variable
Pierre-Marie Pédrot (May 29 2020 at 13:40):introduced by the binder in foo@{i}
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
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
Pierre-Marie Pédrot (May 29 2020 at 13:42):does this make sense so far?
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 ?
Pierre-Marie Pédrot (May 29 2020 at 13:46):if you're in polymorphic mode, yes
Pierre-Marie Pédrot (May 29 2020 at 13:46):in polymorphic mode, there is an ML-style implicit quantification occurring for universe variables
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
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)
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 |= *)
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
Pierre-Marie Pédrot (May 29 2020 at 13:48):so, id id will fail
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
Pierre-Marie Pédrot (May 29 2020 at 13:49):Indeed.
Pierre Vial (May 29 2020 at 13:49):Ok, it's what I wanted to understand. Thanks to you both!
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 ?
Pierre-Marie Pédrot (May 29 2020 at 13:50):Definitely.
Pierre Vial (May 29 2020 at 13:50):Great! Thanks again :)
Pierre-Marie Pédrot (May 29 2020 at 13:50):This is why I believe that (barring unification) universe polymorphism is easier to understand.
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.
Pierre-Marie Pédrot (May 29 2020 at 13:53):I agree that the syntax is very confusing, so this should be highlighted...
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.
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
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).
Pierre-Marie Pédrot (May 29 2020 at 13:56):I am not sure that the Set / Type distinction is very relevant.
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
Théo Zimmermann (May 29 2020 at 13:57):What should we do about Set is indeed something I've been wondering
Pierre-Marie Pédrot (May 29 2020 at 13:58):The reason this is done this way is unfortunately purely historical...
Pierre-Marie Pédrot (May 29 2020 at 13:58):The distinction only makes sense in set-impredicative Coq.
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?
Théo Zimmermann (May 29 2020 at 13:58):Just not include Set at all?
Pierre-Marie Pédrot (May 29 2020 at 13:58):Yes.
Pierre-Marie Pédrot (May 29 2020 at 13:59):Write in in the syntax, and mention en passant that this is a peculiarity
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?
Pierre-Marie Pédrot (May 29 2020 at 13:59):but insisting so much on it is really counterproductive
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
Théo Zimmermann (May 29 2020 at 14:00):Indeed! That was the kind of thing I was wondering about.
Pierre-Marie Pédrot (May 29 2020 at 14:00):I think I remember that Thomas Braibant tried to remove Set once.
Théo Zimmermann (May 29 2020 at 14:00):But couldn't it be replaced by Prop + 1?
Théo Zimmermann (May 29 2020 at 14:00):Thomas Braibant did not have our current CI suite.
Pierre-Marie Pédrot (May 29 2020 at 14:01):Replacing it is likely to create mayhem in unification though
Pierre-Marie Pédrot (May 29 2020 at 14:01):Both from the point of view of functionality and efficiency
Pierre-Marie Pédrot (May 29 2020 at 14:02):Disclaimer: I don't understand universe unification.
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)
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)?
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.
Pierre-Marie Pédrot (May 29 2020 at 14:03):Catastrophic idea syntax-wise, but practical.
Pierre-Marie Pédrot (May 29 2020 at 14:04):I'd rather have had Type@{set} and the like
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.
Pierre-Marie Pédrot (May 29 2020 at 14:04):to have a clear separation between sorts and universe variables
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.
Pierre-Marie Pédrot (May 29 2020 at 14:05):That's a syntactic consideration, so irrelevant and open to bikeshedding
Théo Zimmermann (May 29 2020 at 14:05):Well syntax can help or hinder documentation.
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
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...
Pierre-Marie Pédrot (May 29 2020 at 14:06):That would require rewriting universe unification completely IIUC
Pierre-Marie Pédrot (May 29 2020 at 14:07):Essentially reimplementing a SAT-solver
Théo Zimmermann (May 29 2020 at 14:07):OK then forget it.
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?
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
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
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.
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
Théo Zimmermann (May 29 2020 at 14:12):@Pierre-Marie Pédrot He did not say "impredicativity" but "predicative setting".
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
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.
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.
Pierre-Marie Pédrot (May 29 2020 at 14:20):CIC + univpoly is a conservative extension of CIC actually
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.
Pierre Vial (May 29 2020 at 14:21):A nuance that could be highlighted :)
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
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)
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
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.
*)
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"
Pedro Abreu (Jun 18 2020 at 18:20):Type -> Type is a type though
Li-yao (Jun 18 2020 at 18:20):it's not
Li-yao (Jun 18 2020 at 18:21):uh, I mean, that doesn't make A a type
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
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.
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.
Makes sense, are there other edges on the lambda cube that s and s' wouldn't need to be sorts?
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
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.
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.
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: Oct 13 2024 at 01:02 UTC