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.
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.
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.
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
What do you mean? That if you are lucky it is? Fine, but this is not enough for me.
@Hugo Herbelin @Matthieu Sozeau any idea why we store an algebraic there? Are there other places where we do?
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
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)
.
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)?
also when putting algebraics in terms they can appear in conversion problems
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.
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?
Yes
(Adding algebraics to instances)
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
I'm looking at providing a specification of the system with u + n
universes in MetaCoq.
I don't understand what "taking the successor" means
And a reference implementation.
Universe.succ basically. When you want to compute the succcessor of u
to build u+1
As a user I'd be happy with having algebraics everywhere, but I do believe we have to be superduper careful performancewise
We already have too many ways to trigger exponential blowup in the kernel...
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
Does Bender et al algorithm (the reference mentioned in file acyclicGraph.ml
) support weighted edges?
In the meantime, what about turning the anomaly into an error (e.g. as in #10425)?
Jacques-Henri told me it should be possible at some point, I'd have to check the paper again.
I'm fine with #10425 indeed
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
, ...
AFAIK identity in hott is supposed to be at u
not u-1
I don't think HoTT has that either, equality lives in the same universe as the type on which it is based.
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.
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?
Oh, and thanks for your answers
Yes, refresh_universes
with (Some false)
so that the universe level you get is higher than the inductive type/constant type will work.
Certainly a sum type would be self-explanatory here, sorry for that
And no, algebraics can only appear at the end of arities, in types (barring bugs)
OK thanks!
Last updated: Jun 05 2023 at 09:01 UTC