On Mon, Nov 11, 2019 at 4:46 PM Benoit <[email protected]> wrote:
> 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.
>>
>
> 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.
>
I think the definition doesn't quite do the word justice. It can also mean
"critical" (as in critique) in addition to more hurtful senses, depending
on context. I use the word in the sense of a quick comment that makes a
critical point but doesn't elaborate.
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?
>
Yes, parentheses are specifically recognized by the parser and allows you
to nest any low precedence expression inside a high precedence environment.
The relevant production from the grammar is
expr(max) <- "(" expr(0) ")"
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.
>
I mean putting a coercion later in the file. It could be forbidden, but
then this entails making precise the rules that dictate the acceptability
of the added coercion (and an efficient decision procedure for the
criterion). There is already a similar kind of restriction on coercions:
the coercion graph is required to have no diamonds (more than one path
between any two fixed vertices), and this is checked using a dynamic
version of the Floyd-Warshall algorithm.
> The MM0 parser specification is not deterministic
>>
>
> Would it be possible (and worth it in terms of pros and cons) to make it
> deterministic ?
>
Perhaps this is the wrong way to say it. The parser itself is
deterministic, because the CFG is unambiguous. There is only one parse
according to the CFG, so any valid parse algorithm will get the same result.
You can still have determinism with an ambiguous grammar by simply having a
parsing algorithm that picks something from the grammar, and using that
algorithm as the definition of the parser. But in this case, the CFG
becomes superfluous, as it isn't actually defining the language correctly -
it specifies that certain parses are valid that really aren't. I would much
prefer for the CFG to be authoritative and unambiguous, so that the parsing
algorithm is not a part of the specification.
> 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.
>
Actually, type theories will look at the type system of MM0 and say that it
is too weak. Almost any self-respecting type theory has an infinite number
of types, for example N and N->N and (N->N)->N and ((N->N)->N)->N and so
on. MM0 has a finite number of types, and they all have to be declared in
advance, which is why (try to) I call them "sorts" instead because "types"
suggests a flexibility that MM0 sorts don't have.
This means that you can't use sorts in place of types in a type theory, so
you have to model them inside the logic. This is deliberate, because using
sorts as types in my experience only leads to sadness, because this ties
the complexity of the type system to the complexity of the foundations, and
it's never good enough. HOL uses a type theory that gives you type
constructors and function types but no binders, and people said "hey look
we can make lots of interesting mathematical sets in here" and used the
type system for *sets* in the math sense. But then they become unhappy when
they realize that math sets need more than this; categories and schemes are
higher order objects, and you have things like Z/pZ where a type depends on
a term; suddenly simple type theory is too simple, so the foundation must
grow to dependent type theory. But then you get a big convertibility
judgment for deciding if a term of type Z/4Z is also of type Z/(2+2)Z, and
you want type checking to be decidable but also really powerful, efficiency
goes way down, and it generally becomes a logical mess. And the
mathematicians are still not happy because the system doesn't let certain
true things be type correct.
I want to sidestep this whole thing by making the type system so
impoverished that anything at all nontrivial must go inside the logic. Once
that becomes the standard idiom, the tooling evolves to represent it, and
you still get the nice type system in the end, but it's not tied to
complexity of the foundations any more; you can extend the type system at
will by changing the tactics and leaving MM0 untouched.
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 "~".
>
I agree.
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).
>
If this is your position, then it comes too close to "inference" for my
taste. MM0 used to do more type inference with the "var" keyword, but I
don't think that excessive type inference is good for readability. Instead,
all that inference has been shuffled off to MM1, and MM0 requires
everything be declared in advance, so that it can give errors in the right
places. It's not required that an operator of type A x B -> B be right
associative; if there is a coercion A -> B then arbitrary grouping is
possible. I can imagine MM1 or similar making guesses about this and
populating the fields as necessary, but MM0 is all about saying what you
mean up front. No one reads specs anyway, but the best way to make a
language feel simple and obvious is for it to actually be simple.
Mario
--
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/CAFXXJSvEoQmR6hESD-Z4i9DOajLv3cuF9hAu9cOG8%3D-4SypBgw%40mail.gmail.com.
