search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole #2397

Open andreasabel opened 4 months ago

andreasabel commented 4 months ago

Module Data.List.Relation.Binary.Subset.Setoid is parametrized on a Setoid, but its Properties module not: https://github.com/agda/agda-stdlib/blob/bfd7a7bda8ee55e8d319600c974a3ca7151d752b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda#L9 Instead, each function is parametrized there individually, via anonymous modules. Is there a reason why it is organized like this?

I would have expected to open the Properties module in the same way as its parent module.

JacquesCarette commented 4 months ago

This tends to be for historical reasons rather than any 'good' reason. Evolution of the library happens haphazardly sometimes (no matter how hard we try to review PRs).

In other words, I'd call this a plain bug awaiting a PR to fix it.

MatthewDaggitt commented 4 months ago

No, there's a good reason for all such Properties modules being designed this way. If you parameterise it by a single setoid, then you can't prove properties of functions that move between different types, e.g. map.

jamesmckinna commented 4 months ago

But as @omelkonian writes on #2389 , this is not the case for eg Data.List.Relation.Binary.Permutation.Setoid.Properties, leading to undesirable consequences... wrt map :-( so @JacquesCarette 's point about historical/legacy inconsistency stands.

Ditto. The proposed addition in #2393 ...?

jamesmckinna commented 4 months ago

No, there's a good reason for all such Properties modules being designed this way. If you parameterise it by a single setoid, then you can't prove properties of functions that move between different types, e.g. map.

Is this design principle documented anywhere?

MatthewDaggitt commented 3 months ago

But as @omelkonian https://github.com/agda/agda-stdlib/pull/2389#discussion_r1608424533, this is not the case for eg Data.List.Relation.Binary.Permutation.Setoid.Properties, leading to undesirable consequences... wrt map :-(

Yes that should really be fixed.

Is this design principle documented anywhere?

No, sadly not :sweat: