Classes design and instances

Stream: mathlib4

[Sebastien Gouezel]

I have a bunch of questions on the design of classes in mathlib4, and I hope someone could help me clarify my thoughts.

The implementation of classes is new style, but this is hidden from the user who may think that everything is flattened (i.e., old style). Assume that you have a class with data A_data and then classes that add new Prop properties, say B_prop that extends A_data and then C_prop that extends B_prop and D_prop that extends C_prop. From an API point of view, saying that D_prop is defined as (1) extends A_data, C_prop or (2) extends C_prop or (3) extends C_prop, A_data is the same, but it's not from an inner implementation point of view. If I understand correctly, in (1) there would be a field to_A_data containing the data, and then flattened copies of the additional axioms in B and C, and a field with the addtional D axiom, and the creation of a to_C map (which would not be a field of the structure). While (2) and (3) would be internally the same, with a field to_C and a field with the additional axiom of D (and in (3) the creation of an additional map to_A). Am I correct here? Is there a way to see the internals of the things Lean4 generates when one declares a class like that?

[Sebastien Gouezel]

Then there are diamond-like situations, where there is another class C'_prop extending B_prop, and then D_prop extends both C_prop and C'_prop. Say that one defines it as (1) extends A_data, C_prop, C'_prop or (2) extends C_prop, C'_prop. In the first case, one gets a field to_A and flattened copies of the additional axioms, while in (2) one gets a to_C and flattened copies of the additional axioms of C', again if I get it right.

[Sebastien Gouezel]

No my question is what happens when one creates instances of the classes, and if the order there is relevant. For instance if you create an instance of D having already instances of C and C', will things be nice if you declare it like with already_defined C, already_defined C' and bad if you change the order to with already_declared_C', already_declared_C? (With, in the second case, the map to C borrowing the data field from already_declared_C' and the axiom from already_declared_C)?

[Sebastien Gouezel]

Again, is there a way to check the internals of how Lean 4 has implemented a structure declaration?

[Sebastian Ullrich]

#print on the class will tell you the exact fields

[Sebastien Gouezel]

Would the following design be reasonable? There would be classes carrying only data -- for instance, for semirings, semiring_data would have zero, one, addition, multiplication. And then the real classes need a bunch of properties depending on the data, which could be put into a single Prop-valued substructure. The interest is that when checking that two ring structures coincide, first you need to check that the data coincide, of course, but then by proof irrelevance you would only need to check that the type of the single Prop-valued field is the same, which amounts to checking once again that the data coincide -- just one check, instead of many many checks currently, one for each axiom.

Of course, with this design ring would internally not be defined as extends semiring, but instead ring_data would extend semiring_data, and the map from ring to semiring would not be a field of the structure. (And this would need serious engineering to hide that from the users, and to give the impression that fields of the Prop-substructure are normal fields). The data for comm_ring and ring would be the same, though, so following strings of reductions would be pretty quick.

I wonder if this wouldn't be much more efficient than what we do currently. Not in the near future, of course, because there are much more urgent things, but still I'd be interested in your thoughts.

[Eric Wieser]

I think this is what Agda does

[Eric Wieser]

One advantage of that approach is that if you need an intersection typeclass that doesn't exist, you can use [ring_data R] [is_normed_ring R] [is_linear_ordered_ring R]