quint: Don't treat `{exp}` and `(exp)` as synonymous

I like the separation of lambdas into pure- and effect-lambdas, but we then have to be consistent in the enforcement. For example, set map cannot take an action, so, for example, S map { ... } should never be allowed. You can only write S map (x -> ...) or S.map(x -> ...), omitting a set of parenthesis (i.e. not S.map( (x -> ...) ). Same for exists (but not guess), forall, filter, etc.

Well, the TLA+ semantics is not different. But the distinction between the action mode and other modes is quite important. That’s what TLA+ puts under the rug. I want to make it visible and statically checkable.

Ah, sorry, I was thinking the context of tnt+. The non-determinim is an issue even here tho, iiuc.

I don’t know whether it holds for all TNT expressions, but one of my goals was to eliminate non-determinism in the non-action modes. Non-determinism should be very well-isolated, because it is a side effect 😃

I don’t find this to be a perspicuous expression of the logic. IMO, this seems convoluted and hard to read, given what it does.

action MyAction =
  val someP = S.exists(x -> P)
  {
    | { someP & y <- y + 1 }
    | not(someP)
  }

The conditional is still an expression, that’s right. In most cases, some people might want to write x' = 1 and apalache would treat that as an expression, no side effects. Btw, that would be impossible in TNT 😃

My inclination is to say that our question should be: are the branches of a conditional and the body of an operator just expressions like any other?

If so, we can just pick one form of brackets for grouping expressions, and use that consistently. (For if, this becomes cleaner imo if we use if exp then exp else exp (which is similar to may existing languages, including TLA+).

Examples:

if (a & b) then ( c & d & e ) else ( z )

def A(x) = (
  & a 
  & b 
  & c
) 

Otherwise, if these scopes are meaningfully different from regular expressions, then we can have a principled justification for using different scope delimiters, like we already do for modules. Then we can explain why use of {...} would have a principled, non-ambiguous use in these two cases, while still not overloading it to do double duty.

To make the reason for my concern more concrete, iiuc, this following will valid if we allow {...} and (...) to by synonymous (except when they aren’t, for module scope and delimiting operator arguments):

module Foo = {

def B(x) = (
  if {x} ( 
    x map {y -> y + 1} 
  ) else { 
    x map (y -> {y + 2} - 3) 
 }
)

def A(x) = {
  if (x) {
      & a 
      & ( 
          | { b & c }
          | d
        )
  } else (
    {z & y}
  ) 
}

}

While this could just be left up to coding style, I don’t understand what would justify inviting this kind of chaos! 😄