[CLOSED] Should we have three different application syntaxes?

[bugarela]

As stated in the language specification:

---

Three forms of operator applications

Quint is flexible with respect to operator applications. It mimics several call
styles that can be met in various languages. Given an operator called f and
expressions e_1, ..., e_n, the operator f can be applied to the
expressions e_1, ..., e_n as follows:

1. Quint normal form: f(e_1, ..., e_n).
2. UFCS: e_1.f(e_2, ..., e_n)
3. Infix form: e_1 f e_2, ..., e_n

---

Although this allows more flexibility, it can also make the language harder to learn, examples more inconsistent, and overall bad to community interactions. We should probably choose one form and stick to it, as stated by @jtremback when he brought this to my attention.

What do folks think about sticking to the normal form and removing both UFCS and infix forms? @shonfeder @thpani @konnov @Kukovec @rodrigo7491

[konnov]

I think this would lead to a very rigid syntax, which some people would like and some don't. As I wrote somewhere earlier, we could write automatic reformatters that adhere to only one specific form. For instance, we are doing exactly this in Scala. IMO it is too early to choose one form over another. Once we have a working plugin, we can conduct a user survey. The syntax is well-isolated in the parser.

[Kukovec]

My personal preference is towards (1) and (2), but neither globally.
(1) is well-suited for symmetric or polyadic operators, e.g. and(p,q,r) over p.and(q,r).
(2) is better for some asymmetric operators (mostly over sets), e.g. S.exists( x -> P ) or S.fold(init, (v, x -> e)), but not for others, e.g. S.setOfMaps(T).
I actively dislike (3) in all cases except for symbolic infix operators (+, %, >=, etc.), especially for operators of arity > 2.

[bugarela]

I'm in favor of this. This was my gut feeling since the beginning, I was just not able to justify it to myself. Your motivation is good.

[thpani]

Caveat emptor: I know almost nothing about Quint.
I'm also in favor of this. Different call styles make sense, and I think the language should be opinionated on this to guide the user.

Minor comment: The way (2) is used here looks less like UFCS, rather than Smalltalk-style message passing. Which would fit nicely; use (2) whenever there is a distinguished "object" (here: set, function, ...) in the operator application.

[shonfeder]

I'm really inclined to agree that (3) is undesirable.

I'm instead inclined to just go with (1). With one exception, I don't see the . call notation actually clarifying anything.

I particularly don't like the idea that we'd sometimes have to use . for application and sometimes have to use prefix notation. That inconsistency in Python's syntax is one of its many warts, IMO. Why do we have to do len(ls) to get to the length of a list but ls.append(x) to update it? Similarly, why do we have to do setOfMaps(S, T) to get the set of maps but S.mapOf(x -> e) to map over it? Any particular author may have their own more or less subtle reasoning for deciding when one style of invocation makes sense over another, but this invariably ends up feeling arbitrary to someone else. So, imo, if we decide to keep (2) at all, I'd be in favor of keeping it uniform.

The one exception is the case of function composition via "method chaining. (Your example of S.update(x,y).update(u,v). If this is only mechanism we can have for composing operators, then it's probably worth keeping, tho I'd actually be in favor of instead supporting application and having a pipe or composition operator.

[thpani]

I particularly don't like the idea that we'd sometimes have to use . for application and sometimes have to use prefix notation. That inconsistency in Python's syntax is one of its many warts, IMO. Why do we have to do len(ls) to get to the length of a list but ls.append(x) to update it?

Because len(ls) provides a consistent, uniform interface.

Similarly, why do we have to do setOfMaps(S, T) to get the set of maps but S.mapOf(x -> e) to map over it?

For the same reason. There is no reasonable, unsurprising way to call setOfMaps via prefix syntax, is there? Except maybe (S, T).setOfMaps().

Wouldn't prefix syntax actually clash with you desire for uniformity? Why have indices(ls), keys(f), fieldNames(r) when they all do the same thing?

[bugarela]

I really like the @shonfeder 's idea of introducing pipes instead of (2). Suppose |> is our pipe operator, we could write things like S |> mapOf(x -> e), S |> setOfMaps(T), S |> update(x,y) |> update(x,y). It's more common to see pipes as an alternative to function-style aplications than UFCS. I would like us to go in a direction people are more used to.

