Zulip Chat Archive

Stream: general

Topic: typeclass resolution


view this post on Zulip Bhavik Mehta (Mar 16 2020 at 22:31):

Out of interest, how does typeclass resolution happen in lean? For example, is it acceptable and/or sensible to write both of the following:

instance mono_prod_of_left {X Y Z : C} (f : X  Y) (g : X  Z) [mono f] : mono (limits.prod.lift f g) :=
instance mono_prod_of_right {X Y Z : C} (f : X  Y) (g : X  Z) [mono g] : mono (limits.prod.lift f g) :=

In Haskell for instance, I'd get complained at because of overlapping instances - do we get similar problems in lean?

view this post on Zulip Mario Carneiro (Mar 16 2020 at 22:33):

No, you have a different problem in lean, exponential blowup, because lean tries all the paths if you do this

view this post on Zulip Mario Carneiro (Mar 16 2020 at 22:33):

it is sensible to do, it is like prolog

view this post on Zulip Bhavik Mehta (Mar 16 2020 at 22:35):

Okay great, thanks!

view this post on Zulip Gabriel Ebner (Mar 17 2020 at 09:27):

Mario Carneiro said:

No, you have a different problem in lean, exponential blowup, because lean tries all the paths if you do this

Where does exponential blow-up happen here? Is there some other mono instance I'm missing? With these two instances, Lean will only search mono h for all subterms h, so this should be linear. Following me, Bhavik's instances are perfectly fine (or at least just as bad as every instance we have in mathlib).

view this post on Zulip Mario Carneiro (Mar 17 2020 at 09:44):

ah that's true, I shouldn't have suggested that that instance setup is exponential. I meant in general it can lead to exponential blowup, but with just those instances it is linear.


Last updated: May 10 2021 at 00:31 UTC