Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added "four-line" proposal for units of literals #3266

Open
wants to merge 24 commits into
base: MCP/0027
Choose a base branch
from

Conversation

casella
Copy link
Collaborator

@casella casella commented Oct 25, 2022

Here is my concrete proposal for MCP/0027. The normative text is a few lines (not sure if four or how many), I also added a bit longer description of the rationale in the non-normative text, to clarify why it is formulated in that way.

@casella casella requested a review from HansOlsson October 25, 2022 16:37
@casella casella requested a review from henrikt-ma October 25, 2022 16:41
@henrikt-ma henrikt-ma added the MCP0027 Unit checking label Oct 25, 2022
@henrikt-ma
Copy link
Collaborator

It seems like this proposal has a similar shortcoming as in #3257 when it comes to allowing for connector variable unit inference. I think both proposals should to be modified to not rule out such unit inference.

For example, I expect that the literal in the following model is expected go get unit "1", even though u has unit "":

block Double
  Modelica.Blocks.Interfaces.RealInput u;
  Modelica.Blocks.Interfaces.RealOutput y;
equation
  y = 2 * u;
end Double;

@HansOlsson
Copy link
Collaborator

My main concern is that we seem to have a number of models where numbers are assumed to have a unit, e.g. Modelica.Electrical.Batteries.Examples.BatteryDischargeCharge where Ri=cellData1.OCVmax/1200 (the 1200 is assumedly a current), or Modelica.Electrical.Machines.Utilities.ParameterRecords.IM_SquirrelCageData, and all of the Modelica.Electrical.Spice3.Internal.Mos formulas.

There are also some cases where people write numbers such as 0.0289651159 with an implicit unit (I assume you get it Francesco).

@HansOlsson
Copy link
Collaborator

It seems like this proposal has a similar shortcoming as in #3257 when it comes to allowing for connector variable unit inference. I think both proposals should to be modified to not rule out such unit inference.

For example, I expect that the literal in the following model is expected go get unit "1", even though u has unit "":

block Double
  Modelica.Blocks.Interfaces.RealInput u;
  Modelica.Blocks.Interfaces.RealOutput y;
equation
  y = 2 * u;
end Double;

I would say that it isn't clear how much of a short-coming it is. We could also write it as model Double=Gain(final k=2); and we recently removed the k.unit="1", modelica/ModelicaStandardLibrary#3881 and I wouldn't be surprised that some use k with a literal value and a non-1 unit.

Separating integers and reals seems tempting for 2 and 2.0, but 101325 and 299792458 are also integers.

@henrikt-ma
Copy link
Collaborator

My main concern is that we seem to have a number of models where numbers are assumed to have a unit, e.g. Modelica.Electrical.Batteries.Examples.BatteryDischargeCharge where Ri=cellData1.OCVmax/1200 (the 1200 is assumedly a current), or Modelica.Electrical.Machines.Utilities.ParameterRecords.IM_SquirrelCageData, and all of the Modelica.Electrical.Spice3.Internal.Mos formulas.

I find it concerning that the MSL contains such formulas. I think it is the job of the specification to point of the need for 1200 to get a proper unit.

Clearly, we need to introduce unit checking in the specification with some sort of transition in mind. The fact that the specification hasn't said anything about unit errors so far means that introducing unit checking should be expected to be a backwards incompatible change. For a smooth transition into a unit-correct world, I think we should count on tools mitigating the effects of the backwards compatibility break. For example, a tool could have a non-strict unit checking mode, where unit errors are diagnosed as warnings. Exactly how to do this for an acceptable user experience should be up to the tools, in my opinion; the specification should call an error by its real name.

@henrikt-ma
Copy link
Collaborator

I would say that it isn't clear how much of a short-coming it is. We could also write it as model Double=Gain(final k=2); and we recently removed the k.unit="1", modelica/ModelicaStandardLibrary#3881 and I wouldn't be surprised that some use k with a literal value and a non-1 unit.

My expectation of the Double block would correspond to Gain(final k(unit = "1") = 2). If I wanted a non-unit-preserving relation between input and output, I probably wouldn't have called the block "Double".

I doubt that there's any sensible applications for a Double-like block that without modifying the unit of the gain allows any combination of units on the input and output. In other words, I expect any Double-like block to relate input and output units via some particular unit for the gain. To this end:

With this approach, Gain(final k=2) would actually be equivalent to Gain(final k(unit = "1") = 2) for purposes of unit checking, and it would just be a matter of taste whether to make the "1" explicit or implicit.

@casella
Copy link
Collaborator Author

casella commented Oct 26, 2022

It seems like this proposal has a similar shortcoming as in #3257 when it comes to allowing for connector variable unit inference. I think both proposals should to be modified to not rule out such unit inference.

The goal of this proposal is just to expand the scope of dimensional consistency checking. Unit inference is another story.

@casella
Copy link
Collaborator Author

casella commented Oct 26, 2022

My main concern is that we seem to have a number of models where numbers are assumed to have a unit, e.g. Modelica.Electrical.Batteries.Examples.BatteryDischargeCharge where Ri=cellData1.OCVmax/1200 (the 1200 is assumedly a current), or Modelica.Electrical.Machines.Utilities.ParameterRecords.IM_SquirrelCageData

Hans, I fully understand your concerns. As far as I am concerned, I find those expressions a bit questionable. You write "the 1200 is assumedly a current". I agree with the assumption, but if the model was written as

...
constant SI.Current i0 = 1200;
...
  Ri=cellData1.OCVmax/i0);

it would have been much clearer, and you wouldn't have had to assume anything. This is even more true for Modelica.Electrical.Machines.Utilities.ParameterRecords.IM_SquirrelCageData: I find

  parameter SI.Inductance Lm=3*sqrt(1 - 0.0667)/(2*pi*
      fsNominal) "Stator main field inductance per phase";

a bit fishy. I mean, the unit of inductance is "H", i.e. "V.s/A". On the RHS I see a term 1/(2*pi*fsNominal) which has a unit "s". I would then guess that 3 means 3 Ohm and sqrt(1 - 0.06667) is some dimensionless correction factor. But again, why not making this explicit as

  constant SI.Resistance R0 = 3;
  parameter SI.Inductance Lm=R0*sqrt(1 - 0.0667)/(2*pi*fsNominal) "Stator main field inductance per phase";

which could be positively confirmed to be dimensionally kosher if we introduce this proposal in the language spec? I think we can make this argument with @AHaumer and @christiankral and possibly rewrite these modifiers in a more unit-friendly way.

In any case, this may be considered as a matter of taste or style, but there is no need to argue about that. My point is different.

The language specification doesn't say anything at all about dimensional consistency in the normative part, even with my proposed changes. Hence, a negative outcome of dimensional consistency checking should obviously result in a warning, not an error. As it does in the tools I know best.

The question is: do we prefer to get some "false positive" warnings, such as dimensional inconsistency warnings from the above-mentioned examples, but also to catch plain wrong equations such as v = sqrt(2*g) when writing new models, or do we prefer not to get those false positives, at the price of not getting any warning about plain wrong equations?

As a modeller, I have no doubts: if the price to pay to catch plain wrong equations that would lead to bogus results is to get some false positives, that can easily be dismissed by inspecting the corresponding lines of code, I'm ready to pay it.

and all of the Modelica.Electrical.Spice3.Internal.Mos formulas.

Those models are just a 1:1 transposition of Fortran code, which of course had no concept of unit. They are deliberately confined to an "Internal" package. I don't think anybody would be surprised or annoyed if you get some unit consistency warnings when checking them.

There are also some cases where people write numbers such as 0.0289651159 with an implicit unit (I assume you get it Francesco).