[konnov]

Although this allows more flexibility, it can also make the language harder to learn, examples more inconsistent, and overall bad to community interactions.

Just on that point. Three forms are not hard to learn. We just have to explain them once. A large number of syntax forms a-la TLA+ are really hard to learn though.

[konnov]

1. It will make the grammar much more complex, which is the opposite of what I wanted.
2. We do not seem to have a clear consensus on how specific operators should be written.

[thpani]

re (1): why is a a simple grammar such a priority? was this a design decision down the road? I couldn't find it documented anywhere.

[konnov]

It was a design decision:

Quint should be easy to parse:

It uses a small set of syntactic rules (its ANTLR4 grammar is 120 SLOC).

Quint is an anti-thesis to TLA+. Whereas TLA+ is baroque and full of rules (because of math), Quint is minimal pretty much everywhere, where it makes sense. The hope that at some point we will reach synthesis :)

[thpani]

Aaah, thank you!

Doesn't having 3 call syntaxes directly violate "easy to parse" though?

Or, phrased differently, I think this discussion is about resolving priority between

Quint should be easy to read

and

Quint should be easy to parse

[konnov]

True. There is a conflict between these two points. However, some people say that operator/function overloading makes program harder to read. Obviously, it still exists in many languages, because many people find such programs easier to read too.

[shonfeder]

I'm in favor of removing both (2) and (3), but feel more strongly about removing (3).

If we want to prioritize flexibility of syntax in the direction of infix operators, I'd be in favor of us fully embracing that direction and going for mixfix notation via operator precedence grammars. Having this limited, special case treatment of each function as also an infix notation, with the (imo) very unusual trailing commas list doesn't make much sense to me.

[konnov]

The third form is probably the most obvious candidate for removal (except all math operators should be in this form). However, it may work for people who strongly dislike dots and parentheses, which is the direction of TLA+. Since we do not have the danger of Quint spreading in one day like JavaScript, we can afford a bit of experimentation. Removing things is easy.

We see these three forms appearing in various languages, so I do not want people to reject the syntax for reasons like "it does look like Pascal or Python too much".

Btw, the C syntax offers some flexibility too, which nobody is using. For instance, instead of accessing an array with arr[i], one can write i[arr], since the both are normalized to *(arr + i). It is a technicality, and nobody cares about it. Most likely, people will learn from examples the specific choice of each form for each operator. So I do not see these three forms as a big problem yet.

[shonfeder]

Do you have any other languages in Mind that use infix syntax like x op a, b, c? I’ve never seen infix syntax that will take an un-bracketed sequence of arguments on like that in the rhs. I’d be interested in learning where that comes from :)

[konnov]

Do you have any other languages in Mind that use infix syntax like x op a, b, c? I’ve never seen infix syntax that will take an un-bracketed sequence of arguments on like that in the rhs. I’d be interested in learning where that comes from :)

Yeah, x op a, b, c is really rare, though I have seen it somewhere too. Most likely, x op a is the only reasonable use for the infix notation.

[konnov]

Wouldn't prefix syntax actually clash with you desire for uniformity? Why have indices(ls), keys(f), fieldNames(r) when they all do the same thing?

Ah, that's a very good question. In TLA+, there is only one operator for them, which is called DOMAIN. If we want to have the same operator work for functions (maps), sequences, tuples, and records, then we have to introduce ad-hoc polymorphism (often called function overloading). This only feature made type inference for TLA+ much harder than it could be. Because of this only feature, Snowcat sometimes fails and asks for additional type annotations of let-in definitions. Although we could support ad-hoc polymorphism, we do not have to. TLA+ specifications are relatively small and there is no good reason for having operator overloading.

[shonfeder]

In our discussion last week @konnov seemed to agree on dropping on the universal infix form of application. So this would leave us only with only applications form 1 and 2. This will also fix #79.

[shonfeder]

I think this discussion is resolved for now!

[shonfeder]

Oh, I thought there was a way of closing/resolving discussion. But there is not https://github.com/orgs/community/discussions/3097

So now I've just bumped this discussion to the top of the stack :/

[konnov]

Yeah, I also wanted to close this discussion and found no way to do it. Let's just change it's title to [CLOSED].