instance graphs

Stream: mathlib4

[Floris van Doorn]

As preparation for writing instance priority linters, I wrote some code to generate the current algebraic hierarchy as a graph.
Here is the full "algebraic hierarchy" of mathlib:

FullInstanceGraph.pdf

What are you looking at here?

• All nodes are classes with 1 explicit type argument (and potentially other type-class arguments). So not e.g. Module
• Solid edges are "forgetful" instances from a class to another class (either generated by the extends syntax or by a user). Instances that have multiple source classes are not displayed.
• Dashed edges are classes that have another class as argument (e.g. there is a dashed edge T0Space -> TopologicalSpace)
• Edges in the transitive closure are removed (e.g. there is no direct edge from T1Space -> TopologicalSpace)
• Classes without any edges are not displayed

If this is too overwhelming, here is a subgraph where we only take the classes with 1 argument (no other type-class arguments). That one is almost manageable!

PartialInstanceGraph.pdf

Code and output (in dot format) here: (this also contains all the instances with multiple sources, that are not as easily visualizable in a graph)

https://gist.github.com/fpvandoorn/c398ea0a926a8b4013344d4a45bf9bbb

You can use tred full.dot | dot -y -T pdf > full.pdf to generate the graphs (requires graphviz)

[Martin Dvořák]

Thanks a lot!

I just printed the smaller graph on A3. It is barely readable. I will try A2 if I get a chance.