Li-yao (Jul 13 2020 at 21:04): Li-yao (Jul 13 2020 at 21:04): Pierre-Marie Pédrot (Jul 14 2020 at 10:11):Regarding your first question, the global feeling is that there is a strong tension between expressivity and efficiency.
Pierre-Marie Pédrot (Jul 14 2020 at 10:12):Either you quantify everywhere and you get very generic code, at the cost of exponential blowups, or you unify everywhere and you're basically back to monomorphic code.
Pierre-Marie Pédrot (Jul 14 2020 at 10:13):The current default tries to strike a balance between both, but I am personally convinced that if we want to scale, we need to be essentially monomorphic-like everywhere, and polymorphism must be explicitly asked by the user.
Pierre-Marie Pédrot (Jul 14 2020 at 10:13):There are other questions involved, like the choice of representation for universes.
Pierre-Marie Pédrot (Jul 14 2020 at 10:14):For instance, template polymorphism is horrible in terms of typing rules (and probably unsound in the implementation) but it's efficient because universe instances are inferable
Pierre-Marie Pédrot (Jul 14 2020 at 10:17):As for your second question, normally lists are template polymorphic so you'll get refreshed instances every time you use them
Pierre-Marie Pédrot (Jul 14 2020 at 10:18):To generate fixed universe constraints with lists you need to perform a partial application
Pierre-Marie Pédrot (Jul 14 2020 at 10:18):Those uses of lists will indeed add monomorphic constraints in the global table
Karl Palmskog (Jul 14 2020 at 10:28):how many large Coq projects actually use universe polymorphism at all? I'm sure there are some that absolutely can't live without it, but my feeling is that mostly it's unused or a distraction. Is there an easy way to tell if a project uses non-trivial universe polymorphism or template polymorphism @Pierre-Marie Pédrot?
Gaëtan Gilbert (Jul 14 2020 at 10:30):That would need a definition of non-trivial
Karl Palmskog (Jul 14 2020 at 10:32):Gaëtan Gilbert said:
That would need a definition of non-trivial
yes, I'm basically asking: is there a reasonable definition of / criterion for non-trivial use of universe polymorphism?
Pierre-Marie Pédrot (Jul 14 2020 at 12:06):@Karl Palmskog in the CI only HoTT, UniMath and Mtac2 use universe polymorphism
Pierre-Marie Pédrot (Jul 14 2020 at 12:06):apart from spinoffs of those devs I don't think universe polymorphism is used much in the wild
Karl Palmskog (Jul 14 2020 at 12:11):in this case, maybe it would be warranted in the future to have the option to select "monomorphic stdlib(2)" (for performance + simplicity)
Bas Spitters (Jul 14 2020 at 12:22):@Matthieu Sozeau is working on a more aggressive universe minimization algorithm. That should help efficiency.
Arthur Azevedo de Amorim (Jul 14 2020 at 12:31):I was trying to write a category theory library using universe polymorphism and was running into various issues because Coq was creating universe levels where I didn't want to.
Karl Palmskog (Jul 14 2020 at 12:31):even if it's eventually efficient to check polymorphic universes, wouldn't "certifiably monomorphic" give you more stuff? Like iron-clad guarantee that checking a Qed proof in isolation without checking universe consistency never has a false positive?
Pierre-Marie Pédrot (Jul 14 2020 at 12:38):It's actually the opposite, polymorphic code is better behaved.
Pierre-Marie Pédrot (Jul 14 2020 at 12:39):The monomorphic set of constraints is a global shared state and it's problematic for a lot of reasons.
Pierre-Marie Pédrot (Jul 14 2020 at 12:40):There is this funny counterexample where the value of a boolean in parallel mode depends on the order of scheduling.
Pierre-Marie Pédrot (Jul 14 2020 at 12:40):Also, you never know whether it's legal to link (= Require) two libraries defining monomorphic constraints
Bas Spitters (Jul 14 2020 at 14:36):Draft on minimization:
https://github.com/coq/coq/pull/11512
Emilio Jesús Gallego Arias (Jul 14 2020 at 15:05):Pierre-Marie Pédrot said:
Karl Palmskog in the CI only HoTT, UniMath and Mtac2 use universe polymorphism
Doesn't extlib also provide univ poly definitions?
Paolo Giarrusso (Jul 14 2020 at 15:10):There's also Local Set Universe Polymorphism. in two stdpp files, and those are used in Iris and lambda-rust
Paolo Giarrusso (Jul 14 2020 at 15:31):Also tagging @Janno
Paolo Giarrusso (Jul 14 2020 at 15:33):@Janno what else (in the wild/in CI) uses uni-poly? People already mentioned Mtac2, stdpp, ext-lib, HoTT and UniMath
Janno (Jul 14 2020 at 15:35):I don't actually know. I was actually under the impression that UniMath didn't use universe polymorphism.
Janno (Jul 14 2020 at 15:36):https://github.com/UniMath/UniMath/blob/master/Makefile#L96
Bas Spitters (Jul 14 2020 at 15:49):@Janno that's also my understanding
Alexander Gryzlov (Jul 14 2020 at 20:30):We'd like to try relying on universe polymorphism in FCSL at some point in near future to simplify some definitions
Janno (Jul 16 2020 at 08:22):@Alexander Gryzlov what kind of simplification do you hope to achieve? (My code is rarely made simpler by universe polymorphism. I only enable it when I cannot get the program to work in another way..)
Alexander Gryzlov (Jul 16 2020 at 12:43):Janno said:
Alexander Gryzlov what kind of simplification do you hope to achieve? (My code is rarely made simpler by universe polymorphism. I only enable it when I cannot get the program to work in another way..)
Basically there's some code duplication in https://github.com/imdea-software/fcsl-pcm/blob/master/pcm/unionmap.v that hopefully would go away when the underlying structure is refactored to make use of UP
Kenji Maillard (Jul 16 2020 at 13:12):@Alexander Gryzlov Do you mean to bypass the duplication explained in that comment ?
I decided on the more complicated design to avoid the universe
jump. Heap values are dynamic, and live in Type(1), while most of the
times, ordinary union_maps store values from Type(0), and can be
nested. If the two structures (heaps and ordinary union maps) share
the same code, they will both lift to the common universe of Type(1),
preventing me from using maps at Type(0), and storing them in the heap.
If that's the case you should be able to limit the use of Polymorphic objects to that file and handle the necessary universes explicitly, no ?
Alexander Gryzlov (Jul 16 2020 at 13:14):Kenji Maillard said:
Alexander Gryzlov Do you mean to bypass the duplication explained in that comment ?
I decided on the more complicated design to avoid the universe jump. Heap values are dynamic, and live in Type(1), while most of the times, ordinary union_maps store values from Type(0), and can be nested. If the two structures (heaps and ordinary union maps) share the same code, they will both lift to the common universe of Type(1), preventing me from using maps at Type(0), and storing them in the heap.If that's the case you should be able to limit the use of
Polymorphicobjects to that file and handle the necessary universes explicitly, no ?
I haven't actually started doing this, but when I do, I'll certainly give it a try, thanks!
Matthieu Sozeau (Jul 20 2020 at 09:38):I kind of agree with Pierre-Marie, while lists could be made polymorphic and cumulative, we certainly want to keep lemmas/user developments using global universes for now until we have a more reasonable inference story. There are not many large developments using full polymorphism, and they’re mainly category theory/HoTT related at this point I think.
Matthieu Sozeau (Jul 20 2020 at 09:53):Principal universe inference is currently prohibitively expensive, in terms of generated universes and constraints, because of the mix of cumulativity and polymorphism. One direction to avoid the blow-up is to force users to be explicit about cumulativity, that’s the minimization enhancement I was proposing.
Last updated: Apr 20 2024 at 01:41 UTC