Stream: Coq users

Topic: Questions on Universe Polymorphism


view this post on Zulip Li-yao (Jul 13 2020 at 21:04):

  1. Should datatypes (a) in the stdlib (b) in general be universe polymorphic? My current understanding is that unless you micromanage your universes, the current Coq compiler will get things wrong at some point, so the better default is to live with monomorphic types. Are these merely practical limits of the implementation or is there some fundamental limitation going on? Can we ever hope for some kind of principal universe inference?
  2. I have a rough intuition that making (universe-monomorphic) lists of types gets you one step closer to a universe inconsistency (it at least seems a common factor to some universe inconsistencies involving itree). Is that intuition correct, and if so what are the remaining steps?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2020 at 10:13):

There are other questions involved, like the choice of representation for universes.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2020 at 10:18):

To generate fixed universe constraints with lists you need to perform a partial application

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2020 at 10:18):

Those uses of lists will indeed add monomorphic constraints in the global table

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Jul 14 2020 at 10:30):

That would need a definition of non-trivial

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2020 at 12:06):

@Karl Palmskog in the CI only HoTT, UniMath and Mtac2 use universe polymorphism

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Bas Spitters (Jul 14 2020 at 12:22):

@Matthieu Sozeau is working on a more aggressive universe minimization algorithm. That should help efficiency.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Jul 14 2020 at 12:38):

It's actually the opposite, polymorphic code is better behaved.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bas Spitters (Jul 14 2020 at 14:36):

Draft on minimization:
https://github.com/coq/coq/pull/11512

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 14 2020 at 15:31):

Also tagging @Janno

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Janno (Jul 14 2020 at 15:36):

https://github.com/UniMath/UniMath/blob/master/Makefile#L96

view this post on Zulip Bas Spitters (Jul 14 2020 at 15:49):

@Janno that's also my understanding

view this post on Zulip 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

view this post on Zulip 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..)

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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 Polymorphic objects 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!

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC