Add `Algebra.Action.*` and friends

[jamesmckinna]

Fixes the first part of #2348 . Currently in DRAFT for preliminary feedback.

DONE:

• [x] CHANGELOG
• [x] uses the method of indexing a thing over a raw thing cf. #2252 ... but this seems debatable here? RESOLVED in favour of introducing SetoidAction as a distinct thing, and then indexing wrt such a thing;
• [x] repetition between the _⋆_ structure definable in Raw*Action and corresponding lifts in *Action and Free; RESOLVED the refactoring seems to have made this less evident than before, plus refactoring ⋆-act-cong to make the 'congruence' property more general...
• [x] such structure also depends on showing that Pointwise lifting of the Setoid equality on List gives rise to a Monoid structure for [] and _++_... but this doesn't seem to be already defined/proved anywhere? DONE, but should be refactored downstream
• [x] a Raw*Action might better be described as a Setoid homomorphism between M.setoid × A and A, only I can't seem to find a definition of the former (under Relation.Binary.Construct.Product?) as a product of Setoids? UPDATED: this lives under a mixture of Function and Data.Product.Function.NonDependent.Setoid??? Discoverability epic fail again... sigh. RESOLVED: PR represents a(n uneasy) mixture of the two approaches REFACTORED again to postpone this perhaps in favour of a ...Biased implementation downstream?

