Hi Freek,
I do not know what exactly you oppose, since I do not know what exactly I propose ;-)Well, you propose changing how "notations" select the meaning of a give notation, and I do not think that that is one of the aspects of Mizar that really needs to be changed at the moment. I don't see the problem with it.
The original problem was simplified import of other articles. Your suggestion now seems to be to solve that by
(1) writing (or re-ordering, or just interpreting) the notation directives always in the linear MML order.
Maybe what you actually want to have for the simplified import is stronger:
(2) whenever you merge two (say MML-ordered) series of notation directives, the resolving of the overloading will not change the semantics of any of the merged articles.
I think that (1) might definitely lead to a better organization of MML.What I was trying to show with the "result type of intersection" example is that there is no good linear preference between some overloading variants. So unless overloading in MML is really very simplified (e.g. to the point that there is no overloading at all), (2) can be fairly difficult to do.
That's why I started from the other end, and rather asked what are the overloading mechanisms that people naturally expect, and that are "reasonably stable" under (1) and (2). That's in my opinion parametric polymorphism. And perhaps the possibility to explicitly prioritize in the body of the article.
Yes, as said before, you can emulate a lot of it by "MML policy" (e.g., writing programs that look for the optimal MML order). But that's in my opinion something like fitting parameters of a black-box neural network to perform a simply expressable algorithm.
Josef