Zulip Chat Archive

Stream: general

Topic: class hierarchy


Yury G. Kudryashov (Oct 27 2020 at 16:34):

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 (Oct 27 2020 at 16:44):

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 (Oct 27 2020 at 17:04):

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 (Oct 27 2020 at 17:19):

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 (Oct 27 2020 at 17:49):

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

Floris van Doorn (Oct 27 2020 at 17:52):

@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 (Oct 27 2020 at 17:54):

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

Floris van Doorn (Oct 27 2020 at 17:54):

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 (Oct 27 2020 at 17:54):

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

Floris van Doorn (Oct 27 2020 at 17:56):

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.


Last updated: Dec 20 2023 at 11:08 UTC