Split `Equality` and `Order` out of `Relation.Binary`

[MatthewDaggitt]

Okay, the AIM discussion on Monday and reviewing https://github.com/agda/agda-stdlib/pull/1760 has crystallised something in my mind.

Relation.Binary is fundamentally different from Relation.Unary and Relation.Nullary as it contains hierarchies for both equalities and orderings. I was reviewing #1760 and was about to suggest that we add a ton of more stuff to do with Galois connections under Relation.Binary which seems totally the wrong place for it, but at the same time the only sensible place for it under the current structure.

Proposal: break out the two hierarchies in Relation.Binary into new top-level modules Equality and Order respectively, to give them parity with Function and Algebra hierarchies. e.g. we would have (Order/Equality).(Definitions/Structures/Bundles).

Consequences

• to import IsEquivalence, Setoid etc., you would use Equality instead of Relation.Binary
• to import IsPreorder, Preorder, Poset, etc. you would use Order instead of Relation.Binary
• to import _≡_, refl etc. you would use Equality.Propositional instead of Relation.Binary.PropositionalEquality

Advantages

• Makes it far easier for new users to find equality, arguably the first thing they need and look for.
• Typing open import Relation.Binary.PropositionalEquality in every module is frankly a pain in the neck. open import Equality.Propositional is much shorter.
• Order theory is a rich area, and this would provide a dedicated top-level folder for it.
• Separates out orderings from equality.
• Much lighter dependencies for equalities, as you are no longer forced to import a load of order theory as well.

Obviously we would maintain backwards compatibility for such a big change, by having the existing Relation.Binary(.Structures/Bundles) re-export all the content of the new modules.

What are people's thoughts?

[jespercockx]

I am very much in favour of this proposal! I'm already looking forward to the last day I have to type out Relation.Binary.PropositionalEquality in full :)

[sstucki]

I like the idea, but boy is it going to break backwards compatibility! 😉

That being said, I think people are generally used to the library being in flux at this point. (At least I've heard statements to that effect from many Agda users around me.) So breaking changes might not be as big a deal as one might at first assume.

So 👍 from me.

[MatthewDaggitt]

I like the idea, but boy is it going to break backwards compatibility!

@sstucki can you explain why it would? As mentioned before, the modules Relation.Binary/Relation.Binary.Structures etc. will still exist and will publicly re-export the same content from their new location. Some of the existing modules may have deprecation warnings attached, but I don't think any code should actively break?

[jamesmckinna]

In principle, this seems like a useful/well-motivated change. And as with recent changes I helped push through, I'm not necessarily against breaking changes. That's usually what I expect from a major version bump, even given the maintainers' heroic (truly!) efforts in maintaining deprecation warnings and so forth.

That said, I'm not clear about the various import dependencies (esp. on ...Properties) and ...Definitions) when it comes to proving results about relations (such as reflexive-transitive closures of reduction relations in semantics) which, while they are surely Preorders, that structure is not the 'interesting' structure at hand. Would I now need to import Order.* in order to talk about transitivity? Where would relations which aren't either equivalences or preorders, eg PERs, or uniformities in topology, now belong? Etc. ADDED sorry if this remark seems stupid; those things have to be imported from somewhere, obviously. But the neutrality of Relation.Binary enjoys (well: YMMV ;-)) the cognitive/conceptual advantage that it brings no baggage with it... and the proposal makes the case for "no, we'd really like stdlib to carry some baggage (of conceptual/structuring expectations) around, because this (cognitively) optimises for the common case", which as I said above, seems (potentially) useful/well-motivated.

[sstucki]

@sstucki can you explain why it would? [...] Some of the existing modules may have deprecation warnings attached, but I don't think any code should actively break?

Yes, sorry, bad wording on my part. I guess "boy will this cause deprecation warnings" would be more accurate.

[MatthewDaggitt]

That said, I'm not clear about the various import dependencies (esp. on ...Properties) and ...Definitions) when it comes to proving results about relations (such as reflexive-transitive closures of reduction relations in semantics) which, while they are surely Preorders, that structure is not the 'interesting' structure at hand. Would I now need to import Order.* in order to talk about transitivity?

This is an excellent question and something I'd been thinking about as well. I think the answer is that we'd keep Relation.Binary.Definitions as is (although probably merging with Relation.Binary), because as you say all these definitions make sense outside of a context of the order. Then Order.Definitions and Equality.Definitions would publicly re-export the relevant ones?

Where would relations which aren't either equivalences or preorders, eg PERs, or uniformities in topology, now belong? Etc.

I would imagine that PERs would move into Equality as well. If a serious amount of topology was then added, I think it would indicate the need for a new top-level folder Topology? Does that make sense to you?

[jamesmckinna]

