-
Notifications
You must be signed in to change notification settings - Fork 242
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add Raw
bundles to Relation.Binary.*
hierarchy
#2491
Conversation
This looks pretty good, but I do think that the changes to |
UPDATED: Please ignore this comment! The latest round of debugging commits suggest that the I'm not clear about the history of these things, but why do we have the |
Now added, and manifest at the top updated to reflect those additions. |
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm somewhat undecided if this is the right thing to do. The code seems fine. It is definitely more consistent with what has been done elsewhere, so as a default, this is moving in a coherent direction. I'm just not quite ready to 'approve'.
@JacquesCarette writes:
Beyond your comments on the originating issue #2274 can you say (more) about why you are/might be hesitating? (UPDATED: have just seen your more recent comment there... interesting!) |
Teaching with PLFA right now, have updated to agda-2.7 and stdlib-2.2, and some things have gotten worse. I've got some issues to bring up when I have the time. One example: having |
Are these issues to do with this PR, or general comments deserving a separate issue for v2.1/v2.2, or even on the PLFA tracker? hard to see how |
The example is of the latter kind. But the reason I'm hesitating is related to me finding teaching with post-v2.0 stdlib a bit awkward compared to 1.7. |
Still: suggest you move this thread off this PR? |
Could you submit this as a separate issue, so that we can discuss these issues in detail? |
@wenkokke wrote:
planning to! I've been swamped, so this is still in my ToDo queue. |
Yes, in retrospect it wasn't the best idea, but at the time, it was the only way to add them that preserved backwards compatibility. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The other refactorings look good though!
So, while I would still be happy/happier to see this merged (despite @JacquesCarette 's hesitation about doing so), it's somewhat ironic that we seem, via this route, to have reinstated the 'old' vocabulary (and then erased it via |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This nicely refactors concepts that were free-floating until now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I relent. This is an improvement, on the balance of things, esp. for v2.*.
@jamesmckinna @gallais and I have verified that the changes asked for have been done. So we're over-riding the blocked merge from @MatthewDaggitt . |
Because it's been done but reviewer is not available to do it 'now'
This addresses the
Relation.Binary.Bundles.Raw
part of #2274 ahead of any subsequent refactoring of theAlgebra
hierarchy in earnest, to exploit the standardisation of vocabulary/fixity envisaged there.Adds:
RawX
bundles systematically to mirror those inRelation.Binary.Bundles.X
rawX
manifest fields to each of those inRelation.Binary.Bundles.X
NB. Possible issues:
Relation.Bundles
definitions, this introducesrawSetoid
fields at the top level to eachRawX
bundle, in order to also introduce the negated equality symbol_≉_
uniformly.DecX
hierarchy is not mirrored with a parallelRawDecX
hierarchy... which might otherwise violate the proposed alternative dependency structure outlined in [DRY] Reconciling the indices ofIsX
with those of the correspondingRawX
#2252 ._≉_
defined both forAlgebra.Bundles.Raw.RawX
bundles, and viaSetoid
instances, forAlgebra.Bundles.X
? #2274 the current design forApartnessRelation
introduces its negated relation symbol in theStructures
hierarchy (cf.Algebra.Structures.IsGroup
...), moreover without any fixity declaration; so there are/might be opportunities to rectify this design viapublic
re-export...?