On Flattening

Stream: Lean Together 2021

[Jacques Carette]

I heard some discussions on flattening or not, and I figured I would expand on my position.

First and foremost: I view the question as a false choice. One should not ask whether to flatten or not, as if making this choice is something one is forced to do.

It should be obvious that there are many different classes of 'users' of a math library, from its own developers to very new users. Different classes of users will be best served with different views of the same information contained in the library. A certain class of developers (call them the 'architects') really will want to see a graph-oriented version of theories. These are the people who are most concerned with scalability and compositionality. But when teaching certain things, that is awful, and one wants a fully flat theory. There are also needs for intermediate views: R-modules are one of the best-known situation where a mixture is a good idea. I've personally encountered such situations in category theory itself.

To me, the most important feature is being able to easily have different views of the same information, and easily be able to switch between these views.

[Kevin Buzzard]

In Leo's talk he pointed out that mathematicians make structures with many many fields and he was concerned about potential slow-down if it's internally stored as a flat structure.

[Jacques Carette]

Right! That is why I am quite careful to talk about views. System developers (like @Leonardo de Moura ) should be given the freedom to store things internally as they see fit, as long as the users have ways of seeing the structures in a way that fits their mode of working.

To me, a library like mathlib is a repository of knowledge. One error is to think that the source for that library should match everyone's view of how that information should be created. Another error is to think that the internal representation of the system will match that as well.

This is an extremely difficult problem. The more you actually leverage the structural information of mathematics in encoding mathematics, the harder you make it to get new people on board. But if you don't leverage such information, then you're basically forcing yourself to use a lot (a lot) of human effort to develop everything. Of course, it is also highly parallellizable.

The meta-programming facilities in Lean 4 are extremely exciting to me, as they seem to give one the ability to do some of this in a structured, disciplined way.

[Eric Wieser]

I wonder if we can learn from C++'s multiple inheritance and virtual base classes here? The parallel would be that comm_group holds internal references to where the comm_monoid and group instances are, but crucially both comm_monoid and group contain a reference to the same monoid data. So the data isn't flattened, but it also doesn't force us to pick one base structure to be special

[Jacques Carette]

Better still, one can learn from Category Theory first - these things are pushouts (or pullbacks, if you're like me and prefer to work in the opposite category). In some cases, you even have cartesian lifts. All this extra structure helps you store things more effectively too.

C++'s mechanisms for this are hopelessly broken. I would mostly learn what not to do from it.

[Eric Wieser]

What type of hopeless breakage would I expect to see if I implemented the above class heirarchy in C++ multiple virtual inheritance then?

[Jacques Carette]

I forget the exact details, sorry! The weirdnesses of C++ multiple inheritance are well documented "out there". Other languages handle things better. Scala is one. And various languages in the OBJ3 family too, including CASL.

[Simon Hudon]

One important issue with the way C++ implements multiple inheritance is that the user of the classes concerned have to pay attention to details that should be hidden from them. For instance, if class C inherits methods foo from both A and B, the user has to specify which version they want to call with x->A::foo() or x->B::foo(). That should be handled by the designer of the API. Some programming techniques exist to circumvent the situation but the point is that the C++ design of inheritance gets in the way

[Simon Hudon]

As far as examples to consider, I particularly like the way Eiffel does things. When inheriting two methods with the same name, Eiffel forces you to resolve the ambiguity and rename one or both (if they cannot be merged)

[Eric Wieser]

Meanwhile, lean3 doesn't inherit "methods" (projections) at all. Has this changed in lean4?