Refactor to support multiple definitions of `Data.List.Relation.Binary.Permutation`

[jamesmckinna]

Recent work by

• Choudhury and Fiore, on the free commutative monoid in HoTT, and
• Kupke, Forsberg, and Watters on fresh lists

has looked at lists-modulo-permutation, with a view to establishing that (Setoid) structure as (a representation of) (the carrier of) the free commutative monoid, with the former alluding to difficulties in establishing such results for the stdlib definition of permutation, and the latter, IIUC, by observing that fresh/sorted lists, by providing a constructive representative of the equivalence-classes-modulo makes such difficulties more tractable, at the cost of a(nother) new representation (but one already in the library, and interesting in its own right).

Each of the above, IMHO, fails to tackle the elephant in the room (incl. stdlib ;-), alas, by taking a prefix-closed, transitive relation which can swap only the top two elements of a list; it's very fiddly, and requires transitivity to be built in), namely that there are two 'natural' definitions of the relation, for which it is interesting (and useful/computationally relevant!) to prove the equivalence between them (something already done, but lost in the archaeology of my PhD thesis back in 1992), namely as:

• declaratively the least congruence for [], _∷_ (and hence for _++_) which 'makes _++_ commutative', ie relates as ++ bs and bs ++ as
• algorithmically the least relation such that [] is related to itself, and that if cs is related to as ++ bs, then c ∷ cs is related to as ++ c ∷ bs (whence the correctness of insertion sort)

I've recently come across the following definition, due, which I learnt from Ralf Hinze (UPDATED: apparently the inspiration for him came from Choudhury and Fiore's paper above), which may easily be shown equivalent to each of these definitions (NB in the Propositional case, I'm still looking at the Setoid generalisation), as the least relation such that:

• [] is related to itself
• if as is related to bs, then a ∷ as is related to a ∷ bs
  (so that we have left-prefix-closure for _++_, if not full congruence, straightaway)
• if as is related to b ∷ cs, and bs is related to a ∷ cs, then a ∷ as is related to b ∷ bs (whence the correctness of mergesort, as well, again IIUC)

This may easily be shown to be reflexive, symmetric, makes _++_ commutative, and by a slightly fiddly length induction, may be shown to be transitive. Cancellation properties, as well as full congruence, follow easily from this.

PROPOSAL: subject to the Setoid generalisation working out, that we replace the library definition with the one above, together with the Properties showing it equivalent to the declarative and algorithmic ones above.

ISSUES:

• the library computes a notion steps counting the number of rule applications of the existing constructors, but AFAICT, it is used nowhere else in the library, but would need to be retained for backwards-compatibility (I don't see the point myself, but hey)
• we might argue about whether the new definition is more tractable, but it certainly is more beautiful (again, IMHO), esp. as regards the free commutative monoid characterisation

[gallais]

Can't we have them all (and prove them equivalent if they are) rather than replacing?

[jamesmckinna]

Can't we have them all (and prove them equivalent if they are) rather than replacing?

Indeed... I suppose for me there is always a question of what gets 'blessed' as a definition, especially given that, on the one hand, the existing definitions have been the topic of (relatively speaking, so much) shade from other authors (including me ;) it feels like a definition tuned to correlate with TranspositionList, rather than being defined in its own right/on its own terms), and on the other, the tension around the library design philosophy about not having multiple definitions of the same thing (there are honorable exceptions, but I've always understood that as an ambient principle).

But if it does 'simply' get added as a new definition, then where should it live?

[gallais]

I would be in favour of having separate submodules.
We already have the case with Fin, albeit with a privileged version: Data.Fin.Permutation
(permutation as a bijection) and Data.Fin.Permutation.Transposition.List.

[jamesmckinna]

OK, I think that makes sense. One possibility, looking at the current organisation, is that each of Setoid and Propositional key off Homogeneous, so that module could be swapped out... but I'll work on doing it as a separate thing.

[jamesmckinna]

From Data.List.Relation.Binary.Permutation.Propositional:

-- An inductive definition of permutation

-- Note that one would expect that this would be defined in terms of
-- `Permutation.Setoid`. This is not currently the case as it involves
-- adding in a bunch of trivial `_≡_` proofs to the constructors which
-- a) adds noise and b) prevents easy access to the variables `x`, `y`.
-- This may be changed in future when a better solution is found.

Well, I've been wondering if this is the better solution? cf. the discussion of #1113 , where now, we could avoid trans as a constructor completely...

[JacquesCarette]

I'm also in favour of separate sub-modules.

And I, of course, have my own implementation, which is again different. See Bag.agda for the proof, and SetoidPermutation.agda for the relation, based on Conor's partitions (which I've generalized to Setoid), all available in the repo PureBaggery under Exploration/ .

I've been meaning to submit both codes on partitions on stdlib (Conor's already given assent to do so), I just have not had the time to actually do it.

[jamesmckinna]

@JacquesCarette writes:

And I, of course, have my own implementation, which is again different. See Bag.agda for the proof, and SetoidPermutation.agda for the relation, based on Conor's partitions (which I've generalized to Setoid), all available in the repo PureBaggery under Exploration/ .

Of course! (but without the hint/link, how would we know? etc. ;-))

Interesting that you don't need the 'merge' rule as such, or at least not in its 'symmetric' form, but I guess that is all wrapped up in the partition definitions, which I haven't looked at. Yours and Conor's version seems closest to the one I dub 'algorithmic' above...

And you develop all of the free commutative monoid machinery, too, which should please @Taneb and hopefully resolve #1281 to his satisfaction... Chapeau!

[JacquesCarette]

I develop it all twice, once the CS way, and once the Math way. The Math way, when spelled out in full, is quite silly - and thus its name in the repo.

[jamesmckinna]

So as a riposte, I've developed a branch off stdlib an interim measure, see #2317 which refactors to isolate all the dependency of Permutation on Homogeneous (as well as considerably simplifying/improving some proofs in Data.List.Relation.Binary.Permutation.Setoid.Properties along the way, specifically dropMiddleElement by proving a better version of split), with a view to then dropping in those Properties instead for the Hinze representation.

BREAKING change: Data.List.Relation.Binary.Permutation.Setoid thereby does not export the constructors of Homogeneous (and why should it?)

[jamesmckinna]

NB. See also #1354 and #1761 for comparison and prior thinking on the topic (including my own, which I had forgotten about 🤦 )

UPDATED: and a concrete proposal for how to take #1354 forward, as well as making space to support multiple (re-)implementations of the basic relation. Suggest maybe renaming this issue to

Refactor to support multiple definitions of `Data.List.Relation.Binary.Permutation`

both to avoid overlap with the originating #1354, and in the constructive spirit of the above responses arguing persuasively for such pluralism...?