8000 [ add ] Choudhury and Fiore's alternative definition of `Permutation` for `Setoid`s by jamesmckinna · Pull Request #2726 · agda/agda-stdlib · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

[ add ] Choudhury and Fiore's alternative definition of Permutation for Setoids #2726

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.

Sign up for GitHub

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

Jump to bottom
Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open

[ add ] Choudhury and Fiore's alternative definition of Permutation for Setoids #2726

wants to merge 14 commits into from

Conversation

jamesmckinna
Copy link
Contributor
@jamesmckinna jamesmckinna commented Jun 2, 2025 •
edited
Loading

Alternative definition, as described in #2311, and towards open problems arising from #2723 and #2725

NB.:

  • UPDATED: I've previously misattributed this to Ralf Hinze, but credit properly belongs to Choudhury & Fiore, apparently
  • module name? ChoudhuryFiore, like Hinze before, it, doesn't sit well with library style? But will change for the time being, against the possibility of eventually superseding Permutation.Setoid with this definition?)
  • a bit rough around the edges; maybe should be DRAFT for the time being... or else could be fixed up in v3.0 once we agree which representations to bless for that release? UPDATED: have now done so

TODO:

  • Base/Properties refactoring
  • CHANGELOG

Regarding the Sorted lemma of #2723

property1 : xs ↭ ys → Sorted xs → Sorted ys → xs ≋ ys

suggest that this be handled in a downstream PR:

  • subrelation _∼ₛ_ in which list cs is Sorted, is equivalent to _∼_ (given a sorting algorithm, or at least the existence of a sorted representative of the _∼_ equivalence class)
  • _∼ₛ_, with some gymnastics, satisfies property1, but the paper proof I have needs tidying up

@jamesmckinna jamesmckinna added this to the v2.3 milestone Jun 2, 2025
@jamesmckinna jamesmckinna mentioned this pull request Jun 2, 2025
Open
@jamesmckinna jamesmckinna mentioned this pull request Jun 3, 2025
Open
@jamesmckinna
Copy link
Contributor Author

@MatthewDaggitt 's approach to property1 via Fin n as a canonical representing type for Sorted lists seems much better, so good not to pursue this further here!

@JacquesCarette
Copy link
Contributor

This is also equivalent to the more general version using Inverse, no? If you're not going to pursue further, close?

@jamesmckinna
Copy link
Contributor Author

This is also equivalent to the more general version using Inverse, no? If you're not going to pursue further, close?

No to closing, the comment was about pursuing a proof of property1. The rest I definitely want to pursue, because this is (IMHO: much) 'better' than what we already have in terms of prep and swap etc.

What is the "more general version using Inverse"?

@JacquesCarette
Copy link
Contributor

A Permutation is a special case (for finite types) of a type isomorphism, i.e. the case for Fin n. The category (Nat, Permutation) is the skeleton of (FinSet, Isomorphism). (In fact both are rig categories, and they are rig isomorphic).

@jamesmckinna
Copy link
Contributor Author
jamesmckinna commented Jun 5, 2025 •
edited
Loading

@JacquesCarette wrote:

A Permutation is a special case (for finite types) of a type isomorphism, i.e. the case for Fin n. The category (Nat, Permutation) is the skeleton of (FinSet, Isomorphism). (In fact both are rig categories, and they are rig isomorphic).

Fantastic! Thanks so much for this (and apologies for not going back to #2311 where you do reference your own developments, and I never properly followed those up :-():

  • Rig not Semiring (still sad the library blesses the latter nomenclature over the former)
  • The machinery for all this is in stdlib, but not the actual theorem (never mind the 'skeleton of...' property: but did you mean rig-isomorphic, and not rig-equivalent? can a skeleton of a category ℂ ever be isomorphic to ℂ unless it's already skeletal? maybe I need to go back to CT school)

Nevertheless, all that said (and doubtless more that could be said), at least one reason I favour this Hinze definition over others, including anything based on coordinatisation via Data.Fin.Permutation would be, among other qualities:

Now, this comment (and perhaps others above) properly belong to #2311, as 'design' rather than 'implementation', so I'll stop here.

@jamesmckinna jamesmckinna marked this pull request as draft June 5, 2025 08:07
@jamesmckinna jamesmckinna changed the title [ add ] Hinze's definition of Permutation for Setoids [ add ] Choudhury and Fiore's alternative definition of Permutation for Setoids Jun 5, 2025
@gallais
Copy link
Member
gallais commented Jun 5, 2025

@jamesmckinna In that last commit I think you forgot to add the moved file so it just looks like
you nuked everything.

As for the naming debate, I would say stay away from naming it after people unless it's
already an established convention (e.g. Boolean/Heyting/Kripke). For instance we called this
module Data.List.Relation.Unary.Sufficient rather than Data.List.Relation.Unary.McKinna ;)

@jamesmckinna
Copy link
Contributor Author
jamesmckinna commented Jun 5, 2025 •
edited
Loading

🤦 as to deleting the addition; now restored. Thanks @gallais !
Plus: having the courage of my convictions from #2311 and calling this Algorithmic... will consider here, or downstream, adding Permutation.Declarative as well, and refactoring their properties to witness the equivalence (and probably delete the equivalence with existing _↭_, to avoid downstream naming/deprecation issues...)

@jamesmckinna jamesmckinna marked this pull request as ready for review June 5, 2025 18:15
@JacquesCarette
Copy link
Contributor

but did you mean rig-isomorphic ?

I meant naturally isomorphic as rig categories (though I did omit 'in the presence of the axiom of choice').

@JacquesCarette
Copy link
Contributor

Having said that: there are strong reasons for having many different representations of permutations in stdlib. They have their (powerful, disparate) pros and cons. Where it is not always clear that different representations of _<_ are worth it (though the cognoscenti do know), for permutations, it is a very different ball game. The equivalence of the different representations is usually seriously non-trivial too.

I'm also with @gallais on naming. Especially for permutations. While you may have learned X or Y permutation from a specific paper by specific people, usually those representations are decades if not centuries old. We need to hunt down the 'proper' names.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
addition refactoring
Projects
None yet
Milestone
v2.3
Development

Successfully merging this pull request may close these issues.
3 participants
@jamesmckinna @JacquesCarette @gallais
0