agda
Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole
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.
- https://github.com/agda/agda/issues/7294?notification_referrer_id=NT_kwDOABGgkrMxMDg0NzE1Nzg3ODoxMTU1MjE4#issuecomment-2135731299
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.
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.
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 ...?
No, there's a good reason for all such
Propertiesmodules 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?
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:
Similarly, for the parametrisation of ...Propositional.Properties modules? cf. #2514