Stream: math-comp users

Topic: finmaps and universes


view this post on Zulip Bas Spitters (Dec 16 2020 at 20:07):

@Arthur Azevedo de Amorim @Cyril Cohen We're currently working around an issue in fmaps caused by Choicetype is not universe polymorphic. I guess making it polymorphic would be very invasive for mc. Could you please confirm that suspicion?
Is there any experience in mc using upolymorphic definitions?

view this post on Zulip Cyril Cohen (Dec 16 2020 at 20:45):

mathcomp only uses 3 universes AFAIK (and I do not think either or @Arthur Azevedo de Amorim or my fmap do otherwise)... Hence I'm not sure what the impact is. I think @Enrico Tassi or @Assia Mahboubi did experiments on mathcomp at some point, maybe they have more informative answer

view this post on Zulip Enrico Tassi (Dec 17 2020 at 09:53):

I think it may make sense to selectively turn on universe polymorphism on a few constructions and see if it works. But I'm afraid it is a bit of an uncharted territory, and I'm not competent enough about univpoly to know if one can still build a monomorphic theory on top a polymorphic one. Is it that viral? IIRC a monomorphic definition can use an instance of a polymorphic one.

view this post on Zulip Arthur Azevedo de Amorim (Dec 17 2020 at 13:30):

It would be really nice if universe polymorphism could be integrated into MathComp and the standard library. I've run into universe issues like this before, though for unrelated reasons.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 11:25):

I don't think it would be reasonable to do it with the current universe system. A try was made by Andreas Lynge a while back and he run into many issues with minimization etc... However, we are working on a more general setup (at least allowing algebraics everywhere) that should give the right primitives for math-comp to define universe polymorphic structures but also to be able to specialize them at specific universes, without blowing up the number of universes and constraints.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 11:25):

Sorry it's taking so long to get there :)

view this post on Zulip Karl Palmskog (Dec 18 2020 at 12:00):

assume universe polymorphism is integrated into Stdlib and/or MathComp. Can we say for sure that this will not cause strange universe consistency errors and performance issues for people who are not interested in using the polymorphism? If not, then it may be better to develop separate libraries

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:02):

I'd be way more concerned about efficiency. I don't share the optimism of @Matthieu Sozeau about algebraic universes.

view this post on Zulip Pierre-Marie Pédrot (Dec 18 2020 at 12:03):

There are so many things that can go wrong, especially in unification...

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 12:16):

I agree performance and the amount of annotations needed are the big ifs. However if math-comp can really be annotated with 3 universes, then it should not be impossible.

view this post on Zulip Enrico Tassi (Dec 18 2020 at 13:23):

A try was made by Andreas Lynge a while back and he run into many issues with minimization

Do you remember what he tried exactly? IMO he tries to compile mathcomp with univpoly on, everywhere.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 15:58):

Yes, that was the spirit.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 16:02):

https://github.com/andreaslyn/coq/commits/SSR-FOR-HoTT is one branch with some of this work but I'm not sure it is the right one.

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 16:02):

@Bas Spitters might remember better than me here

view this post on Zulip Matthieu Sozeau (Dec 18 2020 at 16:07):

Well, https://github.com/andreaslyn/math-comp/commits/hott shows the port of math-comp at the time, it's more refined than just adding Set Universe Polymorphism. IIRC the main problems we encountered were due to minimization, and some issues with tactics. However it tried also moving equality to Type, HoTT-style, which could be very invasive.

view this post on Zulip Bas Spitters (Dec 18 2020 at 16:25):

Yes, that was the idea. I'll check whether there was work on another branch.

view this post on Zulip Bas Spitters (Dec 19 2020 at 15:52):

Here's the work on minimization:
https://github.com/coq/coq/pull/11512
https://github.com/coq/coq/issues/10513


Last updated: Feb 08 2023 at 07:02 UTC