Looks like an inherent ambiguity that is not solvable by priorities, since those select between a re-ordering of the tree using the same productions. Will do an experiment with SDF3
Conversation
The grammar above is indeed inherently ambiguous. For example, how would you parse `z (a : b)(c : d) -> e f` ?
2
Yeah, I'm curious what Agda does there. I would expect a language to at least say 'help, add parens here please!'
1
Oh, Agda lacks `:` for type annotation, again getting around this issue. 🤔
2
I wonder if has a thought. In some ways type annotation in terms being related to proof search? Assuming / hypothesis vs proof cut? Idk.
1
1
Not sure on what exactly you mean but it sounds like bidi typechecking is relevant: there type annotations let you embed checking terms into synthesis terms.
2
This Tweet is from a suspended account. Learn more
So there’s a certain precise way that : in pi and other type formers is fundamentally different from : as annotation or cut, and we all just are usually programming in settings where this distinction isn’t visible ?
1
1
This Tweet is from a suspended account. Learn more
Yeah, that's a good way to look at it, thanks! I guess I've been a fan of `(x : S) -> T` because a seems to build a nice bridge from programmers who understand `S -> T` (in contrast to `Π x : S. T` and `∀ x : S. T`.
1
But yeah, you are indeed right that it might end up looking like an 'annotation', which has shown up in my explanations and wording! If you thinking strictly right-to-left that is (as most English speaking programmers do I guess). 🤔