I get it. Let them get a warning, if they know what they're doing they can simply ignore it. If they really don't want to see those warnings, they are free to define constants with proper units and use them instead, which I personally see as a much more elegant and clear modelling style.

Based on my experience, I am a lot more worried about accidentally writing a wrong model and not being warned about it. Happened to me and my co-workers twice already in the last 3 years. The consequences are a lot worse in this case.

@casella
Copy link
Collaborator Author

casella commented Oct 26, 2022

Clearly, we need to introduce unit checking in the specification with some sort of transition in mind.

@henrikt-ma I'm not at all sure about this. Personally, I don't think there is any need to be this strict.

In any case, we are straying away from the scope of this PR again. This PR is not aimed at introducing formal strict unit checking, not even to pave the way for it. As I said, I don't think there's any need of that. This PR has the much humbler goal of allowing to generate warnings for people that accidentally write wrong equations that are not caught by dimensional consistency checking because they contain some dimensionless numerical factor. That's it.

The fact that the specification hasn't said anything about unit errors so far means that introducing unit checking should be expected to be a backwards incompatible change. For a smooth transition into a unit-correct world, I think we should count on tools mitigating the effects of the backwards compatibility break. For example, a tool could have a non-strict unit checking mode, where unit errors are diagnosed as warnings. Exactly how to do this for an acceptable user experience should be up to the tools, in my opinion; the specification should call an error by its real name.

@henrikt-ma, AFAIK at the moment you are the only one proposing to formally introduce unit checking in modelica 😅.

From an end-user perspective, I see no need to do that, and I'm not seeing other people pushing for this. Why should we bother to introduce non-backwards compatible changes that nobody's asking for? Besides, we'd end up debating endlessly about hotly debated issues such as: is "rad" a base unit?

I'm just trying to improve non-normative dimensional consistency checking for equations containing non-dimensional factors and, yes, to slightly discourage people from mixing variables with units and numbers-that-are-supposed-to-have-some-unit in the same expression, which I find a bit lousy, by getting them some warnings when checking their models. Warnings that they can happily ignore, if they know what they're doing. No big deal.

@christiankral
Copy link

This is even more true for Modelica.Electrical.Machines.Utilities.ParameterRecords.IM_SquirrelCageData: I find

  parameter SI.Inductance Lm=3*sqrt(1 - 0.0667)/(2*pi*
      fsNominal) "Stator main field inductance per phase";

a bit fishy.

I very much agree, that the caclculation of the default machine parameters is neither intuitive nor formally correct.

The calculation is a consequence of a machine reference impedance ZRef = 1 Ohm = VRef / IRef. This reference impedance is in turn a result of the reference phase voltage VRef = 100 V and the reference current IRef = 100 A. As neither the reference voltage VRef nor the reference current IRef are parameters declared in either machine model, ZRef could at least be used as an internal (protected) constant to calculate the inductances and resistances with consistent units.

parameter SI.Inductance Lm=3*ZRef*sqrt(1 - 0.0667)/(2*pi*
      fsNominal) "Stator main field inductance per phase";

The induction machine documentation reads:

image

@henrikt-ma
Copy link
Collaborator

@henrikt-ma, AFAIK at the moment you are the only one proposing to formally introduce unit checking in modelica 😅.

If we are not aiming at formalizing unit checking in the specification, I don't see the point of MCP-0027. If all you care about is a tool-specific way of catching certain unit errors, just ask your favorite tool vendor to solve this in a tool specific way, but don't expect your libraries to pass unit checking in other tools, and don't expect that libraries developed with other tools will play nicely with the unit checking in your tool of choice.

No, we must keep the long term goal of Modelica code portability between tools in mind here, and our community would be right to demand of the specification that it lays down unit checking rules that make the Modelica library ecosystem reasonably free of unit errors. For this to happen, tools need to reject unit errors with support in the specification, and tools must not reject use of units that is valid according to the specification. (Where there is a gap in the specification, a tool might opt for a warning if it doesn't like of units are used.)

From an end-user perspective, I see no need to do that, and I'm not seeing other people pushing for this. Why should we bother to introduce non-backwards compatible changes that nobody's asking for?

I have always had the other impression: our users find it very strange that there's a formal syntax for how to express units, but no rules for how to check them.

Besides, we'd end up debating endlessly about hotly debated issues such as: is "rad" a base unit?

I don't deny that this is a problem, and therefore I think it is important that we don't close too many doors as we set out on this endeavor.

I'm just trying to improve non-normative dimensional consistency checking for equations containing non-dimensional factors and, yes, to slightly discourage people from mixing variables with units and numbers-that-are-supposed-to-have-some-unit in the same expression, which I find a bit lousy, by getting them some warnings when checking their models. Warnings that they can happily ignore, if they know what they're doing. No big deal.

I, on the other hand, want to make sure we don't introduce some ad-hoc rules that will not fit in the long-term development of a formal system for unit checking. I don't think it helps making them non-normative at this point, as it would be weird for tools to ignore the only rule we have about unit checking.

Co-authored-by: Henrik Tidefelt <[email protected]>
@casella
Copy link
Collaborator Author

casella commented Oct 27, 2022

If we are not aiming at formalizing unit checking in the specification, I don't see the point of MCP-0027. If all you care about is a tool-specific way of catching certain unit errors, just ask your favorite tool vendor to solve this in a tool specific way

Of course I could ask the developers of omc to implement my proposal without going to the hassle of have it passed into the Modelica Specification. But that's not my intent here. I don't want this feature to be tool-specific, I want this to hold for all tools, and I want all people that write Modelica code to be aware of it and to expect it to be used by tools. I also want to make sure I'm not missing something, so I'm actually seeking the feedback and discussion of the MAP-LANG group to make the proposal as good as possible.

What I don't want to do now is to introduce a complete formal type-checking handling of units. Why? Because it won't be backwards compatible, so it will trigger endless discussions, and because it will trigger even more discussions because it's tricky (see the is-rad-a-base-unit thread). I am fine with whatever method tools implement to warn me about dimensionally inconsistent equations, I don't see any need to go further than what we have now in the specification.

Except for one tiny detail: the current specification implies that the unit of literal constants is the default unit of Real, i.e. "", which makes supposedly dimensionless factors act as dimensional wildcards. So, with the current MLS, tools will never catch dimensionally inconsistent equations as soon as they include some literal constant, no matter how smart they are. Unless they make some assumption which are unfortunately not stated in the MLS and are thus questionable, because they would be tool-specific, not Modelica-specific. So I'd like to improve that, by adding a normative rule about giving the right unit attribute to Real literals. This is not a tool-specific issue, it is rather a language feature. I want modellers to be aware of that, and tool implementors to exploit that. As with all things Modelica.

That said I'm fine with the technicalities of unit checking being left to tool implementors. I assume they can do a good job, exactly in the same way I assume they can do a good job at solving equations correctly and efficiently.

but don't expect your libraries to pass unit checking in other tools, and don't expect that libraries developed with other tools will play nicely with the unit checking in your tool of choice.

That's precisely why I want this rule about units of literals to be part of the specification. To avoid the possibility that different tools make different assumptions about it, resulting in non-portable behaviour. That's been precisely the point of MCP 0027 since its inception, some years ago 😅

I have always had the other impression: our users find it very strange that there's a formal syntax for how to express units, but no rules for how to check them.

There are also no rules on how to solve equations in the MLS, which one may find very strange, given that all tools actually do that. Should we put that in the specification as well?

I, on the other hand, want to make sure we don't introduce some ad-hoc rules that will not fit in the long-term development of a formal system for unit checking.

As far as I understand, my proposal (the normative part) doesn't do that, but maybe I'm missing something. Can you point out one or two concrete examples, where you show that my proposal would be incompatible with yours?

I don't think it helps making them non-normative at this point, as it would be weird for tools to ignore the only rule we have about unit checking.

The non-normative part in this PR is just to explain the rationale. What is important is the normative part, as usual.

chapters/lexicalstructure.tex Outdated Show resolved Hide resolved
chapters/lexicalstructure.tex Outdated Show resolved Hide resolved
@HansOlsson
Copy link
Collaborator

I agree with this goal, and find this proposal good in itself. However, my main concern isn't about the language.

Unit checking (especially using this proposal) will not only generate the desired unit-warnings, but also unit-warnings from used libraries - like MSL (and others).

With modelica/ModelicaStandardLibrary#4041 other unit-errors are eliminated in MSL
And with modelica/ModelicaStandardLibrary#4051 also in ModelicaTest

However, adding units of literals as proposed here will generate about 1MB of warnings for MSL, so not only modelica/ModelicaStandardLibrary#4050 but more.

Do we have the resources to handle that? Note that some of them can be corrected in a straightforward way, but others require more - and we have already noticed that some of the changes intended to handle this have been incorrect, later corrected in modelica/ModelicaStandardLibrary@cf30cb7

\item The result of \lstinline!x + L!, \lstinline!L + x\lstinline!, \lstinline!x - L!, \lstinline!L - x!, \lstinline!x*L!, \lstinline!L*x!, \lstinline!x/L!, where \lstinline!x! is an expression with non-empty \lstinline!unit! attribute string `<s>` and \lstinline!L! is an expression containing only literal constants, shall have the same \lstinline!unit! attribute string of \lstinline!x!.
\item The result of \lstinline!L/x\lstinline! shall have the \lstinline!unit! attribute string `1/(<s>)`.
\item The result of \lstinline!x^L! shall have the \lstinline!unit! attribute string of \lstinline!product(fill(x, L))! if L is a positive Integer, or the unit of \lstinline!1/product(fill(x, L))! if L is a negative Integer.
\item If either side of a relational operator is a literal constant, then it is assumed to have the same \lstinline!unit! attribute string of the other side, if that is well-defined.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggest "If either side of a relational operator is an expression containing only literal constants" to mirror the formulation in rule 1. Otherwise T > (5+3) does not match this rule.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unless we find something better than "expression containing only literal constants", that is 😅

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Of course. But step 1 is to use a consistent formulation in all rules, to then update it in step 2. :-)

