MIL Ch. 7 Hierarchies: Multiple inheritance

Stream: new members

[Kabelo Moiloa]

I don't understand at all what this sentence from Mathematics in Lean means:

In case of multiple inheritance like for semi-groups, the auto-generated “symmetry-restoring” instances need also
to be marked.

I'm familiar with "multiple inheritance" from object oriented programming (say CLOS), I think what is meant here however Semigroups don't extend anything, did the author's perhaps mean Rings instead of Semigroups?

[Kabelo Moiloa]

@Patrick Massot I saw from the git blame that you added this comment to Mathematics in Lean please do explain further.

[Patrick Massot]

My advice is to forget what you know from object oriented programming and instead read again the beginning of that section. And I definitely meant Semigroup.

[Patrick Massot]

This is really subtle stuff and that chapter is probably the most difficult one, so don’t worry if you need time to digest it.

[Eric Wieser]

To be explicit: what is the "multiple" inheritance for Semigroup (G) extends Mul G?

[Eric Wieser]

I'm also confused by this wording, and would expect Monoid (G) extends MulOneClass G, Semigroup G to be a better example

[Eric Wieser]

(modulo converting those examples to the analogous ones replacing Mul with Dia you use in MIL)

[Kabelo Moiloa]

Eric Wieser said:

I'm also confused by this wording, and would expect Monoid (G) extends MulOneClass G, Semigroup G to be a better example

I admit that I didn't read the section carefully and reading it again with @Patrick Massot's comment in mind got me to learn what was meant by a "symmetry restoring instance," so that the quote at least makes sense to me. I now boldly claim that what was meant was Monoid₁ not Semigroup₁ :nerd: :smile: .

Indeed I'm sufficiently confident in this that I don't mind marking this thread as "done" because my confusions are resolved even if they haven't yet caused an improvement in the wording that I (and perhaps @Eric Wieser as well) think would be helpful. Should I do so? Maybe raise an issue about this on the git repo?