[fixes #1363] Add `Algebra.Literals` #2264

jamesmckinna · 2024-01-24T10:16:23Z

Possible fix for #1363 .

The design, at present, is pretty convoluted (I felt as though I were writing SML functors again!):

based on [DRY] Reconciling the indices of IsX with those of the corresponding RawX #2252 , defines IsPointedMonoid as an extension of RawMonoid by an abstract point, in Algebra.Structures.Pointed;
defines abstract Literals for such structures in-place, using Algebra.Definitions.RawMonoid._×_;
defines their associated Number instance in Algebra.Structures.Literals;
defines PointedMonoid bundles, in Algebra.Bundles.Pointed, and their associated Number instance in Algebra.Bundles.Literals;
constructs an instance from a SemiringWithoutAnnihilatingZero using 1# as the point;
re-exports the Number instance for such from Algebra.Literals.

I would really welcome a review, with hints as to 'sensible' refactoring, if any.

JacquesCarette

I only understood the point of this once I read through all the backlog, including #1363.

So I think the smallest algebra that has Number in it is "pointed unar" (single point, single unary operation). BiPointedMonoid is a really weird thing! (I know it is called PointedMonoid, but to me, Pointed means 1 point, not 2).

JacquesCarette · 2024-01-26T22:01:42Z

src/Algebra/Bundles/Pointed.agda

+    rawMonoid  : RawMonoid c ℓ
+  open RawMonoid rawMonoid using (Carrier)
+  field
+    •      : Carrier


The comment "1 binary operation & 2 elements" is correct, but the rest of the names (Pointed, etc) give the wrong impression of having a single distinguished element. BiPointed ?

Much to think about here. Ever since my abortive Pointed draft PRs #1958 #1963 , I've been thinking about PointedX (and how to formalise the lift map/pointed extension operation from X in a 'signature polymorphic' way) in general...

The two points in PointedMonoid play distinct roles, so I'm unhappy to identify them as '2 points', because one is distinguished as an identity, while the other is an unconstrained extension of the signature...

... that said, BiPointedSet/BiPointedMagma do make sense, especially as Raw bundles, but I've always been resistant to universal algebra ideas in this regard precisely because not all 'freely constructed' such signatures make sense in the absence of additional structure...?

So from my POV, I'd want to keep things more cleanly separated...

Nitpick: they do "make sense", but they are not necessarily sufficiently useful. Phrased that way, I'd say that our current state of knowledge makes this true. [Usefulness is a temporal quality, not absolute.]

The next question is: that extra point, is it meant to be preserved by homomorphisms or not? If not, then rather than Pointed what you're describing is Inhabited (I'm writing that up separately, i.e. the observation that the category whose objects are pairs of a type and a point of that type, but whose homomorphisms don't preserve that point, are exactly the inhabited types, without needing to have a notion of truncation).

Of course, a Monoid is always inhabited -- the right name here would be NonTrivialMonoid although that's tricky as the one-point monoid is a model as you don't actually want to assert that the extra point is not unit! Best you might be able to do is to ask that the obvious homomorphism induced by 'swap' not be homotopic to the identity.

Also an excellent observation (although I'm still insufficently homotopically-inclined to arbitrate on the last point). I think that points should be preserved (esp. in this setting, because _+ pt is the unary operation at hand, and we want it as (part of) ~~an NNO-instance~~ a SuccessorSet instance to be preserved?

And NonTrivialMonoid...: does that exclude the case 0# = 1#? I wouldn't want to insist on that...?

jamesmckinna · 2024-01-27T06:59:34Z

@JacquesCarette you wrote

I only understood the point of this once I read through all the backlog, including #1363.

Apologies for not providing enough context! As one of the commenters in the original issue, I'd imagined (magical thinking) that you'd still be across the issue (plus: never being entirely clear where 'detailed design discussion' belongs... on the issue, or on the pR?)

It might have been easier to follow the original suggestion and simply use Semiring..., and structure the development around having the literal numerals arise as a Semiring... homomorphism, but I'd also been trying to follow the library style of introducing operations as minimally-committed as possible, and then building properties on top of that (that gloss may reveal that I have misunderstood ...).

I'd reached the present PR in that spirit: 1# isn't special as a point, until you start to try build up towards the homomorphism property (most of the pieces of which are in fact already present in various places), and for numerals, that additional structure isn't needed.

Identifying (Bi)PointedMonoid was the surprising outcome of that journey.

Your comments are very helpful... and (Bi)PointedUnary suggests perhaps a better attack via MonoidAction/NNO, with Nat inducing a lot of structure via freeness/initiality...?

JacquesCarette · 2024-01-27T14:34:24Z

Facing the fact that there's only so much that I can keep in active memory all the time...

My current feeling is indeed that PointedUnary (whose initial algebra is the carrier forNat) is the originator of much of the structure, which does get pushed around via MonoidAction / NNO.

jamesmckinna · 2024-01-28T11:05:11Z

PointedUnary, or NNO as the 'official' name for this? (I lean towards the latter, for historical/mathematical/categorical reasons; others may prefer the former for consistency/uniformity reasons with the rest of the library...)

JacquesCarette · 2024-01-28T14:38:03Z

Is it actually an NNO though? Weak NNO even? The issue is that this is just that data part of NNO and none of the properties.

So it's rawNNO, in a sense. Which is rather bleh. (I'm not a big fan of PointedUnary btw, but at least you don't expect any laws to hold.)

jamesmckinna · 2024-01-28T15:15:13Z

Is it actually an NNO though? Weak NNO even? The issue is that this is just that data part of NNO and none of the properties.

So it's rawNNO, in a sense. Which is rather bleh. (I'm not a big fan of PointedUnary btw, but at least you don't expect any laws to hold.)

Good point. But I think I'd be happier (given the intended mode-of-use of this PR) to call it RawNNO?

UPDATED: IIRC, the only thing we would require of an IsNNO, as distinct from the Raw version would be that the 'successor' be a congruence. The only 'laws' one really expects to hold concern NNO-homomorphisms, so I don't think that anything need be 'weak' about this at all? Previously I wrote

Or am I missing something?

yes! yes! yes! I've been a total idiot ignoring initiality... apologies to all, especially @JacquesCarette , for my idiocy on this point.

JacquesCarette · 2024-01-28T16:26:19Z

I fully agree that if it is defined locally in this file, then RawNNO makes sense. But is it, or is it going to fit in the full Algebra hierarchy?

MatthewDaggitt

The design, at present, is pretty convoluted

Agreed. This PR needs some serious thinking about the design.

it needs a README file to show it actually works...
Is Pointed supposed to be whole new subhierarchy? If so it should go under Algebra.Pointed.(Structures/Bundles) rather than Algebra.(Structures/Bundles).Pointed
Having said that why do we need such generality? I feel we could get this working in about 5 lines of code in Algebra.Properties.SemiringWithoutAnnihilatingZero without needing to go through add 5 new modules, an entire new algebraic subhierarchy, and an entire new way of indexing algebraic structures. I think we need a pretty convincing argument for the need for the extra generality to justify all of this.

MatthewDaggitt · 2024-01-30T02:59:00Z

src/Algebra/Bundles/Literals.agda

+
+open PointedMonoid pointedMonoid
+
+-- Re-export `Number` instance defined in Algebra.Structures.Literals


There is no instance defined in Algebra.Structures.Literals....

No, but this seems to be the model in eg Data.Nat.Literals which I had been mindlessly following...

MatthewDaggitt · 2024-01-30T03:01:09Z

src/Algebra/Structures/Pointed.agda

+
+record IsPointedMonoid
+  (rawMonoid : RawMonoid c ℓ)
+  (• : RawMonoid.Carrier rawMonoid) : Set (c ⊔ ℓ)


I'm confused. You don't have a not equal to assumption between • and ε so there's not necessarily two elements...

Absolutely! Degenerate instances are/should always be possible: we don't insist that 0# not be equal to 1# in (Semi)ring*, for example.
So perhaps the comment is bad, but this was mindless/lazy cut-and-paste from Algebra.*...

MatthewDaggitt · 2024-01-30T03:01:30Z

src/Algebra/Structures/Pointed.agda

+  _×• : ℕ → Carrier
+  n ×• = n × • where open Definitions rawMonoid
+
+  module Literals where


Why define this as a named module, and not just a Number record directly?

I had stymied myself with imports from Agda.Builtin.FromNat, perhaps in the mistaken belief that that was how Number instances get introduced...

I had (for some reason) wanted to distinguish between the declaration of a module defining the implementation, from its export via a number : Number ... definition elsewhere...

jamesmckinna · 2024-01-30T16:10:59Z

So, thanks to each of you for the feedback on what was an 'essay'/attempt to attack the problem, while balancing a lot of ... competing tensions in how/where the library might be extended, esp. in respect of Pointed structure.

I'd be very happy to retire this one (or move it to DRAFT) while we revisit the originating issue to discuss how to tackle an acceptable solution. But like many 'leftover' so-called low-hanging-fruit issue, I was surprised where this one took me, once I started to take the idea more seriously in the spirit of 'put things at the place of maximum generality/reusability'...

(Meta: I maintain a tab of the list of low-hanging-fruit issues since 2020, and periodically pick one up to play with... but I'm conscious that some of those should be closed, but weren't at the time that a PR was posted which did fix them, and some of them, like this, end up more intricate than at first sight appears. But grateful to @MatthewDaggitt for the hint, sometimes at least, to not over-think things... ;-))

jamesmckinna · 2024-01-31T12:55:18Z

The design, at present, is pretty convoluted

@MatthewDaggitt wrote:

This PR needs some serious thinking about the design.

Agreed! My approach may be flawed, but it seems as though this hasn't been picked up since late 2020 when it was first proposed. I'd been picking at it on and off since 2021, but this was my first 'concentrated' effort since then.

1. it needs a `README` file to show it actually works...

OK.

2. Is `Pointed` supposed to be whole new subhierarchy? If so it should go under `Algebra.Pointed.(Structures/Bundles)` rather than `Algebra.(Structures/Bundles).Pointed`

That's a very good question! I had been following my nose a bit, given earlier attempts with the simplest cases of such a hierarchy, and wondering, but not (oops! this got left out earlier) committing to, the thought that perhaps, indeed, we did?

3. Having said that why do we need such generality? I feel we could get this working in about 5 lines of code in `Algebra.Properties.SemiringWithoutAnnihilatingZero` without needing to go through add 5 new modules, an entire new algebraic subhierarchy, and an entire new way of indexing algebraic structures. I think we need a pretty convincing argument for the need for the extra generality to justify all of this.

All fair points. And on that basis, I'd be happy to withdraw this, in favour of someone coming up with just such a simpler solution, save for the following:

we will want, eventually, to have something equivalent to {Raw}NNO in the library, won't we? And this does seem to be the actually minimal node (rather than the posited SemiringWithoutAnnihilatingZero) in the hierarchy where the nth iterate (starting at 0#) of _+ 1# belongs, or not? It doesn't need Semiring... until and unless you want to prove that it defines a Semiring... homomorphism from Nat to its image in the given algebra; but even then, that actual image itself is in fact already a Semiring by virtue of the various homomorphism properties proved for the n ×_ operation in Algebra.Properties.Monoid.Mult... (I think!); see also lemmas about semiring structure induced by _× x #2272
that said, none of that Semiring... structure per se appears in the interpretation of the Number literals themselves as constants in the Carrier of a suitable algebra (they don't care what arithmetic they enjoy! they're 'just numerals')), so NNO seems the 'sweet spot' for such a thing?
happy to give way on the Pointed hierarchy, but it draws attention to how the existing approach (not indexing over a Raw bundle, but over its flattening into a telescope) actually makes it harder to entertain such extensions, or to systematically adding derived operations cf. Missing derived operations in Algebra.Structures.IsGroup/Algebra.Bundles.Raw.RawGroup #2268 ... IMHO.

