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.
2
1
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.
Yeah, that’s why my function types start with a keyword
Possibly - but braces are scarce, even more so in a DT language. I could actually have a starting sigil for ‘patterns’, which could help.
1
Show replies