Remove arity information in `Relation` module paths

[MatthewDaggitt]

There's been some talk on Zulip of removing the distinction between Nullary/Unary/Binary/Ternary in the Relation sub-hierarchies as they are long, noisy and sometimes not very meaningful. I'm broadly in favour but will need community help with the refactorings as this a huge change.

More importantly we need to decide what is to replace it? Synthesising various proposals from people over the years here's a first attempt:

• Relation (combines old `Relation.Binary/Ternary hierarchy?)
  • Equivalence/Equality?
  • Order
  • Other
• Predicate (replaces Relation.Unary?)
• Sets (replaces Relation.Nullary?) (don't think we can use Set?)

[wenkokke]

I don't think Relation.Predicate is particularily meaningful either? Especially if we're using it as a synonym for Unary?

[wenkokke]

I think a solid base proposal would be to just remove the occurances of Binary, Nullary, and Unary:

s/Relation\.\(Binary\|Nullary\|Unary\)/Relation/g

That would let us automate most of the work, and we'd only have to think about merging the base modules.

[wenkokke]

Could anyone explain why negation and decidability are defined in Relation.Nullary, though? They seem very... unary?

[MatthewDaggitt]

I don't think Relation.Predicate is particularily meaningful either? Especially if we're using it as a synonym for Unary?

I wasn't suggesting Relation.Predicate, only Predicate?

I think a solid base proposal would be to just remove the occurances of Binary, Nullary, and Unary:

Hmm, so maybe I have mis-stated my position... I'm primarily on board with this proposal because the names are long and cumbersome, and, anecdotally, most newcomers to the library find that Relation.Nullary/Unary is a confusing place to look for many key definitions. I do think the distinction between the Nullary/Unary/Binary is valuable (I'm less bothered about the distinction between Binary/Ternary/... etc.). Given that I think smooshing them all into one is probably not the way to go...

Could anyone explain why negation and decidability are defined in Relation.Nullary, though? They seem very... unary?

Predates me. My guess is that they act on nullary quantities, i.e. sets, and therefore they live in the nullary module. @nad might be able to confirm or deny?

[nad]

Predates me. My guess is that they act on nullary quantities, i.e. sets, and therefore they live in the nullary module. @nad might be able to confirm or deny?

https://github.com/agda/agda-stdlib/blob/e926c7d6e69d8cee9b976e61126dd6d9829bff84/src/Relation/Nullary.agda#L1-L5

[gallais]

Where should pointwise equality of 3 lists go in the new scheme?

Currently we have Data.List.Relation.Binary.Poinwise and we would add the new module Data.List.Relation.Ternary.Pointwise.

[MatthewDaggitt]

Minor nit-picking, I'd argue that we shouldn't be defining pointwise equality over 3 lists but instead be going straight for n lists via Linked (Pointwise R) or All (Pointwise R). Regardless, it's a good point @gallais.

Perhaps Data.List.Relation.Pointwise and Data.List.Relation.Pointwise.Nary, like we have Data.Product/Data.Product.Nary?

[MatthewDaggitt]

Superseded by the proposal in https://github.com/agda/agda-stdlib/issues/1763