Issues (WON'T DOs):

• the equivalence of a *Action and the corresponding Monoid homomorphism (cf. #1960 ) between M and Endo A; BLOCKED on #2342
• a suitable notion of homomorphism of MonoidActions...and where should that thing live?

[jamesmckinna]

Note to self: 'tipped' lists and the adjunction preserving List as an initial algebra.

[JacquesCarette]

What's a 'tipped' list?

[jamesmckinna]

What's a 'tipped' list?

A datatype I first learnt of from Conor (possibly invented by him? In any case, early 2000s in Durham IIRC): it's analogous to List A, except that at nil you can store a value of some (other) type B (and various games one might play as to whether that type is existentially/universally quantified, or merely supplied as an additional parameter).

Ralf Hinze pointed out to me last week that one may easily show an isomorphism between that and (List A) * B because _ * B, having a right adjoint, preserves colimits/initial algebras...

... and there may (ought to!) be some relationship with the Minamide construction (POPL, 1998) in connection with tail recursion modulo constructors...

in any case, such a tipped list corresponds to a symbolic/'non-materialised' fold, and hence to the iterated monoid action (which materialises it!), generalising difference lists etc.

[JacquesCarette]

Aha, a 2-sorted pointed unar! Nice.

record 2PU (A B : Set) : Set where
  field
    push : (a : A) -> 2PU -> 2PU
    point : (b : B) -> 2PU

[JacquesCarette]

Looked at the code itself right now: I expect that in Algebra.Construct.MonoidAction, all I will find are constructions of monoid actions. I did not expect to find the definition of the representation of an action to be in the same file. This belongs elsewhere.

I'm happy for the construction (at the end of the file) to stay where they are, but not so for the definition of the concepts themselves.

[jamesmckinna]

So... as to "belongs elsewhere"... : where do you propose exactly?

[JacquesCarette]

Algebra.Action.Monoid would not be bad at all. To be more forward look, maybe Algebra.Action.Bundles or something like it.

One could go crazy and do Algebra.MultiSorted.Action.Bundles but I think that's overkill, even if "not wrong".

[jamesmckinna]

Re: your 2PU... I was more thinking

data TipList (A B : Set) : Set where
  [_] : A ->TipList A B
  _::_ : B -> TipList A B -> TipList A B

the record version is... the 'wrong' way round?

[JacquesCarette]

Sorry, I have "free theories" on the brain. Your TipList is the object part of the left adjoint to the forgetful functor from 2PU to Set x Set. (Urg, I hate how that sounds - I'm not a big fan of lathering on categorical lingo unless it actually enlightens.)

[jamesmckinna]

Sorry, I have "free theories" on the brain. Your TipList is the object part of the left adjoint to the forgetful functor from 2PU to Set x Set. (Urg, I hate how that sounds - I'm not a big fan of lathering on categorical lingo unless it actually enlightens.)

Thanks for the clarification! I think I had at least glimpsed that from my reference to direction... but I hadn't joined all the dots. And so, no need to apologise, the category theory is fine (and helpful ;-))!

[MatthewDaggitt]

Yes, I agree with @JacquesCarette. X.Construct modules are for building records found in X.Structures/Bundles.

I agree, splitting it into something like Algebra.Action.Bundles and Algebra.Action.RawBundles makes sense to me!

[jamesmckinna]

Lots of helpful feedback @MatthewDaggitt thanks!

I'm undecided about Algebra.Action.Bundles vs Algebra.Action.Monoid, preferring the latter until we have more examples of the phenomenon?

As for Raw, I'm wondering if it's easier to start from a Func (M.setoid ×ₛ A) A, packaging the congruence data, and not introducing a new type for the sake of it...

[MatthewDaggitt]

I'm undecided about Algebra.Action.Bundles vs Algebra.Action.Monoid, preferring the latter until we have more examples of the phenomenon?

Can you have actions on Semigroup or Ring or other structures?

[jamesmckinna]

The classic example is "module" which is a Ring acting on an AbelianGroup... etc. or indeed Ring itself as a Monoid action on an AbelianGroup with the same underlying Setoid

[jamesmckinna]

Temporarily defeated by the complexity of the refactoring... sigh. But nearly there!

[jamesmckinna]

Currently the IsRaw* structures aren't really raw, but vanilla Setoid structures (with cong)... so further refactoring might be in order to tease those apart. But let's turn this over to review in the meantime?

UPDATED collapsed Raw back into Structures...

[jamesmckinna]

Thanks very much to @JacquesCarette for the review comments. I've updated to partly 'streamline', and partly to leave hooks for downstream generalisation. Not convinced it's an overall improvement though!

[jamesmckinna]

Given the trouble I've had thinking about this, no longer sure this is low-hanging-fruit...

[jamesmckinna]

Recent commits:

• fix notations to be asymmetric in Structures
• simplify definitions of Bundles (so: a Biased version might be useful for deriving Actions from Funcs of suitable type)
• rename Free to FreeMonoid, but now the module structure needs simplification

TODO (?):

• define the Action property in Algebra.Definitions... multi- vs. single-sorted distinction again...? ;-)

[jamesmckinna]

@JacquesCarette back now ready for review, but I dare say there'll be more to discuss!

[jamesmckinna]

I seem to be going round in circles redefining things repeatedly... DRY! Trying to fix this ...

... and need to rethink. Back to Draft...

[jamesmckinna]

@JacquesCarette back now ready for review, but I dare say there'll be more to discuss!

OK, I mean it this time...;-)

Highlights of the most recent refactoring:

• sort out the dependencies to reduce duplication/get things 'right'
• naming: (iterated) action properties now take their names from the Monoid, not from the underlying action map

Possible further work: NOW DONE

• move ListAction from Bundles to Construct.FreeMonoid, because they are they are the Setoid analogues of the free Monoid iterated actions... and perhaps don't need to be 'free-standing' in Bundles...?

[jamesmckinna]

Thanks very much @JacquesCarette for the very detailed feedback! I think I'd be happy to leave to a subsequent refactoring the lifting out of the -act properties to a separate Algebra.Action.Definitions module, but I can start to see how that might go... and how that might help keep things straight when passing from one action to its iterated form...

[jamesmckinna]

Coda: @JacquesCarette did your allusion to NonEmpty lists mean that you also might want:

module SemigroupAction (M : Semigroup c ℓ) (A : Setoid a r) where

  private

    open module M = Semigroup M using (_∙_; setoid)
    open module A = Setoid A using (_≈_)

  record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ)
    where

    open SetoidAction.Left leftAction public

    field
      ∙-act  : ∀ m n x → m ∙ n ▷ x ≈ m ▷ n ▷ x

(and: MagmaAction even!?) with MonoidAction being refactored to have a SemigroupAction subfield...?

[jamesmckinna]

I realised writing the last comment that my fixation on Monoid actions blinded me to the simpler structures, and with it, Krohn-Rhodes decomposition.

Separately, by weakening things even further down to MagmaAction, then we would get to observe that the additional generality afforded by actions, namely that associativity is not even an optional thing for these structures, because the ∙-act axiom essentially forces a version of associativity of the action map, even when/if the _∙_ structure itself is not associative...

... but, conversely/correspondingly, associativity is needed for the Algebra.Construct.Self actions...

[jamesmckinna]

I think it now looks a lot more tight, but please feel free to re-review @JacquesCarette and @Taneb : I've tried to honour the spirit of your most recent round of comments, so many thanks for the nudge(s) to do so.

Only thing left outstanding would be to factor out the Algebra.Action.Definitions, but that can happen later? Happy to do it now, for completeness's sake, if you think it would improve the overall contribution.

Have now done some experiments, and so have started to wonder if everything should be refactored so as to be parametrised on a (renamed) Boolean (L/R) so that all the Left/Right duplication can be avoided...?

... UPDATED: up to the fatal object/meta flaw, namely that record field names can't be parametrised on an internal value... sigh. Won't pursue this!

[jamesmckinna]

Converting back to DRAFT while I figure out:

• [ ] Algebra.Action.Definitions
• [ ] MagmaAction and SemigroupAction
• [ ] consequences of the above for Construct.Self (OK for Semigroup, by associativity; not so for Magma!) and Construct.FreeMonoid (might want to revert to Free to include Semigroup case as well?)

[JacquesCarette]

I should reply to some specific comments: yes, definitely also including SemigroupAction and MagmaAction are things that I had in mind. MonoidAction as you subsequently discovered (and I discovered the hard way as well) is too special to offer sufficient insight into actions in general (the same is true of Monoid, and I've fallen into that trap too.)