SO structure question

Stream: general

[Kevin Buzzard]

I always forget about the difference between extending and not extending when defining structures, so I asked a question on stackoverflow because search will then work better for me in the future: https://stackoverflow.com/questions/60130605/extending-or-inferring-pid-ufd-in-a-lean-class-definition

[Floris van Doorn]

My guess is that the definition unique_factorization_domain is sub-optimal: it's generally better to extend the structure.
Unique factorization domains were defined in 2018 by @Johannes Hölzl, so my guess is that back then we knew less well what the best way was to set up classes.

There is a small downside in using extends: it will increase the type-class search for unrelated type-class problems, because there is now an instance unique_factorization_domain -> integral_domain.

[Chris Hughes]

Why is it better to extend the class?

UFD is a rarely used class, so does that make the downside more significant relative to the upside?

[Floris van Doorn]

Why is it better to extend the class?

I think we've noticed almost all type-class instance bottlenecks with modules/algebras/vector spaces where we have classes with other classes as arguments. Of course, those hierarchies are much larger, but I think part of the problem is the instances that are arguments to classes (which, in those cases are necessary).
There is a performance problems with a instance instance [integral_domain \a] [unique_factorization_domain \a] : .... If there are multiple instance paths to integral_domain \a and none to unique_factorization_domain \a then type-class inference will go through all possibilities of the integral_domain \a search.

UFD is a rarely used class, so does that make the downside more significant relative to the upside?

Perhaps that is a good enough reason, as a workaround until we have the type-class inference of Lean 4.