-
Notifications
You must be signed in to change notification settings - Fork 235
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 Algebra.Action.*
and friends
#2350
base: master
Are you sure you want to change the base?
Conversation
Note to self: 'tipped' lists and the adjunction preserving |
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 Ralf Hinze pointed out to me last week that one may easily show an isomorphism between that and ... 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' |
Aha, a 2-sorted pointed unar! Nice. record 2PU (A B : Set) : Set where
field
push : (a : A) -> 2PU -> 2PU
point : (b : B) -> 2PU |
Looked at the code itself right now: I expect that in 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. |
So... as to "belongs elsewhere"... : where do you propose exactly? |
One could go crazy and do |
Re: your data TipList (A B : Set) : Set where
[_] : A ->TipList A B
_::_ : B -> TipList A B -> TipList A B the |
Sorry, I have "free theories" on the brain. Your |
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 ;-))! |
Yes, I agree with @JacquesCarette. I agree, splitting it into something like |
Lots of helpful feedback @MatthewDaggitt thanks! I'm undecided about As for |
Can you have actions on |
The classic example is "module" which is a |
I seem to be going round in circles redefining things repeatedly... DRY! Trying to fix this ... ... and need to rethink. Back to Draft... |
OK, I mean it this time...;-) Highlights of the most recent refactoring:
Possible further work: NOW DONE
|
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.
One super-minor thing (and a suggestion to a question left in the code).
Thanks very much @JacquesCarette for the very detailed feedback! |
Coda: @JacquesCarette did your allusion to 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: |
I realised writing the last comment that my fixation on Separately, by weakening things even further down to ... but, conversely/correspondingly, associativity is needed for the |
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 Have now done some experiments, and so have started to wonder if everything should be refactored so as to be parametrised on a (renamed) ... UPDATED: up to the fatal object/meta flaw, namely that |
Converting back to
|
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.
What is here is great. I'll review again when more stuff gets added.
I should reply to some specific comments: yes, definitely also including |
Fixes
the first part of#2348 .Currently in DRAFT for preliminary feedback.DONE:
CHANGELOG
IsX
with those of the correspondingRawX
#2252 ... but this seems debatable here? RESOLVED in favour of introducingSetoidAction
as a distinct thing, and then indexing wrt such a thing;_⋆_
structure definable inRaw*Action
and corresponding lifts in*Action
andFree
; RESOLVED the refactoring seems to have made this less evident than before, plus refactoring⋆-act-cong
to make the 'congruence' property more general...Pointwise
lifting of theSetoid
equality onList
gives rise to aMonoid
structure for[]
and_++_
... but this doesn't seem to be already defined/proved anywhere? DONE, but should be refactored downstreamRaw*Action
might better be described as aSetoid
homomorphism betweenM.setoid × A
andA
, only I can't seem to find a definition of the former (underRelation.Binary.Construct.Product
?) as a product ofSetoid
s? UPDATED: this lives under a mixture ofFunction
andData.Product.Function.NonDependent.Setoid
??? Discoverability epic fail again... sigh.RESOLVED: PR represents a(n uneasy) mixture of the two approachesREFACTORED again to postpone this perhaps in favour of a...Biased
implementation downstream?Issues (WON'T DOs):
*Action
and the correspondingMonoid
homomorphism (cf. Bundles forAlgebra.*Homomorphism
, and their algebra:Hom
-'sets' forAlgebra
#1960 ) betweenM
andEndo A
; BLOCKED on Port two Endomorphism submodules over to new Function hierarchy #2342MonoidAction
s...and where should that thing live?