Handle units of literal constants by means of rules for the empty unit

[henrikt-ma]

I have prepared this PR in response to #2127 (comment).

Now, the proposal is hopefully easier to compare with the alternative designs, and we can keep refining it to our taste without cluttering the conversation in #2127 or the main PR of the MCP.

[henrikt-ma]

Ping, @bilderbuchi (I wan't able to add you as a reviewer).

[bilderbuchi]

Thank you for writing this up!

[henrikt-ma]

@bilderbuchi, so far you have helped me polish details of the presentation of this PR. Thanks a lot for this! Maybe you would also like to say something about the bigger picture of the proposal, that is, the idea to define unit checking with the help of empty units?

To me, the key feature of the proposal is that the resulting unit checking becomes a bottom-up analysis on the expression tree, as it makes unit checking easier to implement and reason about compared to alternative approaches that have been discussed in the past. Do you have any thoughts about this part? Would it deserve a non-normative comment in the specification text?

[bilderbuchi]

What I want to do next is extract the flow chart of the unit determination process as outlined in here. I hope that this will yield some insight where the proposal can be tweaked to become simpler structured. I found this harder than expected, so will have to break out pen&paper.

At this point I prefer @casella's smaller-scoped proposal, as it is much easier to make sense of, and thus get agreement to merge. One hope I have is that when we have flowcharts of both proposal, we might find a way to fit the smaller proposal (only dealing with the wildcard effect) into yours cleanly.

[henrikt-ma]

What I want to do next is extract the flow chart of the unit determination process as outlined in here. I hope that this will yield some insight where the proposal can be tweaked to become simpler structured. I found this harder than expected, so will have to break out pen&paper.

I think that this is where the bottom-up aspect comes into the picture: Rather than a flow chart, the essence of the proposal is that the unit of an expression is derived from the units of the children in the expression tree. Sometimes, the resulting unit of an expression is the empty unit, and one of four things may happen:

• Under certain circumstances, the empty unit can be propagated up the expression tree, postponing the transition to "standard dimensional analysis".
• Under certain circumstances, the expression can get an inferred unit for compatibility with dimensional analysis requirements.
• One might find oneself in the unfortunate situation of undefined unit semantics, but I'm pretty sure that any mechanism we come up with will leave lots of situations undefined until we do further work that's beyond this MCP. It is important that we leave things undefined rather than making rushed decisions to specify unit semantics in ways we might regret in the future.
• Otherwise, the unit of the expression defaults to implicitly being cast to "1".

What I am also trying to show here, beside the simplicity of having a bottom-up analysis, is that there's a clear path forward which comes down to gradually defining more and more unit semantics until there is no way to end up in the third item of the list.

[casella]

@henrikt-ma I think we should first make sure we agree on what I just wrote in #2127, to avoid misunderstandings. Then, I can proceed with the review, and also post my MCP proposal.

[henrikt-ma]

@bilderbuchi, I really appreciate your comments. Any change we could have a short screen sharing session for resolving them, while also being able to discuss the direction the proposal as a whole? If you're interested, please respond to [email protected], so that we don't clutter this issue with meeting planning.

[bilderbuchi]

You're welcome! :-)
I'd prefer to keep the context here, also to avoid rehashing discussions/points with/for others.
The direction of the proposal is your own, of course. I remarked on potential issues I perceive, and problems I ran into when I tried to put your proposal into a unit determination flow chart. I want to do my part to mature your proposal, so that when @casella's proposal comes in, we can compare both of them on their merits re #2127, and not lose time discussing/iterating avoidable issues/inconsistencies/etc.

[henrikt-ma]

The direction of the proposal is your own, of course. I remarked on potential issues I perceive, and problems I ran into when I tried to put your proposal into a unit determination flow chart. I want to do my part to mature your proposal, so that when @casella's proposal comes in, we can compare both of them on their merits re #2127, and not lose time discussing/iterating avoidable issues/inconsistencies/etc.

A challenge in preparing a solution for MCP-0027 is to delimit the design so that it addresses the unwanted literal constant wildcard effect, while still leaving enough gray areas open for future design. For me, it has been important to come up with a design where one can see a chance of this maturing into a complete specification of unit checking in Modelica. To make this visible, I found it necessary to put the empty unit handling in a context where some general rules about unit checking are stated already today, but at the same time I try to leave matters open where it is possible to do so without the risk of loosing sight of the complete unit checking solution.

This said, I now plan to do my best to address your comments without having you in the immediate feedback loop.

[bilderbuchi]

Also addition/subtraction? Or all operators? I'm not sure...

[henrikt-ma]

Yes, this is where I see a possibility to simplify the presentation by concentrating on just the propagations of the empty unit up the expression tree. Then we get this simple rule:

• All binary numeric operators as well as unary negation result in the empty unit if and only if all operands have empty unit. If one of the operands has non-empty unit, all operands must have non-empty unit, meaning that unit inference gets applied to the operands with empty unit.

[bilderbuchi]

Sounds good.

[henrikt-ma]

I gave it a try, and it seems to me that this led to considerable simplification of the proposal. Maybe we could consider this conversation resolved, and continue the discussion in conversations attached to the updated text?

(By the way, I'll be away until Monday.)

[HansOlsson]

Comparing it to #3266 (comment) it seems that it has the same critical flaw.

In general, my issue with some proposals is that there are way too much text and theory, but too little actual practice.

I can see that the other proposal - changed to not apply to addition and subtraction - does detect actual modeling issues; but also that it finds a number of issues that aren't that important and will take time to correct. I don't know if people are actually willing to put in the effort to correct - and I don't know the corresponding result for this proposal.

[henrikt-ma]

In general, my issue with some proposals is that there are way too much text and theory, but too little actual practice.

I think it needs to be seen in the light of me looking for a solid ground on which to implement unit checking in System Modeler, where the specification at least marks a starting point for something that can evolve into a set of rules that make unit consistency a model feature that is portable between tools.

[qlambert-pro]

In general, my issue with some proposals is that there are way too much text and theory, but too little actual practice.

Can you explain what you mean by that, because to me this proposal is very clear?

[qlambert-pro]

I can see that the other proposal - changed to not apply to addition and subtraction - does detect actual modeling issues; but also that it finds a number of issues that aren't that important and will take time to correct. I don't know if people are actually willing to put in the effort to correct - and I don't know the corresponding result for this proposal.

You are just describing the properties of a sound logical system, as opposed to a complete one.
At the end of the day, if MA wants the models produced with modelica to be portable it will have to opine on where unit checking should fall on the sound to complete spectrum. And most people, expects a sounder system when we talk about type checking. This will obviously imply a lack of backward compatibility, but then again the spec does not currently support the rejection of models relying on invalid unit use anyway.

[HansOlsson]

I don't see why this proposal has unit propagation separate from unit inference, and especially not why it would be a problem mixing unit propagation and unit derivation. Having separate rule sets makes it harder to follow, and also to me this raises the concern that a model may look correct and report some unit derivation, and then applying that in the model would give a unit error.

Similarly, I don't see why connect-equations must be treated differently.

If we connect flange_a and flange_b there will be equations for components of the connector - and to me, it seems natural that the unit-rules for connections are identical to the rules for the generated equations. Obviously, I can see reasons for having special code for unit-checking the connect-equations in practice (e.g., detecting the problem in the GUI - or just generating a better diagnostics message).

[henrikt-ma]

I don't see why this proposal has unit propagation separate from unit inference, and especially not why it would be a problem mixing unit propagation and unit derivation.

I found it hard to reason about unit derivations involving unit inference if the units of component references in the expressions wouldn't already be determined by unit propagation. I saw a big risk of ending up with complicated cyclic dependencies between the two, and that even if a tool could work it out it might be difficult to explain the errors in such entangled situations to a user.

Having separate rule sets makes it harder to follow

I expect it to make reasoning easier: The unit propagation mechanism should be a very simple mechanism which only serves to fill in "missing" units of components, and detect the very basic inconsistencies that don't involve any of the more complicated rules for deriving units of expressions. Once all components have their units, reasoning about units of expressions gets very much easier.

and also to me this raises the concern that a model may look correct and report some unit derivation, and then applying that in the model would give a unit error.

I don't understand this concern, could you elaborate?

Similarly, I don't see why connect-equations must be treated differently.

If we connect flange_a and flange_b there will be equations for components of the connector - and to me, it seems natural that the unit-rules for connections are identical to the rules for the generated equations. Obviously, I can see reasons for having special code for unit-checking the connect-equations in practice (e.g., detecting the problem in the GUI - or just generating a better diagnostics message).

It's because I'm afraid of making propagation based on sums in general. Therefore, I think there's a need to have something special for allowing unit propagation via the flow equations.