Enrico Tassi (Oct 30 2020 at 17:42): Enrico Tassi (Oct 30 2020 at 17:42):My intuition about algebraic unvierses is that they are computed while type checking, but then they are discarded. Indeed they don't have a name and they are not first class w.r.t. the constraint system (e.g. they cannot occur on the right).
While adding support for universe polymorphism to Elpi I discovered that, at least inductive types, are stored in the environment with potentially an algebraic as their sort. Eg
Coq < Print list.
Inductive list (A : Type@{list.u0}) : Type@{max(Set,list.u0)} :=
nil : list A | cons : A -> list A -> list A
(* {list.u0} |= *)
I'd like to know why and if it would makes sense to put a non algebraic universe there (in Coq, or at least in Elpi's API).
The point is that I see the env as a source of good data (as in safe to use), but here the sort of the inductive is not.
Enrico Tassi (Oct 30 2020 at 17:45):For example one bug I had to fix in my code is that the parametricity translation was doing something like (transposed to ocaml)
match ty with
| Sort as t -> Prod ... (Prod... t)
and this is "dangerous" since the term you obtain may not be type checked. The fix is to not reuse t but put a fresh universe and then type check the term, which is also fine, but not exactly the kind of API I dream of.
Enrico Tassi (Oct 30 2020 at 18:19):To clarify. A term may or may not type check, and that is fine. But a term containing al algebraic universe cannot be type checked, you get an error that is really telling you the thing you passed is outside of the domain of typecheck, like Rel -1 or Var ""... Finding such a term in the env is quite odd to me.
Gaëtan Gilbert (Oct 30 2020 at 18:21):But a term containing al algebraic universe cannot be type checked, you get an error that is really telling you the thing you passed is outside of the domain of typecheck
that's no true in general
Enrico Tassi (Oct 30 2020 at 18:24):What do you mean? That if you are lucky it is? Fine, but this is not enough for me.
Enrico Tassi (Nov 02 2020 at 09:18):@Hugo Herbelin @Matthieu Sozeau any idea why we store an algebraic there? Are there other places where we do?
Gaëtan Gilbert (Nov 02 2020 at 09:31):types of inductives and constants can be of the form forall ..., Type@{algebraic} (with no algebraic in the forall domains)
bugs and using the algebraic syntax may lead to algebraics appearing elsewhere
Hugo Herbelin (Nov 02 2020 at 10:05):Any occurrence of max(u,v) can be seen as a compact abbreviation for the unique global w such that u ≤ w and v ≤ w and which is minimal for that. And similarly, any u+n can be seen as a compact abbreviation for some globals w1... wn such that u < w1 < ... < wn, with wn in place of u+n and minimal for that.
The point is that a constraint max(u,v) ≤ z can be reduced to v ≤ z and u ≤ z, and a constraint u + 1 ≤ z to u < z. These are the constraints which we get when typing a term where algebraic universes occur only in the codomain.
Conversely, general constraints of the form z ≤ max(u,v) would require a disjunction and this is why they are rejected. Since such constraints are produced by application of an argument to a function whose codomain has a max, this is why max is forbidden in codomains.
I don't know either how general constraints of the form z ≤ u + n could be treated (but maybe can the acyclicity check be done on a graph which contains such algebraic expressions, I actually did not think about it).
Note that we would still be able to resolve u ≤ max(u,v) without requiring a disjunction, and not failing on such constraint. We could also make an arbitrary choice and resolve z ≤ max(u,v) by requiring z ≤ u.
Are there other places [than
Inductive] where we do?
We do in Definition f (X:Type) := Type. where the type is some u + 1.
In theory, I guess we could also in definitions of the forms Definition f (b:bool) := if b then Type else Type., as using such definition will not give rise to constraints of the form z ≤ max(u,v).
Gaëtan Gilbert (Nov 02 2020 at 10:16):as using such definition will not give rise to constraints of the form z ≤ max(u,v).
what about when you check the branches against the return annotation (which has the algebraic)?
Gaëtan Gilbert (Nov 02 2020 at 10:17):also when putting algebraics in terms they can appear in conversion problems
Matthieu Sozeau (Nov 02 2020 at 10:59):I believe a better solution would be, as Hugo suggest, to stop treating algebraics specially. In the kernel this means being able to check constraints of the form max (u1+n,...) <= max(v1+k,...) which should entirely be possible (albeit maybe a bit less efficient if there are a lot of <= max() constraints). One could take the succcessor of any universe and no longer get the "algebraic-on-the-right" error or have to deal with the distinction between "safe/typeable" terms and non-typeable arities. The universe inference part of elaboration would have to deal with l <= max(u, v) constraints however. It could be modified to fail if these don't have unique solutions (e.g. are not already implied by an l <= u or l <= v (or u <=/>= v) constraint), asking the user to provide a universe annotation/explicit constraint. I suspect adding algebraics could reduce tremendously the number of generated universes and constraints for universe-polymorphic definitions.
Gaëtan Gilbert (Nov 02 2020 at 11:23):The kernel already checks constraints involving algebraics, see ugraph.check_leq
One could take the succcessor of any universe and no longer get the "algebraic-on-the-right" error
what does this mean?
I suspect adding algebraics could reduce tremendously the number of generated universes and constraints for universe-polymorphic definitions.
Adding algebraics to instances?
Matthieu Sozeau (Nov 02 2020 at 11:24):Yes
Matthieu Sozeau (Nov 02 2020 at 11:24):(Adding algebraics to instances)
Matthieu Sozeau (Nov 02 2020 at 11:25):Indeed, it's easy to check, and taking the successor is just adding 1. But the graph currently does not handle l <= u+1 correctly
Matthieu Sozeau (Nov 02 2020 at 11:27):I'm looking at providing a specification of the system with u + n universes in MetaCoq.
Gaëtan Gilbert (Nov 02 2020 at 11:27):I don't understand what "taking the successor" means
Matthieu Sozeau (Nov 02 2020 at 11:27):And a reference implementation.
Matthieu Sozeau (Nov 02 2020 at 11:28):Universe.succ basically. When you want to compute the succcessor of u to build u+1
Pierre-Marie Pédrot (Nov 02 2020 at 11:28):As a user I'd be happy with having algebraics everywhere, but I do believe we have to be superduper careful performancewise
Pierre-Marie Pédrot (Nov 02 2020 at 11:29):We already have too many ways to trigger exponential blowup in the kernel...
Matthieu Sozeau (Nov 02 2020 at 11:37):Yes, this certainly has to be experimented with. It might also bring perforrmance gains by changing many l <= u constraints into l <= max(...,l,..) constraints
Hugo Herbelin (Nov 02 2020 at 11:56):Does Bender et al algorithm (the reference mentioned in file acyclicGraph.ml) support weighted edges?
Hugo Herbelin (Nov 02 2020 at 12:07):In the meantime, what about turning the anomaly into an error (e.g. as in #10425)?
Matthieu Sozeau (Nov 02 2020 at 12:15):Jacques-Henri told me it should be possible at some point, I'd have to check the paper again.
Matthieu Sozeau (Nov 02 2020 at 12:16):I'm fine with #10425 indeed
Hugo Herbelin (Nov 02 2020 at 12:51):In some sense, we would also need u - 1, for instance to type eq in HoTT (with -indices-matter), where we would like to have @eq Prop and @eq Set in Prop, @eq Type@{1} in Set, ...
Gaëtan Gilbert (Nov 02 2020 at 13:12):AFAIK identity in hott is supposed to be at u not u-1
Matthieu Sozeau (Nov 02 2020 at 13:45):I don't think HoTT has that either, equality lives in the same universe as the type on which it is based.
Matthieu Sozeau (Nov 02 2020 at 13:49):Also, I think truncation levels should stay different from universe levels in general. The circle in Set certainly does not have a proof-irrelevant equality.
Enrico Tassi (Nov 02 2020 at 14:25):Let me make my question more precise. I'd like to have a safe API now, where safe means that one can ask to the system the type of list and add a universe constraint using any subterm of the type of list on the right.
I can look for algebraics in any mutual inductive body (the datatype in env) and, as @Gaëtan Gilbert says, and put a fresh variable in the target plus some constraints as @Hugo Herbelin explains.
I also understood I have to patch the output of Typeops.type_of_global_in_context since also constants can have algebraics in their type.
I can do the same thing with the output of pretyping/typing or pretyping/pretype if it is always possible to do the replacement.
IMaybe I found an API I could just call, Evarsolve.refresh_universe ~onlyalg:true sigma t, but I don't get the documentation of the bool option. Eg, how should I call it?
val refresh_universes :
?status:Evd.rigid ->
?onlyalg:bool (* Only algebraic universes *) ->
?refreshset:bool ->
(* Also refresh Prop and Set universes, so that the returned type can be any supertype
of the original type *)
bool option (* direction: true for levels lower than the existing levels *) ->
env -> evar_map -> types -> evar_map * types
Anything else? Can algebraics occur in the body of constants?
Enrico Tassi (Nov 02 2020 at 14:26):Oh, and thanks for your answers
Matthieu Sozeau (Nov 02 2020 at 14:41):Yes, refresh_universes with (Some false) so that the universe level you get is higher than the inductive type/constant type will work.
Matthieu Sozeau (Nov 02 2020 at 14:41):Certainly a sum type would be self-explanatory here, sorry for that
Matthieu Sozeau (Nov 02 2020 at 14:42):And no, algebraics can only appear at the end of arities, in types (barring bugs)
Enrico Tassi (Nov 02 2020 at 15:13):OK thanks!
Last updated: Jun 05 2023 at 09:01 UTC