Ditching the Pi is one of the syntactic changes we're most looking forward to though...
Conversation
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 ! 🤪🤯
2
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
Indeed. I think human parsing ability should be a concern
1
Note that the above example was generated to optimize evaluation performance by Agda, so it's probably not fair of me to post it. I just thought it was super amusing though! 😊