Private class/structure members

Stream: lean4

[Andy Soffer]

Lean has a really useful property where members with the same name are "coalesced" when inheriting as a mechanism to resolve the diamond-inheritance problem. One negative side-effect of this is that the coalescing happens by default, even if I don't want it to. I can of course give complex names to fields in the hopes that no one else uses that name, but I'm wondering if there is another mechanism to ensure that names aren't merged.

One could imagine, for example, having Monoid and Group classes each with an op field, and wanting them to be coalesced in some cases, but not for Ring where the Monoid is for multiplication and the group is the additive group.

[A.]

I think if you avoid extends then it doesn't happen? But I'm not sure and I seem to recall that I've been surprised before.

namespace pig1

class Monoid (α : Type) where op : α → α → α
class Group (α : Type) where op : α → α → α

class Ring (α : Type) extends Monoid α, Group α

example {α : Type} [Ring α] : (Ring.toMonoid.op : α → α → α) = Ring.toGroup.op :=
  rfl -- succeeds

end pig1

namespace pig2

class Monoid (α : Type) where op : α → α → α
class Group (α : Type) where op : α → α → α

class Ring (α : Type) where -- much like the above but done by hand
  toMonoid : Monoid α
  toGroup : Group α

example {α : Type} [Ring α] : (Ring.toMonoid.op : α → α → α) = Ring.toGroup.op :=
  rfl -- fails

end pig2

[Andy Soffer]

This is a reasonable workaround, but comes with a tradeoff I don't really like, which is that I don't get the field merging when I want it. Without it as I build up each class I need to effectively determine all the fields I would want transitively and place them in each class, since I'm not getting them via inheritance.

I guess I was hoping for something like being able to annotate fields as private so they'd be accessible explicitly via myRing.toGroup.op but have the others merged.

[Kim Morrison]

Nothing like this exists at present.

[Kyle Miller]

One could imagine, for example, having Monoid and Group classes each with an op field, and wanting them to be coalesced in some cases, but not for Ring where the Monoid is for multiplication and the group is the additive group.

The way this is done in practice (in mathlib) is to have AddGroup, which has its own add field and + notation, and Monoid, which has its own mul field and * notation.

Do you have other concrete use cases for this?

[A.]

I remember now that what surprised me was the merging of fields that hadn't been introduced through the extends mechanism. I wonder would anything be lost if merging were restricted to such fields only? So that pig1 would no longer work but this pig3 still would.

namespace pig3

class Op (α : Type) where op : α → α → α

class Monoid (α : Type) extends Op α
class Group (α : Type) extends Op α

class Ring (α : Type) extends Monoid α, Group α

example {α : Type} [Ring α] : (Ring.toMonoid.toOp : Op α) = Ring.toGroup.toOp :=
  rfl

end pig3

[Andy Soffer]

No other use cases (all flavors of this problem). There are definitely solutions in practice... I'm really just playing around and trying things out.

Thanks for the help!