What’s the tiniest example program that has this ambiguity and uses both flavors ?
Conversation
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.
2
seems like the real issue is overloading of parens!
2
1
1
It gets so much worse when you want to add operator sections. Now you have one more overload `( expr op )` for each operator, and they even need to parse `expr` with different precedences! Feels like the most vexing parse for LL parsers.
1
1
Sacrifice more bracket sigils to the parse gods!!
1
1
I did actually propose something in that direction
Quote Tweet
We're thinking of replacing the `(= 5)` operator section notation with a more mathy `· = 5`. This both makes parsing easier and less ambiguous (think `(-1)`) and extends naturally to notations of higher arity (`Γ ⊢ · : ·`).
Show this thread
3
1
I like Agda's approach of using `_` for sections - eg. `_= 5`
2
Not sure if it can handle `Γ ⊢_:_` though...