class hierarchy

Stream: general

[Yury G. Kudryashov]

I've realized that I don't understand why creating M*N classes (e.g., ordered_semiring etc) is better for typeclass search than mixins. If we have M * N typeclasses, then there are very exponentially many paths from, e.g., ordered_add_monoid to linear_ordered_field, and Lean has to check every path. Am I correct?
BTW, should we ask Daniel Selsam (not tagging him for now) what will work better in Lean 4?

[Eric Wieser]

Is it motivated by saving characters? [semiring S] [ordered_semiring S] [left_cancel_semiring S] is longer to type than [ordered_left_cancel_semiring S], even though that's not a good argument.

[Yury G. Kudryashov]

I don't think that saving characters is a good goal. If we'll find out (this is a big IF) that mixins work better than M * N * K classes, then we can come up with a syntax telling Lean to introduce [left_cancel_semiring S] and all typeclasses on S needed as arguments to left_cancel_semiring. E.g., something like [!left_cancel_semiring S].

[Eric Wieser]

I've seen that suggestion before as [[left_cancel_semiring S]], and agree that it would be a solution to the typing problem

[Yury G. Kudryashov]

I think that main issues we should discuss are (a) elaboration speed; (b) maintainability.

[Floris van Doorn]

@Gabriel Ebner (I think) has optimized the type class search algorithm so that it caches failures during the search. So it doesn't have to search all exponentially paths, but it still has to go through all M * N classes.

[Yury G. Kudryashov]

How does it know that different paths lead to the same value?

[Floris van Doorn]

With the order-algebra interface, I'm also wondering whether it's better to separate out the order class, e.g. [linear_order G] [ordered_group G]. I'm not sure if there is much gained by also separating out [group G], since the fields ordered_* class will greatly depend on *.

[Floris van Doorn]

I think the algorithm assumes that diamonds lead to definitionally equal instances.

[Floris van Doorn]

In many cases it doesn't matter: if it couldn't find comm_ring S when coming from ring S then it also cannot find comm_ring S when coming from comm_semigroup S.