Who has the most ancestors? A top ten list

Stream: mathlib4

[Kyle Miller]

Each of the numbers in the first column is the total number of ancestors of the structure in the second column plus one:

69 RCLike
68 ConditionallyCompleteLinearOrderedField
63 NormedLinearOrderedField
60 CanonicallyLinearOrderedSemifield
60 CommCStarAlgebra
58 CStarAlgebra
58 LinearOrderedField
55 LinearOrderedSemifield
51 DenselyNormedField
51 NontriviallyNormedField

[Kyle Miller]

Here's the histogram of these numbers for all of mathlib:

[0, 2963, 349, 138, 86, 49, 25, 31, 19, 10, 13, 9, 6, 10, 11, 4, 6, 7, 8, 2, 5, 2, 5, 6, 0, 2, 5, 2, 3, 3, 1, 1, 3, 2, 2, 0, 1, 3, 4, 5, 2, 0, 1, 0, 2, 5, 0, 0, 0, 1, 1, 2, 0, 0, 0, 1, 0, 0, 2, 0, 2, 0, 0, 1, 0, 0, 0, 0, 1, 1]

[Sébastien Gouëzel]

I don't understand how RCLike can have so many ancestors. Shouldn't it just have two, the reals and the complexes?

Or by ancestors do you mean the number of fields, and subfields of fields, and so on?

[Kyle Miller]

A "parent" is a structure that appears in the extends clause, and an "ancestor" is the transitive closure

[Kyle Miller]

docs#RCLike has four parents

[Edward van de Meent]

out of curiosity, does something like docs#RingEquiv have 2 or 3 ancestors parents? because it uses extends with 3, but in a sense one of those is also a proper ancestor, and therefore not something you're interested in?

[Edward van de Meent]

for those who don't want to look it up, structure RingEquiv A B .... extends Equiv A B, AddEquiv A B, MulEquiv A B

[Kyle Miller]

I'm not sure I understand the question, RingEquiv has three direct parents (yes, one is implied by the other two), but you need to walk the whole graph of parents to find the set of ancestors.

[Kyle Miller]

Here's the list: #[`RingEquiv, `Equiv, `MulEquiv, `AddEquiv, `MulHom, `AddHom]

[Edward van de Meent]

i guess it's not relevant to the number of ancestors, i was just wondering if this is something that is relevant to whatever you're interested in analysing...

[Edward van de Meent]

i just noticed i meant to write parent where i wrote ancestor in my question...

[Kyle Miller]

Yeah, that was my confusion about your question. I even looked at a dutch<->english dictionary to see if that explained it :-)

[Edward van de Meent]

sorry about that :upside_down:

[Matthew Ballard]

If you collapseProp-valued fields/structures, what does that look like?

[Kyle Miller]

But no, that's not something I'm analyzing currently @Edward van de Meent, I was just trying to estimate a performance impact of a new algorithm. Though it's interesting that the parents are out of order. I don't see why we want Equiv to come first.

[Edward van de Meent]

i seem to recall it is in order to make it symmetric in some way?

[Kyle Miller]

Does anything go wrong having structure RingEquiv A B .... extends MulEquiv A B, AddEquiv A B instead?

[Kyle Miller]

I was hoping that we would make all extends lists eventually satisfy a locally consistent ordering condition, and this goes directly against it.

[Kyle Miller]

@Matthew Ballard Can I interpret "collapse" as "throw out from the ancestor lists"?

[Matthew Ballard]

If A extends B by only prop fields, then identify them

[Kyle Miller]

Ah, interesting. That's doable of course, but it'll take a bit of coding.

[Matthew Ballard]

Or impose a penalty for each data carrying field.

[Matthew Ballard]

If I want to unify two structure instances by expanding them along a constructor, then the more data carrying fields I expose the worse the score is.

[Eric Wieser]

Perhaps what @Edward van de Meent was getting at, but there are some classes which are morally parents of one another (there is a Foo.toBar instance that constructs no new data), but for whatever reason this is not registered with Foo _ extends Bar _