Add Number literals for any SuccessorSet

[jamesmckinna]

Fixes #1363

NB:

• naming/hierarchy: adds Algebra.Literals rather than Algebra.Structures.Literals
• fixes spurious over re-export in Algebra.Bundles.SuccessorSet
• in-place implementation of fromℕ, rather than defining that as the unique morphism from Algebra.Construct.Initial.SuccessorSet UPDATED: made the definition local, to future-proof the API
• TODO (downstream?): as with [fixes #2273] Add SuccessorSet and associated boilerplate #2277 adds no new {Is}SuccessorSet structures/bundles to existing Algebra.* nor Data.* in order to be able to create Number instances; cf. discussion on the issue as to where/how to create the 'right' ones so that they are consistently implemented across the whole *Ring* hierarchy in such a way as to have the 'right' properties...

Issue:

• should the module parameter be supplied as an instance? as a RawSuccessorSet?

Could be v2.1 or v2.2?

[JacquesCarette]

Tiny tweak and a question.

[jamesmckinna]

A potential problem (but not, perhaps, in practice?): the Number implementations defined

• in Data.Nat.Literals for Agda.Builtin.Nat.Nat, and
• (hypothetically at this stage) in Data.Nat.Properties for Data.Nat.Base.ℕ via isSuccessorSet

will be distinct: the second, in particular, will be (needlessly) more strict in its implementation of fromNat, than the first.

Is this a genuine problem? If so, what's the 'best' way to finesse this, except via separate, 'hand-cut' implementations of Number on a case-by-case basis?

[JacquesCarette]

I do wonder if this is a genuine problem, at least in the context of Agda. [It might be!] It feels like a conundrum that is more philosophical: is stdlib trying to support prove-first-program-second Agda, or something else? There's a different library for program-first-prove-sometimes for Agda.

Of course, the most interesting would be prove-AND-program, with a purposefully symmetric operator in there. Agda sure doesn't feel ready for that.

[jamesmckinna]

I do wonder if this is a genuine problem, at least in the context of Agda. [It might be!] It feels like a conundrum that is more philosophical: is stdlib trying to support prove-first-program-second Agda, or something else? There's a different library for program-first-prove-sometimes for Agda.

Of course, the most interesting would be prove-AND-program, with a purposefully symmetric operator in there. Agda sure doesn't feel ready for that.

Returning to this comment, I wondered a lot about the first part: stdlib can often feel, in its structural organisation, that it is program-first (via Data.X.Base), and then prove afterwards (via Data.X.Properties). Or am I missing something?

The second part, I don't really understand at all: how would we get a symmetric operator out of fromNat? (Or was this comment intended for another thread elsewhere?)

[JacquesCarette]

Returning to this comment, I wondered a lot about the first part: stdlib can often feel, in its structural organisation, that it is program-first (via Data.X.Base), and then prove afterwards (via Data.X.Properties). Or am I missing something?

You are quite right that, structurally, stdlib feels program-first. But it is proof-first in its actual details, for the most part, i.e. the definitions in Data.X.Base are usually the ones that make proofs easy.

Of course, the most interesting would be prove-AND-program, with a purposefully symmetric operator in there. Agda sure doesn't feel ready for that.

The second part, I don't really understand at all: how would we get a symmetric operator out of fromNat?

My bad, what I wrote was not clear: I mean that 'AND' to be at the meta-level, to be a symmetric operation on 'prove' and 'program' as concepts!

[jamesmckinna]

Back to the philosophical question: of course it makes no difference for Nat: because data.Nat.Instances doesn't need to change its definition of literals via Number?

Accordingly, I suggest either merging this now, or else putting to draft while I add all the IsSuccessorSet implementations throughout the library: but maybe that's better as a downstream PR? Thoughts welcome!

[JacquesCarette]

Merging this now probably makes sense, but I'd want a concurring opinion - perhaps @gallais who has already looked at it?

[jamesmckinna]

@gallais this is one we missed in our meeting on Friday. Are you willing to approve/merge?

[MatthewDaggitt]

As this is something that can't be reasoned about internally in Agda, I'd be willing to approve if we added some test cases somewhere? Either in a private block, or more ideally in a very short README file?

[jamesmckinna]

I'll try to come back to this soon, after I've cleared a lot of other cruft out of my head, and can page this one back in. But it's not a deal-breaker for v2.2., so happy to push back (to v2.3 or v3.0) if that's helpful?

[jamesmckinna]

I'm going to shelve this, as I'm not even sure now about the design, and not quite sure how best to fulfil @MatthewDaggitt 's request for 'test' data...

[MatthewDaggitt]

not quite sure how best to fulfil @MatthewDaggitt 's request for 'test' data...

For the future if this is revisited, I would take a SuccessorSet bundle, create the relevant instance and then try writing 0, 1, 2 etc...

[jamesmckinna]

Thanks @MatthewDaggitt for the steer.
The reason for my wobble/hesitation about all this was the sense that, yes, you really could define an interpretation of n : ℕ (indeed, for Ring, of i : ℤ) out of suc# (suc# (... zero#)...) (given by the unique morphism from the free SuccessorSet!), but that by contrast with primitive numerical literals, these things wouldn't compute properly, nor be exactly what you want, which I think is much more like extending the signature of suitable algebras to include numerals as syntax... that is to consider the free extension of suitable algebras via the interpretation. Maybe this PR is worth pursuing for its own sake, but I wonder if it would benefit from some more thought,... and returning to implementing Free things first.
But perhaps this is an instance of making 'the perfect the enemy of the good'?

[MatthewDaggitt]

I mean if we don't have a compelling use case, then I'm not sure if we should be adding them. So in that sense, yes happy to leave this as draft and revisit later.