Change the synxtax, save the world
Conversation
Ditching the Pi is one of the syntactic changes we're most looking forward to though...
1
Oooh, what are you changing to? `(a : A) -> B a`?
1
That's the plan. Makes it so much more comfortable moving dependent parameters before/after the colon in a signature
1
1
I agree - there's much to like about this notation. Thoughts on Agda's more radical: `(a : A) (b : B a) -> C a b`?
2
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.
1
1
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 ! 🤪🤯
Note that some crazy cases actually pop up in real code. I was most amazed by this, which even pushes the human’s parsing ability:
Quote Tweet
Replying to @andrasKovacs6 and @JonSterling
hahaha this is just so... amaze
1
Indeed. I think human parsing ability should be a concern
1
Show replies
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
Show replies