Paolo Giarrusso (Jul 19 2020 at 15:40): Paolo Giarrusso (Jul 19 2020 at 15:40):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.
Reynald Affeldt (Jul 19 2020 at 15:47):@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.
Paolo Giarrusso (Jul 19 2020 at 15:51):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?
Paolo Giarrusso (Jul 19 2020 at 15:53):I mean for Coq 8.13. Maybe in fact it’s prod_* which should become deprecated notations for curry and uncurry — but that’s technical choice which could be taken later (seems just a matter of minimizing the migration cost)
Reynald Affeldt (Jul 19 2020 at 15:55):Deprecation of prod_* definitions + addition of the "correct" definitions sounds like a good idea to me.
Robbert Krebbers (Jul 19 2020 at 15:59):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).
Paolo Giarrusso (Jul 19 2020 at 17:05):@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).
Reynald Affeldt (Jul 19 2020 at 17:12):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.
Reynald Affeldt (Jul 19 2020 at 17:17):(Of course, this is a problem wrt unmaintained code but otoh wouldn't a pile of notations contribute to confusion?)
Paolo Giarrusso (Jul 19 2020 at 17:23):oh, I’m assuming the notations can be deprecated
Paolo Giarrusso (Jul 19 2020 at 17:27):Oh, and they’d have to be “only parsing” notations (well, abbreviations)
Paolo Giarrusso (Jul 19 2020 at 17:28):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
Théo Zimmermann (Jul 20 2020 at 08:29):@Paolo Giarrusso Please go ahead. Making curry / uncurry the new definitions and prod_curry / prod_uncurry the deprecated compatibility aliases seems like a good strategy.
Yishuai Li (Jul 21 2020 at 02:02):I've opened https://github.com/coq/coq/pull/12716
Last updated: Oct 13 2024 at 01:02 UTC