Zulip Chat Archive

Stream: new members

Topic: Adding new instances


view this post on Zulip Riccardo Brasca (Dec 16 2020 at 15:39):

What is the general attitude for adding new instances? Should we add as much instances as possible or it is better to keep their number not too high (for performance reasons for example). I see that there is no algebra R I.quotient, where I is an ideal of R. Should I add it?

view this post on Zulip Mario Carneiro (Dec 16 2020 at 15:42):

The rules for adding instances are more complicated than that. It comes down to how the instance affects the overall search problem. Loops are bad, more instances are bad but only very slightly; instances are organized according to their type class (in this case algebra), so it depends on whether there are already many instances in this class and also how many search problems for other things go via this class (I would think not many, because algebra already has two input arguments).

view this post on Zulip Mario Carneiro (Dec 16 2020 at 15:43):

The other major thing is whether there will be any competition for the things that this instance will satisfy, because non-defeq diamonds in the typeclass system are also bad

view this post on Zulip Eric Wieser (Dec 16 2020 at 15:44):

This sounds like a more powerful version of docs#mul_action.quotient, right?

view this post on Zulip Riccardo Brasca (Dec 16 2020 at 15:48):

Yes. It is very easy ,ring_hom.to_algebra (ideal.quotient.mk I) is enough. To me it seems very natural to have it, but I can write it down explicitly in my theorems of course.

view this post on Zulip Eric Wieser (Dec 16 2020 at 15:56):

smul is defined as a * xunder the quotient, right?

view this post on Zulip Riccardo Brasca (Dec 16 2020 at 16:01):

Yes, it is (ideal.quotient.mk a) * x.

view this post on Zulip Riccardo Brasca (Dec 16 2020 at 16:03):

There is absolutely nothing deep or interesting in this particular case, I was just wondering how to deal with missing instances that from a mathematical point of view are obvious.

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:07):

I only ask because I was worried that it might not be defeq to the mul_action instance

view this post on Zulip Riccardo Brasca (Dec 16 2020 at 16:08):

Ah, I see that there are subtle problems sometimes...

view this post on Zulip Eric Wieser (Dec 16 2020 at 16:21):

Although actually that's not relevant here, ideals are not quotient_groups.

Your instance sounds like a good ide ato me


Last updated: May 10 2021 at 18:22 UTC