@bilderbuchi
Copy link

BTW, all these test cases we are collecting along the way seem really useful. Are those put to use somewhere? ModelicaTest?

@bilderbuchi
Copy link

In the course of searching for an improved formulation (nearly there), I realised that we seem to not have specified the unit-checking behaviour of the equality/assignment operator (10.6.1), i.e. how it deals with unitful, empty or undefined unit strings, which seems to make the proposal incomplete.

Is there a place in the spec that I am unaware of? If not, we have to add a rule for that, and will include that in my updated proposal.


The following rules apply:
\begin{itemize}
\item The result of \lstinline!x + L!, \lstinline!L + x\lstinline!, \lstinline!x - L!, \lstinline!L - x!, \lstinline!x*L!, \lstinline!L*x!, \lstinline!x/L!, where \lstinline!x! is an expression with non-empty \lstinline!unit! attribute string `<s>` and \lstinline!L! is an expression containing only literal constants, shall have the same \lstinline!unit! attribute string of \lstinline!x!.
Copy link

@bilderbuchi bilderbuchi Dec 15, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have a proposal to resolve the distinction between built-in (exp()) and other (specificEnthalpy()) functions. In effect, we have to replace "expression containing only literal constants" with "expression containing only literal constants and mathematical operations".
Because there's some context to write up around this, see the separate gist https://gist.github.com/bilderbuchi/317bc1a2e039f477462a61f5826260ea

