Stream: Coq users

Topic: [stdlib] Universes: arrow and flip (polymorphic or not)


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

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

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

view this post on Zulip Karl Palmskog (Jan 05 2022 at 11:03):

if flip is caveat emptor, then I think it should have some warning...

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

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

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

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

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

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC