Stream: Elpi users & devs

Topic: purge_algebraic_universes

Enrico Tassi (Jun 30 2023 at 11:26):

@Enzo Crance if I recall correctly you disabled this piece of code, but I don't recall why exactly. I'm here with @Gaëtan Gilbert which does something similar in his Lean exporter as well. Can you provide an example where purging algebraics is bad?

Enzo Crance (Jun 30 2023 at 12:54):

I needed a bit of time to remember why I had commented this code in the first place.

It seems to be at least called on global reference declarations coming from Coq. For example, the following declaration of list will be displayed with 2 universes in Elpi through coq.env.indt(-decl), as the output sort of the inductive will be replaced with a Type@{u1} and a constraint on the fresh u1.

Inductive list@{u} (A : Type@{u}) : Type@{max(Set,u)} :=
  | nil : list@{u} A
  | cons : A -> list@{u} A -> list@{u} A.

In my code, I want to remember links between universes, otherwise the new terms I generate from this input will have too many binders, lose the information that they are linked, and potentially they won't be correct. I want to limit as much as possible the number of bound universes and not lose information.

Enzo Crance (Jun 30 2023 at 12:56):

In general, anything preventing me to read and write information about universes is a problem. For the read part it looks like commenting this code is sufficient. For the write part, it is the problem we mentioned at CUDW, i.e. impossibility to instantiate constants with algebraic universes...

Last updated: Oct 13 2024 at 01:02 UTC