I also collected all the test cases I could find so far in one place, so we could cross-check against them (and maybe add to a test suite later -- ModelicaTest?): https://gist.github.com/bilderbuchi/317bc1a2e039f477462a61f5826260ea#file-mcp-0027-test-examples-md

I started a new discussion thread because the previous one grew huge and hard to view.
Feedback welcome!

Copy link

@bilderbuchi bilderbuchi Jan 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@casella I'd like to hear thoughts on this approach (BB2a, BB2b, respectively) to express the distinction between builtin and other functions?

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@HansOlsson @henrikt-ma @casella it would be great to get your feedback on my comment https://github.com/modelica/ModelicaSpecification/pull/3266/files#r1049500278 with a proposed approach to resolve the distinction between built-in (exp()) and other (specificEnthalpy()) functions, and hopefully make progress on this PR. :-)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe that built-in functions should be treated uniformly with other functions as much as possible, and we need to distinguish it in some other way. Specifically specificEnthalphy is a function where the interface-variables have non-empty units, and that should be preserved. Note that some built-in functions have unit (specifically for Angles) in Modelica.Math, which is kind of identical to having unit="1".

So in one sense many built-in functions can be seen as having unit="1" meaning that we can limit literal-part to functions where the interface is without unit. However, having an interface for built-in functions will stumble on abs, sign, sqrt, atan2, etc where it makes more sense to say that the unit-handling is defined according to the mathematical rules.

Additionally for deriving units it makes sense that each function call is treated separately; so that if a user defined their own abs-function it is possible to have different units for each call. With such a rule we can just exclude function calls from the literal part; as x+myabs(2) will be a two-step procedure: myabs#1.input=2, x+myabs#1.output.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the prompt feedback!

I believe that built-in functions should be treated uniformly with other functions as much as possible, and we need to distinguish it in some other way.

This seems like a reasonable aspiration to me! However, I caution that, to get this proposal over the finish line, Francesco (IMO rightly so) relentlessly tries to limit the scope of the proposal to dealing with the "wildcard effect" of literals only. Therefore, a more uniform treatment should maybe be built out elsewhere/after this is merged?

So in one sense many built-in functions can be seen as having unit="1"

Logically/"in a sense" as you say, I agree, but is this specified already?

meaning that we can limit literal-part to functions where the interface is without unit. However, having an interface for built-in functions will stumble on abs, sign, sqrt, atan2, etc where it makes more sense to say that the unit-handling is defined according to the mathematical rules.

As the present challenge revolves around "literals+function calls" only (i.e. an "expression of type L"), I don't think the mathematical rules (e.g. relating input and output units of sqrt) do not come into play at all?
A couple of lines down in the present PR diff, those functions are specifically limited to "dimensionless" inputs.

Additionally for deriving units it makes sense that each function call is treated separately; so that if a user defined their own abs-function it is possible to have different units for each call.

I'm not sure what part of my proposal touches upon that (or precludes different units for different calls)? I'm confused.

I'm not aware (but I'm not a specialist on that) that such unit semantics (output unit == input unit) are expressible with current Modelica for non-built-in functions?

With such a rule we can just exclude function calls from the literal part; as x+myabs(2) will be a two-step procedure: myabs#1.input=2, x+myabs#1.output.

I think (but don't remember exactly anymore) this two-step procedure is basically the wider issue of composing an expression (and its ultimate unit) from a tree of sub-expressions (and their units), I think as mainly @henrikt-ma worked on. The present PR tries to deal with one type of expression only (resulting unit of an expression involving literals), not the general case.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No need to say sorry, I recognize your points myself. I understand that a conclave-style workshop would be preferable, but I'm not sure if such an approach is in the cards?

However, IIRC the way it seemed to me at least was that this proposal was near ~consensus (or readyness for review), and most conversation threads concluded. The main remaining item was I think to resolve the precision/scope of the "expression containing only literal constants" formulation, which I attempted again back in December with this Gist.

Copy link

@bilderbuchi bilderbuchi Jun 8, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW, I'm not even sure how could I actually read the current proposal. Is there a way to get this branch compiled into html or PDF?

The CI system compiles a PDF, you have to navigate to the build checks below, on the Jenkins page hit the "ARtifacts" button in the upper right, and download the pdf. In this case, this link: https://test.openmodelica.org/jenkins/job/ModelicaAssociation/job/ModelicaSpecification/job/PR-3266/23/artifact/MLS.pdf (page 13)
Pretty neat I have to say, hats off to the MA dev that set this up! :-)

Copy link

@bilderbuchi bilderbuchi Jun 8, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To summarize the situation hopefully more simply (from my point of view/recollection), and maybe spare you a re-read:

  • What we have already reached full consensus on right now is the desired behaviour of unit checking while avoiding the "wildcard effect", as codified in the set of unit-test-like examples that I collected from the discussions in one place here. If all else from this PR should be "lost", I hope that this set of examples is preserved to jump-start a future iteration on this topic.
  • What remains is to find out the/a minimal change to the spec that corresponds to that desired behaviour.
  • Your PR here is an attempt to formulate such a change.
  • The one thing your PR does not yet cover correctly is the last example in the section https://gist.github.com/bilderbuchi/317bc1a2e039f477462a61f5826260ea#proper-functions (as called out in that section).
  • My proposal update BB2a rectifies this deficiency AFAICT.
  • I'm asking if this proposal BB2a is acceptable in content/principle. If yes, I also ask if the refactored formulation BB2b, that streamlines the whole diff, is agreeable. I consider the second point optional if it turns out to be contentious.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As it was pointed out below in #3266 (comment), the language group is not ready to incorporate a solution to the wildcard effect in isolation. Instead, it seems that what we have learned in these discussions need to be carried over to a fresh start on unit checking where we try to break down the problem into smaller pieces, and where we in the end will be able to see the complete picture of unit checking before merging anything to the master branch.

Copy link

@bilderbuchi bilderbuchi Jun 12, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I missed this recent comment in the notifications/PR discussion, thank you for that update!
After a couple of months of mostly productive back-and-forth iteration, and half a year of inactivity, that certainly feels like a disappointing outcome to me.
One can only hope that, after having failed to achieve sufficient consensus on this minimized-scope problem, making the scope of the problem larger will enable achieving that consensus somehow. This sounds unintuitive to me 😅, but if this is the way this works, hopefully such a holistic perspective will succeed in unblocking things for the language group. 🤞

I hope that at least the list of test cases we all came up with together will be useful during these future discussions.

@henrikt-ma
Copy link
Collaborator

henrikt-ma commented Dec 15, 2022

In the course of searching for an improved formulation (nearly there), I realised that we seem to not have specified the unit-checking behaviour of the equality/assignment operator (10.6.1), i.e. how it deals with unitful, empty or undefined unit strings, which seems to make the proposal incomplete.

Is there a place in the spec that I am unaware of? If not, we have to add a rule for that, and will include that in my updated proposal.

No, you haven't missed it. This is why it is so difficult to solve the problem of literals in isolation; we must avoid specifying things about the literals without having an idea of how the solution would fit into a more complete picture of unit checking in the future.

I hope that there will be a substantial session on unit checking during the upcoming design meeting next year, so that we'll be able to take a step back and think more about the bigger picture. We need to seek language group (and others, like the MAP-Lib would of course also be most welcome to join) consensus about what we want to get out of the units in Modelica in the end, and a more longterm roadmap where this question about literals should be just one of several sub-problems we need to solve along the way.

@casella
Copy link
Collaborator Author

casella commented Dec 15, 2022

I'm all in for the big discussion. But in the meantime, I'd like to get a warning on v = sqrt(2*h) being wrong, without compromising future improvements.

Seems like I'm not going to get that, after all 😞

@casella
Copy link
Collaborator Author

casella commented Dec 15, 2022

