Stream: Lean Together 2021
Topic: On Flattening
Jacques Carette (Jan 06 2021 at 17:20):
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 (Jan 06 2021 at 17:26):
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 (Jan 06 2021 at 17:52):
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 (Jan 06 2021 at 18:53):
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
group instances are, but crucially both
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 (Jan 06 2021 at 19:21):
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 (Jan 06 2021 at 20:29):
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 (Jan 06 2021 at 21:05):
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 (Jan 07 2021 at 06:42):
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
B, the user has to specify which version they want to call with
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 (Jan 07 2021 at 06:44):
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 (Jan 07 2021 at 07:47):
Meanwhile, lean3 doesn't inherit "methods" (projections) at all. Has this changed in lean4?
Last updated: May 08 2021 at 21:09 UTC