Confusion about "forgetful inheritance"

Stream: new members

[The-Anh Vu-Le]

I am reading Chapter 7.1 of Mathematics in Lean and I am struggling to understand the solution to the bad diamond presented here.

If I understand correctly, the problem is that

• Z is a Ring, and any ring R forms a Module R R, with ring multiplication as SMul.smul
• Z is an Abelian group, and any Abelian group A forms a Module Z A, with zsmul as SMul.smul

Now, ring multiplication and zsmul may not immediately be the same thing definitionally.

However, the solution is to add things to the additive monoid class (making a new AddMonoid₄). I am confused why this helps. I come from an OOP background so there may have been some special mechanism that I am missing to understand, since if extends is similar to OOP's inheritance, AddMonoid₄ extending AddSemigroup₃ does not change AddSemigroup₃ (is that the case in Lean?).

Many thanks!

[Abraham Solomon]

The-Anh Vu-Le said:

I am reading Chapter 7.1 of Mathematics in Lean and I am struggling to understand the solution to the bad diamond presented here.

If I understand correctly, the problem is that

• Z is a Ring, and any ring R forms a Module R R, with ring multiplication as SMul.smul
• Z is an Abelian group, and any Abelian group A forms a Module Z A, with zsmul as SMul.smul

Now, ring multiplication and zsmul may not immediately be the same thing definitionally.

However, the solution is to add things to the additive monoid class (making a new AddMonoid₄). I am confused why this helps. I come from an OOP background so there may have been some special mechanism that I am missing to understand, since if extends is similar to OOP's inheritance, AddMonoid₄ extending AddSemigroup₃ does not change AddSemigroup₃ (is that the case in Lean?).

Many thanks!

I think from an OOP perspective, it isnt the same, more similar would be instances.

This might help, https://lean-lang.org/doc/reference/latest/The-Lean-Language/Type-Classes/#type-classes

This also discusses it from a more programmatical perspective:

https://lean-lang.org/functional_programming_in_lean/type-classes/polymorphism.html

Edit: I vaguely recall forgetful inheritance being a forgetful functor between monoidal categories, i can't actually find where the macro for extends is defined though.

Also from an OOP perspective the following passage from 7. Inductive Types in Theorem Proving with Lean may be helpful:

"In fact, in Lean's library, every concrete type other than the universes and every type constructor other than dependent arrows is an instance of a general family of type constructions known as inductive types."

https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html

[Abraham Solomon]

(deleted)

[The-Anh Vu-Le]

Then, how does AddMonoid₄ help? I have gone through the text many times but cannot understand.

[Abraham Solomon]

The-Anh Vu-Le said:

Then, how does AddMonoid₄ help? I have gone through the text many times but cannot understand.

I was just trying to provide parallels to OOP -- to answer your question unfortunately would require someone who has gone through all of MIL ( I mostly use FPIL and TPIL).

One thing to note about that passage, is it appears they explain it in some detail in a paragraph further up:
"
But the diamond we created with modules is definitely bad. The offending piece is the smul field which is data, not a proof, and we have two constructions that are not definitionally equal. The robust way of fixing this issue is to make sure that going from a rich structure to a poor structure is always done by forgetting data, not by defining data. This well-known pattern as been named “forgetful inheritance” and extensively discussed in https://inria.hal.science/hal-02463336.
"
So to answer why it helps, is not trivial.

This might be helpful, using an analogical example with a different versions of addition on Nat.

https://lean-lang.org/functional_programming_in_lean/dependent-types/pitfalls.html

Otherwise, youd have to be a bit more narrow with your question.

Edit: Note by diamond they refer to the "diamond problem"
https://en.wikipedia.org/wiki/Multiple_inheritance
so your question is really how forgetful inheritance helps with the diamond problem. Might be a complicated answer.

[The-Anh Vu-Le]

Thank you for all the pointers. After some thinking, my question should be: After implementing the solution (forgetful inheritance) with classes/instances related to AddMonoid₄, how will Lean synthesize a Module ℤ ℤ instance? (before the solution, it picks abGrpModule ℤ arbitrarily)

[Kevin Buzzard]

Do you know about the difference between syntactic, definitional and propositional equality? What we do _not_ want to happen in mathlib is that typeclass inference makes random selections depending on exactly how various questions were asked, and you end up with rw [h] failing when h : 1 • a = a and the goal has 1 • a in, but the rewrite fails with an obscure error message because it turned out that the two 1 • as are equal, but the proof isn't rfl. The issue is that rw works up to syntactic equality. What the chapter is explaining is that if you ensure that all routes that the typeclass inference system finds back to smul give exactly the same answer (not just answers that we can prove are the same, but answers which are exactly the same) then this problem does not arise. So the answer to the last question you asked is "it doesn't matter, because all attempts to do this give equal answers, for a very strong notion of equality".

[The-Anh Vu-Le]

Thanks! I understand that. What I don't seem to get is how adding AddMonoid_4 would help since why would having an additional class having any effect on the existing things?

[Kevin Buzzard]

I agree that this is explained in a bit of a confusing manner. I think the precise answer to your question is "it doesn't". But the text says "This story then continues with incorporating a zsmul field into the definition of groups and similar tricks." and once this field is also there, you can override the Z-action on Z.

[The-Anh Vu-Le]

Correct me if I'm wrong, this means that the provided "solution" is not yet complete. What one should do is to

• add the zsmul field to AddMonoid₄ (defined based on the field nsmul also in there),
• • create an AddCommGroup₄ class (requiring creating AddGroup₄ class and AddCommMonoid₄ class based on this AddMonoid₄), and
• define a new abGrpModule instance of Module₁ ℤ A based on this new AddCommGroup₄?
  Edit: maybe at the last step, you need to modify Module₁ class itself to rely on AddCommGroup₄