agda-stdlib
agda-stdlib copied to clipboard
Split `Equality` and `Order` out of `Relation.Binary`
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 useEquality
instead ofRelation.Binary
- to import
IsPreorder
,Preorder
,Poset
, etc. you would useOrder
instead ofRelation.Binary
- to import
_≡_
,refl
etc. you would useEquality.Propositional
instead ofRelation.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?
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 :)
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.
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?
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 Preorder
s, 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 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.
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?
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 PER
s 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)
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.
Okay marking this blocked upstream by https://github.com/agda/agda/issues/4029
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.]
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.
I totally agree with your points @Taneb. Including that the question of where to put propositional equality would then become much harder....
Equivalence.Equality.Propositional
? Equivalence.Propositional.Equality
? Or even Equivalence.PropositionalEquality
.
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
- auto-completion of modules (and other) names
- auto-insertion of appropriate imports if you mention an out-of-scope identifier
?
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
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.
Idea: Order
and Equivalence
, with Relation.Binary.PropositionalEquality
moving to a top-level Equality
module
@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?
@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.
@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.
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.
-
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!