Types with the same name, but declared in different packages: are they the same?

[pefribeiro]

My intuition is that they are different, but we already accept that events and variables, of the same name, declared in different interfaces, are the same. I think we may not have fully considered what happens with types. Minimal example below.

Suppose we have a package B in resource b.rct:

package B
type D

interface IVar {
    var x:D
}
stm STM {
    requires IVar
    initial I
    final F
    transition T0 { from I to F }
}

we declare a type D and an interface that declares a variable x of type D, and a state machine STM that requires x.

Now suppose we have a package A in resource A.rct:

package A
type D

controller ctrl0 {
    var x:D
    sref STM=B::STM
}

The controller ctrl0 references state machine STM from package B directly using B::STM. The type-checker does not flag this as an issue, because the variable x of a type named D is provided by ctrl0 as required by B::STM. However, my understanding is that these types are not the same. Similar issue applies when connecting events whose types' names match, but which are declared in different packages.

This issue is somewhat related to the discussion of issue https://github.com/UoY-RoboStar/robochart-csp-gen/issues/111, in that we can refer to elements of another package using qualified names. This is, in general, useful in a number of situations, namely for the translation from RoboChart to RoboSim. But even if we restricted the referencing of elements using qualified names, and we required use of an import B as follows:

package A
import B::*
type D

controller ctrl0 {
    var x:D
    sref STM=B::STM
}

The validator does not complain that we now have two types of the same name in context. This is a problem of its own.

Still related to https://github.com/UoY-RoboStar/robochart-csp-gen/issues/111 there is a question as to whether we should be able to import individual elements. In that case, I believe import B::STM would not necessarily bring the type B::D into context?

This issue surfaced from an example produced by @madielfilho's translation, which was giving errors in FDR, but not in the validator. There was a mix in usage of types, of the same name, from different packages. The correct treatment there is to, anyway, avoid using types with the same name from different packages. I think that the core issue with imports is subtle.

[pefribeiro]

Just recording here that in discussion with @ana-york we've come to the conclusion that elements at the level of a package are unique to that package, thus the name of a type should include the name of its package as well, if there is one. Thus, what needs to be done is to modify the validator to consider the full name of a type.

[alvarohm]

I think types D in packages A and B are different types. The validator should complain that there are two types with the same name.

When you say that "the name of a type should include the name of its package", do you mean in its own package or where it is imported? For example,

package A type D controller ctrl0 { var x: A::D }

or

package A type D controller ctrl0 { var x: D var y: B::D }

I'm using the 'default' implementation of imports from Xtext, and I don't think it supports imports without the wildcard, but it allows us to refer to anything in the project via the qualified name (without first importing the package), so the second package A above should be allowed (B does not have to be imported).

On Tue, 17 Jan 2023 at 16:12, Pedro Ribeiro @.***> wrote:

Just recording here that in discussion with @ana-york https://github.com/ana-york we've come to the conclusion that elements at the level of a package are unique to that package, thus the name of a type should include the name of its package as well, if there is one. Thus, what needs to be done is to modify the validator to consider the full name of a type.

— Reply to this email directly, view it on GitHub https://github.com/UoY-RoboStar/robochart-textual/issues/68#issuecomment-1385667409, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABEHMYIDJT6AR3QEIHAQLUDWS3AGTANCNFSM6AAAAAAT54PE34 . You are receiving this because you were assigned.Message ID: @.***>

[pefribeiro]

I think types D in packages A and B are different types.

Yes, we think so.

The validator should complain that there are two types with the same name.

I suppose this could be optional, depending on the import mechanism, but currently the validator doesn't complain. We could take the view that by default if in package A you import B::*, then use of D refers to the local declared type, unless it is fully qualified with B::D. (I think that's what the scope provider does at the moment too.)

When you say that "the name of a type should include the name of its package", do you mean in its own package or where it is imported?

I meant for the purpose of determining the type's full name, so that types D in packages A and B are different. The type-checker does not currently do this.

For example, package A type D controller ctrl0 { var x: A::D } or package A type D controller ctrl0 { var x: D var y: B::D }

I think the latter is supported at the moment?

I'm using the 'default' implementation of imports from Xtext, and I don't think it supports imports without the wildcard, but it allows us to refer to anything in the project via the qualified name (without first importing the package), so the second package A above should be allowed (B does not have to be imported).

I'm not sure if this was intended, but based on my experiments it seems to work without the wildcard to import specific elements one at a time.

[pefribeiro]

Just to clarify above regarding use of D, based on my observations, what I think currently happens is:

1. If D is declared in the local package, and in one or more imported packages, then D refers to the local one, unless one specifies the fully qualified name, eg. B::D.
2. If D is not declared in the local package, but is declared in one, and only one of the imported packages (say using import B::*), then use of D refers to type D as declared in the imported package (ie. D and B::D refer to the same type).
3. If D is not declared in the local package, but is declared in multiple imported packages, then use of D doesn't work. I suppose it shouldn't, because it's use is ambiguous and it could get really confusing. In this case, fully qualified names need to be used.

Usage seems fine to me, but it still stands that currently the type-checker doesn't seem to distinguish the types properly, particularly when validating provides/requires and the event connections.