These points might be moot for the time being, but I can't help thinking they will return as issues... eventually. So I had started to explore the consequences of thinking about how they might affect this specific PR... hope that goes some way to explaining, if not justifying, the avenues I'd taken here.

jamesmckinna · 2024-02-02T13:10:05Z

On naming:
we currently have the following choices for an Algebra with a distinguished point (0#? or ‵zero, because it's a 'quoted' version of Agda.Builtin.Nat.zero?)) and unary operation (suc#, or _+1#, or ‵suc because it's a 'quoted' version of Agda.Builtin.Nat.suc?):

PointedUnary? ... the universal algebra way;
NNO/NaturalNumber(s)Object? ... the Lawvere/categorical way;
SuccessorSet? ... the Dedekind way

Can we agree on 'sensible' choices from this palette?

JacquesCarette · 2024-02-02T19:59:51Z

I am happy to entertain any of PointedUnary, RawNNO and SuccessorSet. I feel that a no-laws NNO seems like squatting over a good name prematurely.

jamesmckinna · 2024-02-16T12:01:35Z

Will revisit as and when #2277 gets merged...

jamesmckinna · 2024-04-08T12:05:00Z

Suggest closing this in favour of a fresh start based on #2277 and #2272 .

possible fix for agda#1363

018aa65

jamesmckinna linked an issue Jan 24, 2024 that may be closed by this pull request

Literals for any ring? #1363

Open

jamesmckinna added addition library-design refactoring discussion dependencies labels Jan 24, 2024

jamesmckinna requested review from JacquesCarette, Taneb and gallais January 24, 2024 11:19

JacquesCarette requested changes Jan 26, 2024

View reviewed changes

Merge branch 'master' into pointed-monoid-literals

1ac3d52

MatthewDaggitt requested changes Jan 30, 2024

View reviewed changes

jamesmckinna mentioned this pull request Feb 2, 2024

lemmas about semiring structure induced by _× x #2272

Merged

This was referenced Feb 3, 2024

Add Algebra.Bundles.SuccessorSet and related records #2273

Closed

[fixes #2273] Add SuccessorSet and associated boilerplate #2277

Merged

jamesmckinna marked this pull request as draft February 8, 2024 10:01

jamesmckinna closed this Apr 8, 2024

jamesmckinna removed a link to an issue Jun 4, 2024

Literals for any ring? #1363

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[fixes #1363] Add `Algebra.Literals` #2264

[fixes #1363] Add `Algebra.Literals` #2264

jamesmckinna commented Jan 24, 2024 •

edited

Loading

JacquesCarette left a comment

JacquesCarette Jan 26, 2024

jamesmckinna Jan 27, 2024 •

edited

Loading

JacquesCarette Jan 27, 2024

JacquesCarette Jan 27, 2024

jamesmckinna Jan 27, 2024 •

edited

Loading

jamesmckinna Jan 27, 2024

jamesmckinna commented Jan 27, 2024 •

edited

Loading

JacquesCarette commented Jan 27, 2024

jamesmckinna commented Jan 28, 2024 •

edited

Loading

JacquesCarette commented Jan 28, 2024

jamesmckinna commented Jan 28, 2024 •

edited

Loading

JacquesCarette commented Jan 28, 2024

MatthewDaggitt left a comment •

edited

Loading

MatthewDaggitt Jan 30, 2024

jamesmckinna Jan 31, 2024

MatthewDaggitt Jan 30, 2024

jamesmckinna Jan 31, 2024

MatthewDaggitt Jan 30, 2024

jamesmckinna Jan 31, 2024

jamesmckinna commented Jan 30, 2024

jamesmckinna commented Jan 31, 2024 •

edited

Loading

jamesmckinna commented Feb 2, 2024

JacquesCarette commented Feb 2, 2024

jamesmckinna commented Feb 16, 2024

jamesmckinna commented Apr 8, 2024


		open PointedMonoid pointedMonoid

		-- Re-export `Number` instance defined in Algebra.Structures.Literals

[fixes #1363] Add Algebra.Literals #2264

[fixes #1363] Add Algebra.Literals #2264

Conversation

jamesmckinna commented Jan 24, 2024 • edited Loading

JacquesCarette left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jamesmckinna Jan 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jamesmckinna Jan 27, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jamesmckinna commented Jan 27, 2024 • edited Loading

JacquesCarette commented Jan 27, 2024

jamesmckinna commented Jan 28, 2024 • edited Loading

JacquesCarette commented Jan 28, 2024

jamesmckinna commented Jan 28, 2024 • edited Loading

JacquesCarette commented Jan 28, 2024

MatthewDaggitt left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jamesmckinna commented Jan 30, 2024

jamesmckinna commented Jan 31, 2024 • edited Loading

jamesmckinna commented Feb 2, 2024

JacquesCarette commented Feb 2, 2024

jamesmckinna commented Feb 16, 2024

jamesmckinna commented Apr 8, 2024

[fixes #1363] Add `Algebra.Literals` #2264

[fixes #1363] Add `Algebra.Literals` #2264

jamesmckinna commented Jan 24, 2024 •

edited

Loading

jamesmckinna Jan 27, 2024 •

edited

Loading

jamesmckinna Jan 27, 2024 •

edited

Loading

jamesmckinna commented Jan 27, 2024 •

edited

Loading

jamesmckinna commented Jan 28, 2024 •

edited

Loading

jamesmckinna commented Jan 28, 2024 •

edited

Loading

MatthewDaggitt left a comment •

edited

Loading

jamesmckinna commented Jan 31, 2024 •

edited

Loading