Instantiation (or assignments) of replaceable elements

[modelica-trac-importer]

Reported by choeger on 1 Nov 2012 12:34 UTC In current Modelica, type redeclarations have to be covariant.

  class Foo
    replaceable record Super Real x; end Super;
    parameter Super t;
  end Foo;

i.e. in class Foo to redeclare Super a record at least needs to declare a field Real x but might have more fields (this allows safe substitution in case of projections).

This covariance rule leads to problems when the model containing the replaceable also contains some "assignments" to the polymorphic value:

  class Foo
    record Equal Real x; end Equal;
    replaceable record Super Real x; end Super;
    parameter Super t = Equal(5.0);
  end Foo;

The model above can be instantiated safely. Unfortunately if anyone actually tries to redeclare the type Super, i.e.:

  record Sub
    Real x; Real y;
  end Sub;

  Foo f(redeclare record Super = Sub);

This causes the value f.t.y to be undefined, which is a classical type-error. Note that I used a parameter, since in the case of equations one might be tempted to get away with "scalarization" (Thus leaving undefinedness open until simulation).

The problem is that Foo states that it works for any subtype of Super, yet it actually only works for equivalent types.

Naturally if someone actually tries to instantiate the second snippet, it will fail. But the user is in no position to see why it fails (since the cause of the error is inside Foo and might be authored by someone else).

A similar issue seems to be addressed by the plug-compatibility requirement.

IMO there are three possible solutions:

1. expand the definition of restricted subtyping in section 6.4 to a broader definition and enforce it.
2. simply forbid instantiation of replaceable elements with parameters (thus the default constructor can be used which is naturally also redeclared and provides values). Use modifications to locally change single fields.
3. Explain any "assignment" to structured components by equality + modifications (thus any "undefined" value would always be copied from some other instance).

Personally I'd like to see 1. implemented, 2. is rather restrictive and 3. might confuse users (since it looks like, but is not like mutable elements).

any comments?

---

Migrated-From: https://trac.modelica.org/Modelica/ticket/895

[modelica-trac-importer]

Comment by hansolsson on 1 Nov 2012 13:43 UTC I believe the original idea was the following, which could be seen as variant of (1)

4. For record-equality require that the two records are the same regardless of redeclare; e.g.:

   class Foo
   record Equal Real x; end Equal;
   replaceable record Super Real x; end Super;
   parameter Super t = Equal(5.0);
   end Foo;

   is already an error since 'Super' and 'Equal' are not the same; i.e. even before you actually perform the redeclaration.

Similarly:

  class Bar
    record Equal Real x; end Equal;
    replaceable record Super Real x; end Super;
    parameter Super t;
  end Bar;
  Bar b1(redeclare replaceable record Super=NewSuper);
  Bar b2(redeclare record Super=NewSuper, t=b1.t);

is an error since there could be different redeclaration of 'Super' for b1 (since the redeclaration is replaceable). Note that with a non-replaceable redeclare it should be legal.

Unfortunately this is not trivial to describe and ensure that it is consistent.

[modelica-trac-importer]

Comment by choeger on 1 Nov 2012 17:23 UTC Replying to [comment:1 hansolsson]:

is already an error since 'Super' and 'Equal' are not the same; i.e. even before you actually perform the redeclaration.

That sounds weird. AFAIK Modelica had always been structural. So in your example, both records are equivalent (both are subtypes of the other).

is an error since there could be different redeclaration of 'Super' for b1 (since the redeclaration is replaceable). Note that with a non-replaceable redeclare it should be legal.

Unfortunately this is not trivial to describe and ensure that it is consistent.

That I don't understand? How can b1 be an error? AFAIK such stuff is used everywhere in the MSL?

[modelica-trac-importer]

Comment by hansolsson on 2 Nov 2012 10:09 UTC Replying to [comment:2 choeger]:

Replying to [comment:1 hansolsson]:

is already an error since 'Super' and 'Equal' are not the same; i.e. even before you actually perform the redeclaration.

