Hmm. It's certainly even more consistent with signature syntax, but might need adjustments to our backtracking Pratt parser implementation. Or we give up, parse the LHS as a term, and dissect it in a macro transformer for -> , kind of like in your hack.
Conversation
I think there’s probably a 2-3 pass way you could do it sans backtracking.
1
Yes, the macro expansion would be the second pass. See also Brendan's current hack linked above.
1
In the grammar is it indeed intended that lhs of -> can be an arbitrary term including application?
For example, what is parse of `a b -> c` or of `a (b : c) -> d`?
1
It is in dependent type theory, think `vector (n+1) nat -> nat`. So `a b -> c` = `(a b) -> c`. The second one is indeed unclear (and apparently unprecedented?). The "hack" would assume `(a (b : c)) -> d`, which seems at least defensible, being consistent with the first example.
1
1
Yup that is what I would have thought. Sorry for making you brain explode with this ridiculous grammar ! 🤪🤯
2
Following that reasoning `(a : b)(c : d) -> e` should be parsed as `((a : b)(c : d)) -> e`, i.e. application of a to c
2
1
The ambiguity between ascription and argument annotation can be avoided by a different operator (e.g. :: for ascription), but the problematic ambiguity is between the list of arguments and application. Here is an unambiguous grammar (in SDF3)
1
2
I would say that the distinction between dependent and non-dependent function is semantic. Using an ascription in argument position makes it a dependent function?
1
1
Thus, elaboration could determine that the application arguments in the lhs of a function are individual arguments, either based on syntax (ascr is arg) or based on semantic analysis.
3
2