Thanks Matthew, I always like to have asked an "excellent" question (:blush:), especially if/when I don't already know the/my preferred answer ;-)

Regarding PER moving with Equality... I suppose so, although I'm not sure... do we have much development of PERs yet? (Perhaps they don't need much?) Would that end up under Equality.Partial.*? Maybe that's fine; and/because memorable... part of the cognitive load/availability that users have to share with stdlib lies in maintaining that balance...

Regarding 'other' kinds of Binary relations: yes, I guess they might float up to the top level once they have proved their worth. Perhaps we don't (yet) have much Topology is because the classical notions are notoriously... delicate... as to constructivisation, wrt impredicativity, and points, among other things. So my 'objection', such as it is, might be considered moot, for the time being. (And with it, any other discussion of 'a library for now' vs. 'a library for all time', cf. Bourbaki)

[nad]

I think you should be very careful about starting to use new top-level module names like Equality, at least until issue https://github.com/agda/agda/issues/4029 has been fixed.

I have another library with modules like Equality and Equality.Propositional. This library and some other developments that make use of it contain something like 400 modules, and the library imports the standard library. If the standard library starts using Equality.Propositional (say), then my library stops working.

[MatthewDaggitt]

Okay marking this blocked upstream by https://github.com/agda/agda/issues/4029

[JacquesCarette]

I'm all for this proposal too. One naming question though: Equality or Equivalence ? [Sorry to bring this up, but better to discuss it now rather than later. I mildly prefer Equivalence, but won't fight for it.]

[Taneb]

I'd also prefer Equivalence. There's a lot of equivalence relation that aren't equality (equivalence modulo n, for one, and Always for another). The downside of that name is Equivalence.Propositional is not a good name for Relation.Binary.PropositionalEquality. I don't have a great solution for that.

[MatthewDaggitt]

I totally agree with your points @Taneb. Including that the question of where to put propositional equality would then become much harder....

[JacquesCarette]

Equivalence.Equality.Propositional? Equivalence.Propositional.Equality ? Or even Equivalence.PropositionalEquality.

[gallais]

I think the people who were tired of typing Relation.Binary.PropositionalEquality are not going to like it. :D

Pragmatically, is this issue actually an Agda feature request in disguise for

1. auto-completion of modules (and other) names
2. auto-insertion of appropriate imports if you mention an out-of-scope identifier

?

[MatthewDaggitt]

Pragmatically, is this issue actually an Agda feature request in disguise for

• auto-completion of modules (and other) names
• auto-insertion of appropriate imports if you mention an out-of-scope identifier ?

Well the shortening of the names is, but not the entire proposed refactoring. I think having a top-level Order folder is still conceptually the right thing to do as otherwise there's no natural place for things like #1760

[JacquesCarette]

I don't think anyone has spoken against having a top-level Order (nor questioned its name). I don't think anyone has spoken against top-level "equality" hierarchy, just its name. My read is that the work on Order can proceed right away.

[Taneb]

Idea: Order and Equivalence, with Relation.Binary.PropositionalEquality moving to a top-level Equality module

[jamesmckinna]

@Taneb Did you really mean Equality at top-level, or as Equivalence.(Propositional)Equality? My understanding of Nisse's objection was in particular to avoid any breaking change to his Equality.* hierarchy.

Suggestion: if we really want propositional equality at toplevel, then PropositionalEquality.* seems the (a) way to go?

[Taneb]

@jamesmckinna regardless of which name we choose, @nad's objections apply until https://github.com/agda/agda/issues/4029 is in. I'm sure someone out there is using Order and Equivalence too (or at least we should assume there might be). I very much did mean to put Equality at the top-level.

[jamesmckinna]

@Taneb Thanks Nathan for the clarification. I was doing my usual 'think out loud' given the comments so far, and wanting to see if there could be movement even if agda/agda#4029 were unresolved. So then there's an argument to have about the name of the top-level module for _≡_. I'd be content with, even argue for, PropositionalEquality... to deliberately have it stick out like a sore thumb.

[MatthewDaggitt]

Hmm so given the discussion above, I agree that equality and equivalence is subtly different. But at the same time I don't want to special case PropositionalEquality too much as there are other types of equalities in the library, e.g. HeterogeneousEquality. So my new proposal is that maybe we should have both an Equivalence folder and an Equality folder at the top-level:

• Equivalence

  • Structures
  • Bundles
  • Reasoning

• Equality

  • Propositional
  • Heterogeneous
  • etc.

[nad]

I don't think any of the main Agda developers plan to fix issue https://github.com/agda/agda/issues/4029 any time soon. However, once we have settled on a design I think it would be feasible (but perhaps non-trivial) for someone who is not familiar with the Agda code base to implement the new feature (and help would be available). Contributions are welcome!