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
literally just `(a : A) -> A`
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.
So yeah, the parser needs to take into account that any time, something starting with `(` could suddenly turn into a dependent function type - but only sometimes. `(A) -> A` is non-dependent, for example.
2
seems like the real issue is overloading of parens!
2
1
1
Show replies
Replying to
right now i’ve not thought about this enough to agree with you, i’m thinking of 3 different possibly broken or not ways i’d try to hack around that