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: Oct 13 2024 at 01:02 UTC