That sounds weird. AFAIK Modelica had always been structural. So in your example, both records are equivalent (both are subtypes of the other).

They currently have the same value, but they are not bound together; so a sort of fragile equivalence, which ideally should be detected. There is probably a fancier terms for it (related to dependent type?). It is not directly related to structural vs. nominal types; but it is not a straightforward issue.

Similarly:

  parameter Integer n=2,m=2;
  Real x[n];
equation
  for i in 1:m loop
    x[i]=2;
  end for;

The variable is of size n and the equation is of size m. Since both are 2 they have the same value - but the sizes are not "the same", since a simple modifier can break it, see Locally balanced in section 4.7.

[modelica-trac-importer]

Comment by choeger on 2 Nov 2012 10:45 UTC Replying to [comment:3 hansolsson]:

They currently have the same value, but they are not bound together; so a sort of fragile equivalence, which ideally should be detected.

They are equivalent types. I do not understand what you mean by "bound". Neither does this word occur in section 6.1 or 6.2.

It is not directly related to structural vs. nominal types; but it is not a straightforward issue.

In fact, if you write down the types in Modelica the only difference is their name. Thus, it is exactly related to structural vs. nominal types. In a nominal type system, they are different, in a structural type system they are equivalent.

Similarly:

  parameter Integer n=2,m=2;
  Real x[n];
equation
  for i in 1:m loop
    x[i]=2;
  end for;

The variable is of size n and the equation is of size m. Since both are 2 they have the same value - but the sizes are not "the same", since a simple modifier can break it, see Locally balanced in section 4.7.

I do not see, how this example is related to the ticket. You only showed a principal difficulty of the careless usage of dependent typing in current Modelica: If you insist of making the size part of the array type, you cannot (in general) typecheck the snippet above before evaluating it. In other words: You cannot do any meaningful non-local typechecking.

But this has nothing to do with the constraining type problem above.

[modelica-trac-importer]

Comment by hansolsson on 2 Nov 2012 11:33 UTC Replying to [comment:4 choeger]:

Replying to [comment:3 hansolsson]:

...

Similarly: {{{ parameter Integer n=2,m=2; Real x[n]; equation for i in 1:m loop x[i]=2; end for; }}} The variable is of size n and the equation is of size m. Since both are 2 they have the same value - but the sizes are not "the same", since a simple modifier can break it, see Locally balanced in section 4.7.

I do not see, how this example is related to the ticket.

The issue is that you have something that is ok for the current (default) values of parameter; but you can set parameters to make the sizes different.

The specification says in 4.7:

"A tool shall verify the “locally balanced” property for the actual values of parameters and constants in the simulation model. It is a quality of implementation for a tool to verify this property in general, due to arrays of (locally) undefined sizes, conditional declarations, for loops etc"

So the snippet above is not really correct; but a tool is not required to check it. It would legal if it instead had 'final parameter Integer m=n;'; even though 'n' is still unknown.

That snippet uses integer parameters; my point is that this ticket is about the equivalent problem for class parameters, and I believe they should be treated in the same way.

[modelica-trac-importer]

Comment by choeger on 2 Nov 2012 12:37 UTC Replying to [comment:5 hansolsson]:

That snippet uses integer parameters; my point is that this ticket is about the equivalent problem for class parameters, and I believe they should be treated in the same way.

Ah I see. The point here is, that the problem you are describing might seem similar (since we are indeed talking about abstraction/parameters in both cases), but occurs on a different level. If you want to check the "locally balanced" property, you have to take the actual model-instance (aka a value), so you are acting on the value-level. I do not see a way to avoid this, since Model instantiation is turing-complete.

If you want to check the usage of type parameters, you should be able to handle that at the application site with only the type-signatures (or interfaces) at hand. Currently there is no rule to do so.

While thinking about this issue, it became more clearer to me, what solution 1. would probably need to look like.

In a case like this:

model A
  replaceable record R Real x; end R;
  parameter R r = someExpression;
end A;

