Olivier Laurent (Jan 05 2022 at 09:26): Olivier Laurent (Jan 05 2022 at 09:26):arrow and flip are defined twice in stdlib with the same definition: without universe polymorphism in Program.Basics and with universe polymorphism in Classes.CRelationClasses.
The name clash makes some behaviors difficult to trace. Is there a strong reason to have both? If so is there a standard way to give different names in such a situation?
Gaëtan Gilbert (Jan 05 2022 at 10:50):it's possible that program doesn't need them to be monomorphic, in which case we could just define the polymorphic version somewhere that both depend on (probably Init/Datatypes)
Pierre-Marie Pédrot (Jan 05 2022 at 10:52):Beware with flip, any lemma that mentions it would turn it into a polymorphic one, causing mayhem in performance of setoid rewriting
Karl Palmskog (Jan 05 2022 at 11:03):if flip is caveat emptor, then I think it should have some warning...
Pierre-Marie Pédrot (Jan 05 2022 at 11:05):arrow is also used by setoid rewriting, but I don't know whether it's as critical as flip, which is used pervasively for relation normalization
Pierre-Marie Pédrot (Jan 05 2022 at 11:06):(see https://github.com/coq/coq/issues/14488 for a taste of this kind of horror)
Karl Palmskog (Jan 05 2022 at 11:07):your daily type-theoretic Lovecraftian horror, as narrated by PMP (something like this but with Coq syntax?)
Karl Palmskog (Jan 05 2022 at 12:29):Our every step unsettled the ancient earth. But we were in a realm of death and madness... In the end, I alone fled laughing and wailing through those blackened arcades of antiquity.
Olivier Laurent (Jan 06 2022 at 06:55):Benchmark does not look that bad.
Some project failures should be corrected with the updated commits.
But I have no idea why coq/coq#1939 is back.
Pierre-Marie Pédrot (Jan 06 2022 at 10:59):Ah, yes, actually this is probably fine. The important part for performance is that the lemmas that are part of the TC resolution are monomorphic. Just making flip polymorphic is not enough to make them polymorphic as well, so there is no problem there. It'd be more problematic if we started sharing instances of Proper and the like, but thankfully universe polymorphism is not strong enough to allow Prop instantiations (yet) so we're safe on that side for now.
Last updated: Oct 04 2023 at 23:01 UTC