Thanks for the clear explanations. I didn't know this use of the word "barb", and I see on dictionary.com "unpleasant remark". My remarks were certainly not meant to be unpleasant, and I'm interested in seeing where MM0 goes.
Is it always possible to put parentheses, even where they are not needed? I mean: is there a rule saying that if A is an expression of some type, then ( A ) is also an expression of the same type, so that I can write e.g. "( a * b ) + c" even when "a * b + c" is valid? A few comments as replies below. It may seem strange that you have to redundantly specify this information, > but it's not really redundant. How can MM0 know that scalar is not a > subtype of vector? It may not be right now, but perhaps later you decide to > add a coercion and then it becomes ambiguous. > Do you mean: changing one's mind at a later time, or putting a coercion later in the file? The latter could be forbidden, maybe. > The MM0 parser specification is not deterministic > Would it be possible (and worth it in terms of pros and cons) to make it deterministic ? > Finally, I want to point out that your example is slightly unrealistic. > The MM0 type system is (somewhat deliberately) impoverished, and it would > be very unlikely for you to actually have types "scalar" and "vector" > unless you are in a (very limited) kind of first order proof environment > for modules. You wouldn't be able to do much interesting vector space > theory there, because you have no higher order constructs. Much more > likely, you are working in a ZFC style foundation where everything has the > same type "set", and then type information is next to useless for this kind > of thing. > Indeed, and that's a good point, and this was for the sake of the example. There might be other applications of MM0 not based on set theory, towards type theories, where there could be real-life examples like this. > I will add that I fell into this (cognitive) trap myself, and Giovanni > caught me on it. I said to myself "It doesn't make any sense for "e." to be > right or left associative, because it has type set x set -> wff, so it > can't associate with itself anyway, so I'll just make it left assoc". But > this is not true, because "~" lives at the same precedence, and if "e." is > left assoc then there is a conflict, while if "e." was right assoc then > there would be no conflict. Because *types don't matter during parsing* (at > least, with the MM0 parser algorithm as it currently exists). I've written > a simple C compiler before, and the "A * b;" example of type-disambiguation > between a multiplication statement and a pointer declaration is a real > thing (and a real pain). I don't want to replicate that. > That's a clear explanation. But in the present case, I would say that a solution which is better for human comprehension is to give lower precedence to "~". The suffix and mixfix ideas sound promising, and they would have real-life applications indeed. > I suppose that's true, but it's not obvious. MM0 is designed to be read, > and having mystery rules like that seems like a good way to scare people > off. The precedence system is supposed to be minimal and expressive, but > not surprising, and I can already see the angry github issues asking why > changing a precedence from 42 to 43 with nothing else nearby breaks their > code. > Agreed: this was more of a theoretical remark ! > Regarding the barb about neglecting mathematical practice, I still don't > see your argument. Your example with modules fits perfectly well within the > MM0 precedence system. Yes you have to write those precedences down, and if > you get it wrong then things don't typecheck, but that doesn't mean that > "." isn't right associative in the example. It's *obviously* right > associative because the other option doesn't typecheck, but you seem to be > taking from this fact that it's not associative at all, which isn't true; a > non-associative operator (which MM0 doesn't support) would *always* require > parentheses. > No: I'm taking from this fact that I should not have to specify its associativity since it is obviously right-associative. But I agree that this puts too much work on the parser (if it's even possible, as you said). Benoît -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4a6120d2-8371-4b38-9a49-9c446a80d612%40googlegroups.com.
