Do you have a pointer to the grammar ? Would be interesting as a case for priorities in SDF3
Conversation
This is the grammar that they tend to use:
term ::= var
| term term
| "(" term ")"
| term ":" term
| term "->" term
| ( "(" var+ ":" term ")" )+ "->" term
Coming up with good precendences is left as an exercise 😊
1
3
I have an issue for it here: github.com/pikelet-lang/p
1
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`?
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. 😊
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
Show replies