[fixes #1363] Add `Algebra.Literals`

[jamesmckinna]

Possible fix for #1363 .

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

• based on #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.

[jamesmckinna]

@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]

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]

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]

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]

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]

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?

[jamesmckinna]

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]

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 #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. #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]

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]

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]

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

[jamesmckinna]

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