I have an issue for it here: github.com/pikelet-lang/p
Conversation
Quote Tweet
Replying to @brendanzab
seems like the real issue is overloading of parens!
1
Looks like an inherent ambiguity that is not solvable by priorities, since those select between a re-ordering of the tree using the same productions. Will do an experiment with SDF3
2
2
Yeah, intuitively I'd expect the dependent type to have priority over the type annotation, but I can't see how that could be gleaned from the grammar alone.
1
Change the synxtax, save the world
2
1
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
I do think that some of this is super easy to solve depending on which parser tech you use.
1
I mean, I could just live with backtracking. 😊