Stream: Coq users

Topic: prod_curry/uncurry seem named backward


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

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

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

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

view this post on Zulip Reynald Affeldt (Jul 19 2020 at 15:55):

Deprecation of prod_* definitions + addition of the "correct" definitions sounds like a good idea to me.

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

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

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

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

view this post on Zulip Paolo Giarrusso (Jul 19 2020 at 17:23):

oh, I’m assuming the notations can be deprecated

view this post on Zulip Paolo Giarrusso (Jul 19 2020 at 17:27):

Oh, and they’d have to be “only parsing” notations (well, abbreviations)

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

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

view this post on Zulip Yishuai Li (Jul 21 2020 at 02:02):

I've opened https://github.com/coq/coq/pull/12716


Last updated: Jan 27 2023 at 00:03 UTC