In the course of searching for an improved formulation (nearly there), I realised that we seem to not have specified the unit-checking behaviour of the equality/assignment operator (10.6.1), i.e. how it deals with unitful, empty or undefined unit strings, which seems to make the proposal incomplete.

Is there a place in the spec that I am unaware of? If not, we have to add a rule for that, and will include that in my updated proposal.

The implicit assumption I was making was that <expr1> = <expr2> is wrong if both sides have a unit, and they are different. Otherwise you can't say anything, and that's it.

Seemed pretty obvious to me, but we can make it more explicit and add it to the proposal. However, it seems to me that this goes into the direction of putting implementation directives for dimensional consistency checking in the specification, which I'd say is out of scope here.

@bilderbuchi, with this PR I'd only like to explicitly state that literal constants should not act as unit wildcards in some cases where this is clearly inappropriate and can lead to missing gross mistakes. I'm not trying to specify how unit checking should be performed. I'll leave that to the ingenuity of tool vendors, exactly as we do with index reduction, tearing, solving nonlinear equations, integrating stiff ODEs, etc. No need to explain that in the language specification.

@bilderbuchi
Copy link

bilderbuchi commented Dec 16, 2022

@bilderbuchi, with this PR I'd only like to explicitly state that literal constants should not act as unit wildcards in some cases where this is clearly inappropriate and can lead to missing gross mistakes. I'm not trying to specify how unit checking should be performed. I'll leave that to the ingenuity of tool vendors, exactly as we do with index reduction, tearing, solving nonlinear equations, integrating stiff ODEs, etc. No need to explain that in the language specification.

OK. It's good then that I learned from past mistakes and made this part of my new proposal optional/removable from the get-go :D
I agree that the behaviour of assignment w.r.t unit checking follows common sense. I'm unsure how "far" to specify -- one person's "implicit assumption" may not be shared by everyone. I thought programming language specifications tend to err on the side of fewer "implicit" things, lest you have Undefined Behaviour everywhere.

@bilderbuchi
Copy link

bilderbuchi commented Dec 16, 2022

it seems to me that this goes into the direction of putting implementation directives for dimensional consistency checking in the specification, which I'd say is out of scope here.

I'm not sure how you arrive at this conclusion -- in my view specifying what happens when we encounter x = L (to borrow the lingo of this PR) is not materially different from specifying what happens when we encounter x + L, but I don't have a hard stance on including the equality treatment. We are still specifying behaviour (what), not implementation (how), don't you think?

@henrikt-ma
Copy link
Collaborator

OK. It's good then that I learned from past mistakes and made this part of my new proposal optional/removable from the get-go :D

I consider this a highly valuable aspect of the proposal, as I still have a strong desire for a specification of unit checking which is as tool-independent as type checking in Modelica.

@henrikt-ma
Copy link
Collaborator

I'm not sure how you arrive at this conclusion -- in my view specifying what happens when we encounter x = L (to borrow the lingo of this PR) is not materially different from specifying what happens when we encounter x + L, but I don't have a hard stance on including the equality treatment. We are still specifying behaviour (what), not implementation (how), don't you think?

I've pointed it out before, namely that a key difference between equality and summation is that equality only involves two expressions and therefore doesn't suffer from the (apparent, but still ever so important) associativity ambiguity of summation.

@henrikt-ma
Copy link
Collaborator

The general topic of unit checking was discussed in the language group phone meeting yesterday. We're planning to set up a better structure for addressing the many interdependent design problems, similar to how we have handled the complex MCP for Base Modelica. That is, we set up a structure where several smaller PRs can be targeted towards an MCP branch (or maybe we try a "Github project", whatever that means). This would allow us to first settle the general structure of unit checking without going into the details of exactly how the different operators, built-in functions, etc behave. Once the general structure is set, we can then have a smaller PR about the details of which expressions that may implicitly be given some other unit than "1".

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
MCP0027 Unit checking
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants