[Agda] (Semi)RingWithOne

[Matthew Daggitt]

Hi Sergei,
 Without wishing to get into a citation war, I think there is no clear
consensus that (semi)rings are traditionally defined without a
multiplicative identity. Indeed in every course or textbook I've seen,
they've come with a one defined. Of course that may be a cultural thing.
However given that it's not necessarily clear which way is most common, I
think the standard library will err on the side of sticking with the
current definition. To do otherwise would raise a lot of backwards
compatibility issues with other people's code.

I'm also a bit confused by your statement that the integer numbers does not
have a one. Surely the multiplicative identity of the integers is just "1"?

If there is anything else we can do in the existing framework of the
standard library to help you use the current definitions, do let us know
and we'll consider it for addition.
Best,
Matthew

On Tue, Feb 27, 2018 at 9:11 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear all,
>
> This is a certain minor point about algebra in Standard library.
> I am writing a certain application that relies on  Standard library
> algebra, from Semigroup up to CommutativeRing.
> And I observe the following.
>
> (I) A classical book by Lang (1968) defines that a Ring has an unity
>     element by multiplication.
>
> (II) A classical book by Van Der Waerden (1971) defines that a Ring does
> not necessary has unity. If it has, people call it "Ring with unity".
> I expected that in Standard library it would be called  RinWithOne.
> But I do not find such there.
>
> (III) Standard library defines that Semiring has unity (1#),
>   and Ring inherits Semiring, so that Ring always has an unity element
>   by multiplication. And this agrees with (I).
>   (and naturally, the name RingWithOne is skipped).
>
> (IV) But Standard library also introduces SemiringWithoutOne.
>                                                   -------
>
> (V) Even integer numbers occur a Ring according to (II),
>     but not according to (I).
>
>
> Summing all this, I think that this will be more natural for Standard
> library
> * to define Ring as in (II),
> * to define Semiring with skipping 1#  (instead of SemiringWihoutOne),
> * to define SemiringWithOne as including 1#,
> * to define RingWithOne as inheriting SemiringWithOne.
>
> -- ?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180227/5b04be4c/attachment-0001.html>