instance [semiring α] : semiring (with_zero α)

Stream: maths

[Kevin Buzzard]

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?

[Kenny Lau]

but it really is a semiring...?

[Kevin Buzzard]

Yes!

[Kevin Buzzard]

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

[Kevin Buzzard]

Now apply when the add_semigroup was already an add_monoid

[Kenny Lau]

it's the (co)unit

[Kevin Buzzard]

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

[Floris van Doorn]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

That is not the case for this instance though!

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

By deleting it.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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 :-/

[Mario Carneiro]

Actually you need a distrib add_comm_semigroup monoid

[Kevin Buzzard]

Like pnat!

[Kevin Buzzard]

demisemiring?

[Mario Carneiro]

semirig?

[Mario Carneiro]

you can't spell ring without z