Add `Algebra.Action.*` and friends #2350

jamesmckinna · 2024-04-09T14:41:38Z

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

DONE:

CHANGELOG
uses the method of indexing a thing over a raw thing cf. [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252 ... but this seems debatable here? RESOLVED in favour of introducing SetoidAction as a distinct thing, and then indexing wrt such a thing;
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...
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
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. Bundles for Algebra.*Homomorphism, and their algebra: Hom-'sets' for Algebra #1960 ) between M and Endo A; BLOCKED on Port two Endomorphism submodules over to new Function hierarchy #2342
a suitable notion of homomorphism of MonoidActions...and where should that thing live?

jamesmckinna · 2024-04-10T09:53:40Z

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

JacquesCarette · 2024-04-10T12:14:47Z

What's a 'tipped' list?

jamesmckinna · 2024-04-10T13:29:11Z

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 · 2024-04-10T14:13:25Z

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 · 2024-04-10T14:52:58Z

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 · 2024-04-10T16:19:24Z

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

JacquesCarette · 2024-04-10T16:58:49Z

Algebra.Action.Monoid would not be bad at all. To be more forward looking, 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 · 2024-04-10T21:39:15Z

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 · 2024-04-11T00:37:21Z

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 · 2024-04-11T02:54:18Z

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 · 2024-04-11T04:01:46Z

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!

src/Algebra/Construct/MonoidAction.agda

jamesmckinna · 2024-04-11T04:22:45Z

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 · 2024-04-11T04:26:12Z

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 · 2024-04-11T04:36:32Z

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 · 2025-01-18T11:40:12Z

Waking this up again, prompted by the discussion on #2553 / #2558 ...

JacquesCarette · 2025-01-21T14:35:52Z

You 'woke it up' but it is still Draft?

jamesmckinna · 2025-01-21T17:44:50Z

You 'woke it up' but it is still Draft?

Still DRAFT, yes, it was more a 'note to self' to mark explicit the link with #2558 and to think about more about how to streamline what is here, esp. Magma actions, and the way the passage from an algebra to an algebra of functions... makes things 'more associative' than the vanilla algebra.

Plus, still irritated about the (lack of) parametrisation on left/right... and want to make this 'better' if possible...?

JacquesCarette · 2025-06-26T15:11:10Z

Is perfect the enemy of the good here? Feels like there is quite a lot of quality stuff in here that could go in to v2.3.

jamesmckinna · 2025-06-26T18:41:18Z

Thanks @JacquesCarette , I just haven't had any spare focus to devote to this. For sure it could be v2.3-able, but given the short timescale, I'm happy to make this v2.4 or even v3.0, when I will have had more time to reconsider things?

JacquesCarette · 2025-06-26T19:31:14Z

You tagged the 'wrong' Jacques... I was merely asking you to think whether what's here is already (essentially) good enough to go in.

jamesmckinna · 2025-06-26T19:34:04Z

Thanks for the nudge. I'll try to look at this over the w/e

jamesmckinna · 2025-06-30T09:46:23Z

Some minimal restructuring (plus profiting from now actually having the (Is)Monoid structure/bundle on List with setoid equality), introducing definitions, and MagmaAction, but otherwise will leave anything to downstream refactoring, I think!

MatthewDaggitt

Given that I need to make a release candidate tomorrow, and there are several questions and at least one suspected bug in this code I'm going to bump this to v2.4

MatthewDaggitt · 2025-07-03T03:21:55Z

src/Algebra/Action/Structures.agda

+------------------------------------------------------------------------
+-- Basic definitions: fix notation
+
+record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where


Hmm is there a reason why the hierarchy in Structures is not the same as the hierarchy in Bundles? e.g. Bundles talks about setoids and monoids which don't feature here?

MatthewDaggitt · 2025-07-03T03:22:18Z

src/Algebra/Action/Definitions.agda

+    m n : M
+
+
+


Too many empty lines?

MatthewDaggitt · 2025-07-03T03:25:18Z

src/Algebra/Action/Definitions.agda

+Congruentʳ _◁_ = _◁_ Preserves₂ _≈_ ⟶ _≈ᴹ_ ⟶ _≈_
+
+IsActionˡ  : Actˡ → Op₂ M → Set (c ⊔ a ⊔ r)
+IsActionˡ _▷_ _∙_ = ∀ m n x → ((m ∙ n) ▷ x) ≈ (m ▷ (n ▷ x))


I don't like using the word Is here as it suggests that it is a Structure? Same for Identityˡ. Also by convention for the definitions we use Left and Right rather than the superscripts? Maybe LeftAction and LeftIdentity?

MatthewDaggitt · 2025-07-03T03:27:01Z

src/Algebra/Action/Definitions.agda

+open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
+
+module Algebra.Action.Definitions
+  {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r)


This module parameterisation doesn't work as many of these definitions either use neither or only one of the equalities. This will leave them ill-parameterised when this module is opened unapplied.

MatthewDaggitt · 2025-07-03T03:27:51Z

src/Algebra/Action/Structures.agda

+  _▷⁺_ : List⁺ M → A → A
+  (m ∷ ms) ▷⁺ a = m ▷ ms ▷⋆ a
+
+  ▷⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⋆ x) ≈ (ns ▷⋆ y)


Most of these lemmas would go in Algebra.Action.Properties modules by convention.

MatthewDaggitt · 2025-07-03T03:29:08Z

src/Algebra/Action/Construct/Self.agda

+------------------------------------------------------------------------
+-- Left- and Right- Actions of a Monoid over itself
+
+module Regular {c ℓ} (M : Monoid c ℓ) where


Why is this module called Regular and why is it parameterised by a Monoid? What other algebraic structures do we want to extend this by?

MatthewDaggitt · 2025-07-03T03:29:24Z

src/Algebra/Action/Construct/Self.agda

+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Algebra.Action.Construct.Self where


Should this be called Algebra.Action.Construct.Regular?

MatthewDaggitt · 2025-07-03T03:30:09Z

src/Algebra/Action/Construct/FreeMonoid.agda

+
+open import Relation.Binary.Bundles using (Setoid)
+
+module Algebra.Action.Construct.FreeMonoid


Is this module going to contain other Free actions? It already contains the free setoid action which suggests that it might be ill named?

jamesmckinna · 2025-07-03T07:18:31Z

Happy to bump while these things get sorted out!

JacquesCarette · 2025-07-30T20:29:20Z

I'd love to get this one going into v2.4!

jamesmckinna · 2025-07-31T09:19:13Z

I'd love to get this one going into v2.4!

Thank-you. As with a lot of recent comments from me, I take both encouragement from that, while noting that esp. @MatthewDaggitt 's review comments suggest that there is some way to go for a 'mature' design to emerge; despite my personal attachment to what's already here, I agree that it could be improved, but I need time/space/brains to think about it...

... which I'm not getting at the moment. Moving back to DRAFT, and bumping to (at least) v3.0.

jamesmckinna and others added 4 commits April 2, 2024 07:26

beginnings

b9845ce

factored out MonoidAction

43c9fdb

second beginning

a503156

start small(er)

e2a9815

jamesmckinna added addition low-hanging-fruit library-design labels Apr 9, 2024

jamesmckinna added this to the v2.1 milestone Apr 9, 2024

jamesmckinna marked this pull request as draft April 9, 2024 14:41

fix-whitespace

d9e6bc0

This was referenced Apr 9, 2024

Add Algebra.Construct.WreathProduct and/or Algebra.Construct.SemiDirectProduct #2351

Open

Add Algebra.Action.* #2348

Open

Update Function.Endomorphism.* to avoid use of deprecated Function.Equality #2299

Closed

jamesmckinna linked an issue Apr 9, 2024 that may be closed by this pull request

