Shall we allow for shadowing?

[konnov]

We copied the rule from TLA+ that name shadowing is not allowed. While it is, in principle, a nice rule for single-module specifications, it introduces problems with module composition. We have been running into the same problems with TLA+.

The most annoying case is perhaps the collision of state variables and definition parameters:

module C {
  module A {
    var x: int
  }

  // this could be an imported library developed by someone else.
  module B {
    def plus(x, y) = x + y
  }

  import A.*
  // the parameter x collides with the state variable x
  import B.*
}

While it is easy to keep track of naming conventions in your specs, it is hard to do so in external libraries. For instance, if the library author decides to rename a definition parameter, the new version may introduce a naming conflict.

If we decide to allow for shadowing, we will have to rename names in a Quint spec, before translating it to TLA+.

[bugarela]

Here's an idea that doesn't directly answer the question but might help with conflicts: use some sort of prefix to access state variables, like this. in many OOP languages, or @ in ruby. I particularly like the ruby's @ which is quick to type and very nice to visualize as all syntax highlighters will use an unique color for those variables. Here's an example in ruby:

class A
  def initialize(x)
    @x = x
  end
  
  def plus(x, y)
    x + y
  end

  def plus_x(x)
    x + @x
  end  
end

[konnov]

Interesting point!

[shonfeder]

I really like the idea of introducing some lexical disambiguation of state variables. Shadowing question aside, it's nice how it makes all the state variables immediately clear at a glance!

A nice thing about having a prefix however is that we might use it to track two separate state-spaces that are merged into the same scope....?