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 `curry`

and `uncurry`

— but that’s technical choice which could be taken later (seems just a matter of minimizing the migration cost)

Deprecation of `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 `curry`

/ `uncurry`

the new definitions and `prod_curry`

/ `prod_uncurry`

the deprecated compatibility aliases seems like a good strategy.

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

Last updated: Jun 16 2024 at 01:42 UTC