Unambiguous lexical indicators for state variables

[shonfeder]

Closely related to the discussion about actions in #207

Problematic

In TLA, (state) variables are state functions:

A variable x is a state function -- the state function that assigns the value s〚x〛 to the state s.

Understood from the perspective of the programs specified by a TLA formula, state variables correspond to globally visible mutable regions of state. However, a programmer familiar with sateful programming (which includes Haskeller's: they just have the discipline to quarantine their stateful sub-programs) will be led astray if they try to think of the state variables as mutable values within the context of a TLA spec (see #372 (comment)).

I don't know of a good, precise analog to the semantics of state variables within a TLA formula in any widely used programmings language I'm familiar with. A trick with Prolog DCGs for "Implicitly passing states around" is the closest thing I can think of.

Given the central importance, relative strangeness, and many gotchas of TLA state variables, they may be a good candidate for use of syntactic salt.

Motivation

1. We think it will help reason about specs if all state variables are visible at a glance, and identifiable purely locally, without having to refer back to the initial declaration of variables.
2. Having a clear lexical differentiator allows us to trivially enforce that <- can only be used directly on state-variables (and not, on references to them, e.g., passed in through operator parameters).
3. Adding a less familiar symbol will remind readers and writers of specs to consider these names in a special light.

Concrete syntax proposal

An option we've discussed is to add a distinctive lexical marker to all state variables. The concrete syntax suggested by @bugarela is prefixing variables with a @. iirc, this is inspired by Ruby's use of @ for class instance variables.

Translating an example from one of our example specs, this proposal would look like the following:

  var @board: int -> (int -> str)
  var @nextTurn: str // who goes next

  action Init = all {
    @nextTurn <- "X",
    @board <- 1.to(3).mapBy(_ => 1.to(3).mapBy(_2 => "_")),
  }

  def BoardIs(coordinate, player) =
    @board.get(coordinate._1).get(coordinate._2) == player

  action Move(player, coordinate) = all {
    BoardIs(coordinate, "_"),
    @board <- @board.set(
      coordinate._1, 
      @board.get(coordinate._1).set(coordinate._2, player)
    ),

[konnov]

I think I have continued the discussion on this in the wrong thread: #207 (comment)

[shonfeder]

On one hand, small specs almost entirely consist of constraints over state variables, so @ would just introduce unnecessary noise to a spec

Looking at the examples I've given, it doesn't seem to me to be very noisy at all in small examples that mostly only involve state variables.

So we could simply require to prefix with _ all names that are not state variables and constants

This doesn't give an unambiguous lexical marker for state variables, since state variables would still have the same lexical form as operators and constants.

One more point to the underscore solution. This is one is rather speculative. Local names (such as operator parameters) are usually shorter than the global names (such as names of the state variables), since they are local to their definition. So adding an underscore to them would not be as annoying as adding an underscore to a name of a state variable.

I feel like you may be overstating the costs of prefixing names with a single character. But, you also have loads more experience writing specs than I do. I guess this maybe a good candidate for followup user research?

Large specs leak name conflicts and break modularity. That is, if a module declares a local name foo somewhere in the code, this module is not composable with another module that declares foo as a state variable. So the lexical convention would solve the real syntax issue of composability.

iiuc, requireing the @ prefix on state variables would help with this, but requiring a _ prefix on operator parameters would not, because operator names and let bindings defined with val can still be defined that would clash with state variables.

[konnov]

Maybe I am just having trouble with the @ character. I tried to use it in a small spec, and it looks foreign (maybe not to ruby programmers!). How about :x or ::x?

[romac]

Just a note that, in some languages, a variable starting with an underscore denotes an unused variable, either by convention or enforced by the compiler.

[bugarela]

I dislike prefixing things with underscore in general, due to what Romain pointed out about it detonating unused variables.

As for adding a prefix symbol to state variables, I really like the idea. The thing I struggle with most when reading specs for the first time is the amount of back-and-forth scrolling to remember which names are state variables. The IDE can help with that a lot by highlighting those names with a different color and outlining the objects in the file (as the TLA+ VSCode plugin does), but adding a prefix symbol will:

1. Make this IDE features much easier to implement and lightweight (as it becomes syntax highlighting as oppose to semantic highlighting)
2. Be GitHub compatible (as there is no semantic highlighting for GitHub as far as I can tell, and code navigation is only available for the most used languages)
3. Be more friendly to unsupported text editors (i.e. Ctrl + F @myVar on plain text)

As for @ vs : or ::, I understand that not many people are used to ruby, but I'd prefer to pick something with some background than choose something completely new. And, if people can get use to it in ruby, that's basis to assume people will also get use to it in Quint 😛. But this are just some rational arguments, as I'm personally not particularly in favor of either.

[shonfeder]

I find @bugarela's reasoning compelling here, and it aligns with my own intuitions.

I'm worried that that prefixing with : or :: will look weird in collision with type annotations:

var :foo: Int

vs

var @foo: int

Another point against :: is that it requires twice as many characters :)

What sort of process should we use as a tie breaker here?

[konnov]

I don't think we are going to change this in the near future. But we can always reopen this discussion!