@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?
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
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.
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.
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.
Sorry it's taking so long to get there :)
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
I'd be way more concerned about efficiency. I don't share the optimism of @Matthieu Sozeau about algebraic universes.
There are so many things that can go wrong, especially in unification...
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.
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.
Yes, that was the spirit.
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.
@Bas Spitters might remember better than me here
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.
Yes, that was the idea. I'll check whether there was work on another branch.
Here's the work on minimization:
https://github.com/coq/coq/pull/11512
https://github.com/coq/coq/issues/10513
Last updated: Oct 13 2024 at 01:02 UTC