Stream: new members
Topic: Adding new instances
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?
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).
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
Eric Wieser (Dec 16 2020 at 15:44):
This sounds like a more powerful version of docs#mul_action.quotient, right?
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.
Eric Wieser (Dec 16 2020 at 15:56):
smul is defined as
a * xunder the quotient, right?
Riccardo Brasca (Dec 16 2020 at 16:01):
Yes, it is
(ideal.quotient.mk a) * x.
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.
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
Riccardo Brasca (Dec 16 2020 at 16:08):
Ah, I see that there are subtle problems sometimes...
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