Conversation
I've seen GLR, but not investigated too deeply! That's what tree-sitter uses, right? tree-sitter.github.io/tree-sitter/
2
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
The grammar above is indeed inherently ambiguous. For example, how would you parse `z (a : b)(c : d) -> e f` ?
2
Yeah, I'm curious what Agda does there. I would expect a language to at least say 'help, add parens here please!'
1
Oh, Agda lacks `:` for type annotation, again getting around this issue. 🤔
I wonder if has a thought. In some ways type annotation in terms being related to proof search? Assuming / hypothesis vs proof cut? Idk.
1
1
Not sure on what exactly you mean but it sounds like bidi typechecking is relevant: there type annotations let you embed checking terms into synthesis terms.
2
Show replies
Oh right, it’s a definable function (I forget if the stdlib defines it): just use user-definable sugar around a polymorphic id function, so that “t as T” means id T t.
1
Right, and the stdlib does define it. agda.github.io/agda-stdlib/Fu