Allow to write predicates without question marks

[facundominguez]

Recently #678 introduced the ability to write predicates inside other expressions by using a question mark.

This issue is to investigate if we can remove the question mark.

[facundominguez]

I'm guessing we could use some insight on why liquid-fixpoint has separate parsers for predicates and expressions.

Is the difference between a predicate and an expression only about the operators that they use?

I think that by removing the question mark, the grammar becomes left recursive via: expr0P -> predP -> pred0P -> predrP -> exprP -> expr1P -> expr0P. But I'd like to understand better the motivation of the current implementation ahead of considering changes.

[ranjitjhala]

@facundominguez the honest answer is it is just a quirk of history. Originally we had separate types Expr and Pred and the former were not supposed to be bool valued, but over time this became untenable and so they are all really just a single type BUT the parser somehow still kept this (needless) stratification… so really no good technical reason!

[facundominguez]

Thanks @ranjitjhala. That is helpful to know. In that case, probably we should try consolidating the parsers.

[ranjitjhala]

indeed though even better may be to switch over to a full SMTLIB style prefix-parens syntax …

[facundominguez]

... yes, Ranjit, please start a new issue if you want to change the user interface that far :)

Please correct me if I'm wrong: if Liquid Haskell continues to use the current language, only removing the question mark might still worth the trouble.

[ranjitjhala]

Yup, you’re right! :-)