Zulip Chat Archive

Stream: new members

Topic: Two carriers for submodule

Martin C. Martin (Jun 20 2023 at 21:04):

submodule extends add_submonoid, from which it inherits a field called carrier (via add_subsemigroup), and also sub_mul_action, from which it inherits another field, also called carrier. How do we ensure that these two carriers are the same?

Or is there only one? Here we refer to submodule.carrier, which suggests that maybe there's only a single inherited field? If so, how does that work?

Yaël Dillies (Jun 20 2023 at 21:10):

There is indeed only one. The answer so as to why it works the way you intend it to depends whether you use flat or nested structures. submodule is a flat structure so I'm going to explain this one.

Eric Wieser (Jun 20 2023 at 21:14):

Section 2 of arxiv#2306.00617 has some examples demonstrating how multiple inheritance works, both with flat inheritance (mathlib3) and nested inheritance (mathlib4, but presented in lean 3 in that paper)

Yaël Dillies (Jun 20 2023 at 21:15):

submodule extending add_submonoid and sub_mul_action means that Lean takes their fields and makes them fields of submodule, merging fields with the same name, eg carrier. Then it creates the obvious functions submodule.to_add_submonoid : submodule R M → add_submonoid M and submodule.to_sub_mul_action : submodule R M → sub_mul_action R M where the field add_submonoid.x/sub_mul_action.x gets filled in with submodule.x.

Kyle Miller (Jun 20 2023 at 21:15):

"Flat structures" is switched on with set_option old_structure_cmd true (the structure ends up having the union of all the fields of everything it extends, rather than using any of the parent structures themselves as fields). Yaël's explaining this, but I just wanted to point out that this option is important.

Martin C. Martin (Jun 20 2023 at 21:19):

I was afraid it might be named based. So this means, if person A maintains a structure somewhere and decides to change the name of a field, and unknown to them, the new name happens to be the same as person B chose for their unrelated structure, then person C, who extends both of them, now has only one field, not two. However, I suppose the name is part of the external interface of the structure. There's nothing like hidden fields in OO. There are no implementation details. :)

Kyle Miller (Jun 20 2023 at 21:26):

I didn't realize it's name-based in Lean 4 too. This is fine:

structure A where
  x : Nat

structure B where
  x : Nat

structure C extends A, B

If the types don't match it'll throw an error though.

Kyle Miller (Jun 20 2023 at 21:29):

If you want to protect against this, then just like in OO I think you'd embed rather than extend.

structure C where
  toA : A
  toB : B

Martin C. Martin (Jun 21 2023 at 19:44):

Where can I read more about inheritance in Lean 3?

Eric Wieser (Jun 21 2023 at 19:47):

Did you already read section 2 of arxiv#2306.00617 above? I'm not sure there's much else to know: inheritance is just syntactic sugar for either copying across all the fields, or inserting a parent field

Martin C. Martin (Jun 21 2023 at 19:48):

Ok thanks, I'll read that.

Eric Wieser (Jun 21 2023 at 19:48):

If your question is actually "where can I read more about mathematical uses of structure", https://leanprover-community.github.io/mathematics_in_lean/C07_Hierarchies.html#sub-objects is probably a good resource

Eric Wieser (Jun 21 2023 at 19:49):

(but that's for Lean 4)

Last updated: Dec 20 2023 at 11:08 UTC