Should inner modules have access to its parent's definitions?

[bugarela]

Our docs currently state that nested modules have access to its outer modules definitions. This implies a bidirectional interaction since the outer module can also access it's inner module's values with InnerModuleName::definitionName like expressions. Should we get rid of this behavior?

@konnov @shonfeder @Kukovec @thpani @rodrigo7491 @p-offtermatt what is your opinion on this inner propagation?

[Kukovec]

IMO keep this interaction (with the caveat below); You have two scenarios:

1. The inner module acts purely as a namespace (Inner below). The outer module defines a scope in which x is accessible directly, and the inner module defines a scope in which x2 is accessible directly. Since Inner lies within the former scope x is also plainly accessible within Inner as x. However, because the inner scope is atomic from other parts of Outer, access to x2 necessitates the namespace prefix Inner::x2.
2. The inner module is parameterized, i.e. it defines internal constants, and acts as a class (Inner2),. In this case, I would prohibit Inner2::y, but not <instance of Inner2>::y, since N is not well defined in the former case, but defined in the latter (we don't have a notion of "static" operators, so this is the best you can do). This case is otherwise the same as in (1) w.r.t. scoping.

Example:

 module Outer {
 var x: int

 def x_plus(z) = x + z

 module Inner {
   val x2 = x + x
 }

  module Inner2 {
   const N: int
   val y = x + N
 }

 pred inv = (Inner.x2 - x == x)
}

TLDR: Scala analogue - nested modules with no constants are objects and nested modules with constants are classes defined within the parent object/class.

[thpani]

This explanation makes sense to me, but I wonder if we should disambiguate them on the language level. E.g., like C++'s namespace blocks.

[konnov]

TLA+ modules have two main uses:

• To describe a state machine. I believe this is the original Lamport's intention.
• To describe utility operators that are applicable to any state machine. This is what we see in the community modules.

This is why I thought of stateful and stateless modules. Another option would be to differentiate between stateful and stateless modules by introducing two keywords: machine (for a state machine with variables and/or constants) and module (for a stateless module). I agree that namespaces are important for the stateless modules, whereas stateful modules should be accessed via instances.

[konnov]

We probably want stateless modules to be hierarchical and stateful modules to be flat.

[p-offtermatt]

Another option would be to differentiate between stateful and stateless modules by introducing two keywords: machine (for a state machine with variables and/or constants) and module (for a stateless module). I agree that namespaces are important for the stateless modules, whereas stateful modules should be accessed via instances.

This sounds right to me - if there is a difference in behaviour when accessing names in stateless vs stateful modules, then these should also look obviously different in the code in my opinion, e.g. being introduced with different keywords.

[p-offtermatt]

I think it's good to keep. It's listed in the doc as the recommended way to keep some names hidden, e.g.

module Local {
  var y: int
  def G(x) = set(_local.F(x))

  module _local {
    def F(x) = set(x, y)
  }
}

to hide F(x) outside of Local.

In such a case, both directions are important to have.

This seems to also be the behaviour for nested classes in Java, e.g. see https://stackoverflow.com/questions/5770575/can-an-outer-class-access-the-members-of-inner-classe

[konnov]

This discussion is not relevant anymore, since we have removed nested modules.