I admit I got a bit confused about how parsing would get confused on the pi vs type annotation bit. It’s mostly about grammar power right ?
Conversation
Replying to
Correct. GLL or something could be able to resolve it, or a ton of backtracking, if using PEG.
Quote Tweet
Replying to @Iceland_jack
Nah, the issue is this combo of syntax:
- (a)
- a : A
- A -> B
- (a : A) -> B
Mentally humans prioritise the dependent function, but it’s rather hard to get a parser to do that. A different symbol could help though.
Replying to
What’s the tiniest example program that has this ambiguity and uses both flavors ?
1
literally just `(a : A) -> A`
1
Show replies