Zulip Chat Archive

Stream: general

Topic: diamond problem

Sean Leather (Sep 06 2018 at 09:05):

I'm not sure if this is an instance of the type class diamond problem, but what do you do when you have has_add from add_comm_monoid and need has_add from distrib, given that you have [add_comm_monoid α] [distrib α]? One solution seems to be to use [semiring α] instead, but that seems to me to add unnecessary constraints, since semiring also extends monoid and mul_zero_class. I'm guessing there is another, better way.

Reid Barton (Sep 06 2018 at 09:16):

I think you should avoid being in that situation in the first place.
But I don't understand why there isn't a problem with semiring itself.
Maybe old_structure_cmd magic?

Reid Barton (Sep 06 2018 at 09:19):

Maybe you could make your own "old structure" containing just what you need?

Sean Leather (Sep 06 2018 at 09:20):

Sorry, Reid, I haven't used old_structure_cmd and don't know what you mean.

Last updated: Aug 03 2023 at 10:10 UTC