[ new ] added IsMagma, RawMagma and Magma to Algebra

[MatthewDaggitt]

Self explanatory. In response to @JacquesCarette comment in #455, and the fact that it'll be useful in an upcoming pull request.

It's almost physically painful to do so (:cry:) but I've left the definition IsSemigroup as is, instead of changing it to use IsMagma for backwards compatibility reasons.

[gallais]

Should we have various isMagma proofs in Data.Nat, Data.List, etc.?

[JacquesCarette]

Having such proofs (of isMagma) is probably not timely. Really there should be further algebras (loop, quasigroup, diod, squag, quandle, ...) first created. There are about 200 of these in common use in mathematics. That would give the appropriate scale of the problem. Then one could consider what the best way to provide all the 'obvious' instances.

[JacquesCarette]

And not that the backward incompatibility problem that @MatthewDaggitt talked about is going to get much worse if a haphazard method of developing the algebraic hierarchy is used. The ITP-2010 paper "Type Classes for Mathematics in Type Theory" (https://arxiv.org/abs/1102.1323) discusses some of the scaling issues.

Full disclosure: I've been working on this problem for a while (some first results in 'Theory Presentation Combinators' - https://arxiv.org/abs/1204.0053). It's thorny. I am hoping to do some experiments atop Agda (instead of inside a custom language) instead.

[MatthewDaggitt]

@JacquesCarette that's a very good point. Adding various structures one-by-one is going to result in many of these sub-optimal record definitions.

I'm not sure what to suggest though as a solution. Maybe we should have a concerted effort at some point to try and add as many as possible of the 200 odd in at the same time?

[JacquesCarette]

Adding all of them at once works if you're sure you won't miss any - something I would never bet on.

A better mechanism is to use some amount of meta-programming which creates record definitions from a set of theory combinators. The resulting definitions would be flat, and thus any missing piece of the puzzle could be added post-factor without disturbing previous definitions.

The problem with the current definitions is that they expose the process by which there were built up.

[MatthewDaggitt]

Hmm so I'm really needing Magma.

A better mechanism is to use some amount of meta-programming which creates record definitions from a set of theory combinators. The resulting definitions would be flat, and thus any missing piece of the puzzle could be added post-factor without disturbing previous definitions.

@JacquesCarette do you have any suggestions about how to go about doing this?

If not, then my proposal is to take advantage of v1.0 to adjust IsSemigroup to use IsMagma and then implement the following rule.

No further structures to be added that build upon the hierarchy, but have more than one additional property than the structure that is being built upon.

That should at least guarantee that the problem doesn't get any worse?

[JacquesCarette]

I have lots of suggestions, and am working on a prototype implementation (with @alhassy and @WolframKahl ). But all of these ideas are too 'in progress' to be serious short-term proposals.

In the short term, I think the rule you suggest should at least help slow down the worsening of the problem.

As long as you can't do an amalgamated sum, aka pushout, of record definitions, you'll end up with some duplication of effort. And some duplication is pernicious, as you can end up with 'the same' structure but with different names in the records. From an end-user point of view, this is actually what is wanted (as you want to use the common names); it is from a library maintainer's point of view that things get more difficult.

I think one of the really interesting things about this PR is that IsMagma is not empty! Traditionally, that's what mathematicians think. But, of course, they assume that there is a global equivalent relation around, and assume that congruence holds for all new operators. So where classically IsMagma is empty, here it actually has 4 obligations. Even though Magma actually has no equations at all, so that there is no need for it carry around an equivalence relation. So should Magma actually be parametrized over an unused equivalence relation??

[MatthewDaggitt]

I have lots of suggestions, and am working on a prototype implementation (with @alhassy and @WolframKahl ). But all of these ideas are too 'in progress' to be serious short-term proposals.

Okay I'll look forward to hearing about them in the future!

I think one of the really interesting things about this PR is that IsMagma is not empty! Traditionally, that's what mathematicians think. But, of course, they assume that there is a global equivalent relation around, and assume that congruence holds for all new operators. So where classically IsMagma is empty, here it actually has 4 obligations. Even though Magma actually has no equations at all, so that there is no need for it carry around an equivalence relation. So should Magma actually be parametrized over an unused equivalence relation??

I agree, before using Agda I always thought of a magma as empty as well. But if there's no equivalence relationship and no congruence then there's not much point in wrapping a single operator in a record. The definition of some respectful operator over an equivalence relation is definitely a notion that's useful. As an aside, it would be very difficult to omit the equivalence relation as the equality is passed as a module parameter to Algebra.Structures...

[MatthewDaggitt]

Merging in. Will sort out the hierarchy in another PR.