We can figure out, what type someExpression yields. Let's assume it is R2. Now for the assignment to work, we have a contravariant constraint: R2 <: typeof(r) (where typeof denotes the actual type after redeclaration. Our current spec also tells us, that: typeof(r) <: R.

So, in summary, we get: R2 <: typeof(r) <: R

Applied to my earlier example, the result would be that the redeclaration would be invalid, because the following relation does not hold: Equal <: Sub, this could be detected at the point of the modification.

Note, that enforcing this solution would be absolutely backwards compatible, since we only get better error detection. Yet, it also has some drawbacks:

1. It uses some kind of type-inference (R2 needs to be inferred), which is unusual in Modelica. Inference might lead to a non-decidable system when combined with other features, although I do not think it is very likely.
2. The contravariant constraint is invisible in the source code, thus a user without some significant help from a tool might simply not see the constraint and wonder about "that strange error".

Although I think such a solution would be ideal, it might be much simpler to take solution 2. (I think languages like Java handle it that way):

Instead of checking for valid/invalid redeclarations, we can simply forbid the original model. Accroding to it's own interface, it accepts all possible subtypes of R, thus the assignment is a type error (since it simply does not work for all those subtypes).

The biggest problem with that is, that it might break existing code in e.g. the Media library.

[modelica-trac-importer]

Comment by hansolsson on 5 Nov 2012 09:50 UTC Replying to [comment:6 choeger]:

Replying to [comment:5 hansolsson]:

That snippet uses integer parameters; my point is that this ticket is about the equivalent problem for class parameters, and I believe they should be treated in the same way.

Ah I see. The point here is, that the problem you are describing might seem similar

My point is that it not only seems similar, but is the same. Consider the two models:

model A
  parameter Integer par1=default;
  parameter Integer par2=default;
  parameter Real x[par1];
  Real y[par2];
equation
  x=y;
end A;
model B
  replaceable record Par1=Default;
  replaceable record Par2=Default;
  parameter Par1 x;
  Par2 y;
equation
  x=y;
end B;

These are bad models, since if you modify just one of par1 and par2 you will normally make 'x=y' incorrect.

In this case the restriction on modifiers is that par1=par2; but one can easily give more complex cases (e.g. m=n*2+div(n,2)*n or even worse).

The spec states that A is invalid; and thus puts the burden on the model developer - not the model user and my point is that we should do the same for B.

Verifying correctness in this way for A can be complicated (NP-hard?, halting problem?); and thus tools do not have to verify this. However, a tool can always check A for the given parameter values when an error is found.

Instead of checking for valid/invalid redeclarations, we can simply forbid the original model. Accroding to it's own interface, it accepts all possible subtypes of R, thus the assignment is a type error (since it simply does not work for all those subtypes).

The biggest problem with that is, that it might break existing code in e.g. the Media library.

Yes, that is my suggestion.

We will have to check Media (and also Fluid) libraries - although there are a number of restrictions in Modelica that makes it more likely that the code is correct (e.g. subtyping requires that elements are plug-compatible and not sub-types).

[modelica-trac-importer]

Comment by hansolsson on 4 Dec 2012 22:56 UTC Language group: Need a larger discussion.

[modelica-trac-importer]

Modified by dietmarw on 4 Dec 2012 23:11 UTC

[modelica-trac-importer]

Modified by otter on 20 Sep 2013 10:22 UTC

[modelica-trac-importer]

Comment by hansolsson on 23 Sep 2013 16:01 UTC Language group: needs too much work for 3.3r1.

[modelica-trac-importer]

Comment by hansolsson on 1 Mar 2017 13:42 UTC The specification says in 4.7:

"A tool shall verify the “locally balanced” property for the actual values of parameters and constants in the simulation model. It is a quality of implementation for a tool to verify this property in general, due to arrays of (locally) undefined sizes, conditional declarations, for loops etc"

Seems difficult to specify more (combining usability and possibility to verify), thus this seems the best we can get. Agreement by acclamation.