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
Correct. GLL or something could be able to resolve it, or a ton of backtracking, if using PEG.
2
What’s the tiniest example program that has this ambiguity and uses both flavors ?
1
Wait, I'm not sure backtracking could prevent it - because both interpretations are valid. You want to race them, and prioritise the dependent interpretation.
1
Things get even uglier when you add in Agda's additional sugar:
(A B : Type) (C : Type -> Type) -> C A
It could be either function application or a dependent function, up until you get to the arrow. Then you go with the dependent function interpretation.
2
1
Show replies