Zulip Chat Archive

Stream: maths

Topic: instance [semiring α] : semiring (with_zero α)


view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:39):

OK so @Amelia Livingston just pointed out to me that in algebra/ring.lean we have the following insanity:

instance [semiring α] : semiring (with_zero α) := ...

semiring extends add_comm_monoid so a semiring already has a zero. Adding another zero is something which is I guess logically possible, but at the same time is surely "always a mistake". Should this instance be removed though?

view this post on Zulip Kenny Lau (Aug 06 2019 at 13:50):

but it really is a semiring...?

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:50):

Yes!

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:50):

If you have an add_semigroup and you add a zero, you get an add_monoid

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:50):

Now apply when the add_semigroup was already an add_monoid

view this post on Zulip Kenny Lau (Aug 06 2019 at 13:58):

it's the (co)unit

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 14:30):

Mathlib still compiles if the instance is deleted. Why would we ever want this instance?

view this post on Zulip Floris van Doorn (Aug 06 2019 at 14:35):

Yes, I think we want to get rid of an instance like that.

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:05):

Why would we want to remove it? It's the same as the situation with monoidifying a semigroup that happens to already be a monoid

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:06):

Because every instance makes life a bit slower, and this instance will never be used so cannot do good and might do harm

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:06):

We could have a more accurate instance there but we would need a class for "semiring without zero"

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:07):

but I disagree with the claim that the instance is "wrong"

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:08):

if you actually have a with_zero and it actually has a semiring structure, I don't see how it could be anything but this one

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:28):

I guess I'm arguing that it's "wrong" in the sense that if something has a zero then it's very hard to imagine a good reason for adding another one. With the semigroup to monoid example the semiring might have a 1 but it might not. Here the semiring is guaranteed to already have a zero, and you are adding another one.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:28):

The fact that the instance is not used in mathlib is evidence that the instance is useless

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:20):

The instance isn't used because no one cares about the theory of semirings

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:21):

But could it be the case that it leads type class inference the wrong way sometimes? If so then it should go

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:22):

The instance isn't used because no one cares about the theory of semirings

I think this is too weak. People care about the theory of rings, and a semiring is a ring, but the instance isn't used anyway. The point is that people don't care about adding 0 to something which already has a 0.

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:22):

I don't disagree with this line of argument though. It shouldn't affect too much, unless you are inferring things on with_zero a lot - most types are not of the form with_zero A so it shouldn't lead typeclass significantly astray

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:23):

It would be difficult and probably inadvisable to define a type operator that only adds a zero if there isn't already one there

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:23):

That is not the case for this instance though!

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:24):

It would be very easy to modify this instance so that it only added a zero if there isn't one already there.

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:24):

it's easier to reason about an operator that always adds exactly one new element

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:24):

By deleting it.

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:25):

The reason this instance exists is because it's completing the cartesian product of all concepts in mathlib interacting with all others

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:25):

We think with_zero A is a useful operator, hence it exists, hence we need all applicable instances because users shouldn't need to define those themselves

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:26):

That would be the case if we were dealing with an object which was an add_comm_semigroup and a monoid, but that's not what a semiring is.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:26):

What could concievably be useful is adding a zero to pnat, but I don't know what kind of an object pnat is. It's not a semiring :-/

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:26):

Actually you need a distrib add_comm_semigroup monoid

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:27):

Like pnat!

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 17:27):

demisemiring?

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:27):

semirig?

view this post on Zulip Mario Carneiro (Aug 06 2019 at 17:27):

you can't spell ring without z


Last updated: May 06 2021 at 19:30 UTC