I've seen GLR, but not investigated too deeply! That's what tree-sitter uses, right? tree-sitter.github.io/tree-sitter/
Conversation
I was starting on a hand-rolled parser because over the LR parser generator I was using because `(x : A) -> B` is ambiguous. It could either be parsed as:
- a dependent function type
- a non-dependent function with the input type annotated
I want to prioritise the former.
3
1
1
Do you have a pointer to the grammar ? Would be interesting as a case for priorities in SDF3
1
1
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`?
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
Show replies