prod_curry produces an uncurried function, and prod_uncurry a curried function. Isn't that backward? Or is there a different naming convention that Coq follows?
As a side note, on top of that, std++ adds:
Notation curry := prod_curry. Notation uncurry := prod_uncurry.
which results in those functions being swapped from their Haskell counterpart (while std++ usually follows Haskell notation pretty closely). I know where to report std++ bugs (/cc @robbert), but I wanted to first understand the Coq library choice.
@Paolo Giarrusso Last time I checked I also concluded that it was backward and renamed appropriately for my own purpose https://github.com/affeldt-aist/monae/blob/master/monae_lib.v#L80.
I guess we could fix std++ to have
Notation curry := prod_uncurry. Notation uncurry := prod_curry. — but also add the same notations to the stdlib?
I mean for Coq 8.13. Maybe in fact it’s
prod_* which should become deprecated notations for
uncurry — but that’s technical choice which could be taken later (seems just a matter of minimizing the migration cost)
prod_* definitions + addition of the "correct" definitions sounds like a good idea to me.
Yes, this seems indeed backward. Somehow I missed this when introducing Haskell-like names in std++. Please make an MR for std++ (so we can fix it in std++ now) and Coq (so it can be fixed upstream too).
@affeldt-aist This is now more technical, but should one use separate definitions? I proposed notations to not break syntactic matching (e.g. in Ltac).
I guess it depends on the policy wrt backward compatibility, but if it is really ill-named, then warn that the
prod_* versions are deprecated and invite the user to switch asap to the new definitions sounds reasonable to me.
(Of course, this is a problem wrt unmaintained code but otoh wouldn't a pile of notations contribute to confusion?)
oh, I’m assuming the notations can be deprecated
Oh, and they’d have to be “only parsing” notations (well, abbreviations)
And at least in 8.13 (where I’m assuming that, e.g., both Definition uncurry and Notation prod_curry would appear) I’d want prod_curry and uncurry to be syntactically equal. With a separate prod_curry definition, that’d be playing a “fun” game, called Coq unification roulette :-P
@Paolo Giarrusso Please go ahead. Making
uncurry the new definitions and
prod_uncurry the deprecated compatibility aliases seems like a good strategy.
I've opened https://github.com/coq/coq/pull/12716
Last updated: Oct 03 2023 at 19:01 UTC