Add Algebra.Action.* #2348

Open

MatthewDaggitt reviewed Apr 11, 2024

View reviewed changes

refactor in favour of Pointwise congruence

d7a4ceb

CHANGELOG: added fresh entries

2534bd0

JacquesCarette approved these changes Jan 21, 2025

View reviewed changes

jamesmckinna and others added 5 commits June 30, 2025 09:13

Merge branch 'master' into monoid-action

64d3d1f

add: MagmaAction

f927cd0

fix: remove temporaries, streamline imports

cd3eac5

add: Definitions and refactor to use them

7fdeefc

fix: actually add Definitions

17f1530

jamesmckinna marked this pull request as ready for review June 30, 2025 09:44

jamesmckinna removed the status: blocked-by-issue Progress on this issue or PR is blocked by another issue. label Jun 30, 2025

jamesmckinna added this to the v2.3 milestone Jun 30, 2025

MatthewDaggitt reviewed Jul 3, 2025

View reviewed changes

MatthewDaggitt modified the milestones: v2.3, v2.4 Jul 3, 2025

Merge branch 'agda:master' into monoid-action

cbd8a9a

jamesmckinna marked this pull request as draft September 21, 2025 07:33

jamesmckinna modified the milestones: v2.4, v3.0 Sep 21, 2025

jamesmckinna and others added 2 commits September 21, 2025 08:35

update: CHANGELOG

d0d1e5e

Merge branch 'agda:master' into monoid-action

d4dc42b


		{-# OPTIONS --cubical-compatible --safe #-}

		module Algebra.Action.Construct.Self where


		open import Relation.Binary.Bundles using (Setoid)

		module Algebra.Action.Construct.FreeMonoid

Add Algebra.Action.* and friends #2350

Are you sure you want to change the base?

Add Algebra.Action.* and friends #2350

Uh oh!

Conversation

jamesmckinna commented Apr 9, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna commented Apr 10, 2024

Uh oh!

JacquesCarette commented Apr 10, 2024

Uh oh!

jamesmckinna commented Apr 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JacquesCarette commented Apr 10, 2024

Uh oh!

JacquesCarette commented Apr 10, 2024

Uh oh!

jamesmckinna commented Apr 10, 2024

Uh oh!

JacquesCarette commented Apr 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna commented Apr 10, 2024

Uh oh!

JacquesCarette commented Apr 11, 2024

Uh oh!

jamesmckinna commented Apr 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

MatthewDaggitt commented Apr 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jamesmckinna commented Apr 11, 2024

Uh oh!

MatthewDaggitt commented Apr 11, 2024

Uh oh!

jamesmckinna commented Apr 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jamesmckinna commented Jan 18, 2025

Uh oh!

JacquesCarette commented Jan 21, 2025

Uh oh!

jamesmckinna commented Jan 21, 2025

Uh oh!

JacquesCarette commented Jun 26, 2025

Uh oh!

jamesmckinna commented Jun 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JacquesCarette commented Jun 26, 2025

Uh oh!

jamesmckinna commented Jun 26, 2025

Uh oh!

jamesmckinna commented Jun 30, 2025

Uh oh!

MatthewDaggitt left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Add `Algebra.Action.*` and friends #2350

Add `Algebra.Action.*` and friends #2350

jamesmckinna commented Apr 9, 2024 •

edited

Loading

jamesmckinna commented Apr 10, 2024 •

edited

Loading

JacquesCarette commented Apr 10, 2024 •

edited

Loading

jamesmckinna commented Apr 11, 2024 •

edited

Loading

MatthewDaggitt commented Apr 11, 2024 •

edited

Loading

jamesmckinna commented Apr 11, 2024 •

edited

Loading

jamesmckinna commented Jun 26, 2025 •

edited

Loading

MatthewDaggitt left a comment •

edited

Loading

jamesmckinna commented Jul 31, 2025 •

edited

Loading