Applying Hindley-Milner to unit-checking

RationaleMCP/0027/HindleyMilner.md

@@ -0,0 +1,336 @@
+# Unit checking
+
+Unit checking is the process of inferring the units of Modelica variables, and ensuring the variables are used consistently in expressions and equations.
+
+It takes place after any evaluation of evaluable parameters and no evaluable parameters shall be evaluated during this process.
+(This must be true as long as tools allow the users to opt-out from unit-checking.)
+
+It is performed by using a type inference algorithm, albeit adapted to work with units.
+The algorithm proposed here is based on the Hindley-Milner algorithm.
+At a high level the algorithm collects a set of constraints on the units of expressions.
+It extracts a set of substitutions from these constraints which once applied determine whether a variable has a unit and what that unit would be.
+Any inconsistency discovered during this process is a unit error, and any unit expression that contains remaining unknowns at the end of the process is considered unknown.
+
+The document is organized as follows:
+* [Introduction of what is meant by the unit of a variable](#the-unit-of-a-modelica-variable)
+* [Description of the objects used in the inference algorithm](#unit-constraints-and-meta-expressions)
+* [Definition of unit equivalence and convertibility](#unit-equivalence-and-convertibility)
+* [Unit inference algorihtm](#unit-inference)
+* [Application to Modelica](#unit-constraints-of-a-modelica-model)
+* [Modelica operators on units](#modelica-operators-on-units)
+* [Extensions and limitations](#possible-extensions-and-current-limits)
+
+## The unit of a Modelica variable
+
+The unit of a Modelica variable is the unit associated with the variable after unit-checking has been performed, possibly remaining unknown.
+
+Note that the unit of a variable is not the same concept as the `unit`-attribute of the variable, but in a unit-consistent model, the unit will be equal to the `unit`-attribute when present.
+
+## Unit constraints and meta-expressions
+
+Unit constraints are introduced in the form of an [equivalence](#equivalence) of two unit _meta-expressions_.
+After an evaluation stage, a unit constraint of the form _`u1` is equivalent to `u2`_ will be represented by the _single-sided form_ `u1*u2^-1`.
+
+This section outlines the different constructs that comprise meta-expressions.
+
+### Variables
+The unit of the Modelica variable `var` is represented by the unit variable `var.unit`.
+These are unknowns for the inference algorithm to determine.
+
+### Literals
+
+#### `well-formed` unit
+The `well-formed` units correspond to [Modelica unit expressions](https://specification.modelica.org/master/unit-expressions.html).
+
+For the purposes of unit checking, they can be uniquely represented by their base unit factorization and scaling, up to the order of the base units.
+
+(We discuss why we ignore unit offsets later.)
+
+#### `empty` unit
+An expression with `empty` unit won't contribute to the unit of a parent expression, and will meet any constraints imposed on it.
+In practice, these are used to represent the unit of literal values.
+They provide a more flexible solution than considering any literal value to have unit `"1"`.
+They also provide a stricter solution than letting the unit of literals be inferred, which would effectively make literals wildcard from the perspective of the unit system.
+
+#### `undefined` unit
+An expression with `undefined` unit is used to represent unspecified or error cases, and will meet any constraints imposed on it.
+
+### Operators
+
+#### *
+Consider the meta-expression `e1 * e2`.
+* If both `e1` and `e2` are `well-formed`, it evaluates to a `well-formed` unit resulting from multiplying `e1` by `e2`.
+* If one of them is `empty`, it evaluates to the other one. (In effect, the `empty` unit becomes unit `"1"`)
+* If one of them is `undefined`, it evaluates to `undefined`.
+
+#### ^
+Consider the meta-expression `b ^ e`, where `e` is a rational.
+* If `b` is `well-formed`, it evaluates to a `well-formed` unit resulting from raising `b` to the power `e`.
+* If `b` is `empty`, it evaluates to `empty`.
+* If `b` is `undefined`, it evaluates to `undefined`.
+
+#### der
+Consider the meta-expression `der(e)`.
+* In a constraint where a `well-formed` unit is present, it evaluates to `e * ("s" ^ -1)`.
+* If `e` is `empty`, it evaluates to `empty`.
+* If `e` is `undefined`, it evaluates to `undefined`.
+
+This definition keeps `der(e)` in symbolic form in a model that does not contain any units.
+Otherwise, `der(x) = x` would lead to unit errors even if `x` has no declared unit.
+This also means that in `k*der(x) = -x`, the unit of `k` won't be inferred to be `"s"`.
+
+### Evaluation
+Unit variables can't be found to be `empty` or `undefined` unit.
+This means that after evaluation, a unit meta-expression is either `undefined`, `empty` or does not contain any `undefined` or `empty` unit.
+
+After evaluation a constraint will not contain both a well-formed unit and a `der` meta-expression.
+This means that all constraints can be simplified to have at most one well-formed unit.
+
+## Unit equivalence and convertibility
+
+### Equivalence
+Two well-formed units are said to be equivalent if both of the following are true:
+* Their base unit factorizations are equal.
+* Their base unit scalings are equal.
+
+Examples:
+- `"N"` and `"m/s2"` have different base unit factorizations, they are not equivalent.
+- `"s"` and `"ms"` have different base unit scaling, they are not equivalent.
+- `"K"` and `"degC"` are equivalent.
+- `"kN"` and `"W.s/mm"` are equivalent.
+
+It is a quality of implementation how equality of scalings are checked.
+
+`empty` units and `undefined` units are always equivalent to each other, themselves and any `well-formed` units.
+
+### Convertibility
+A well-formed unit `u1` is said to be convertible to another well-formed unit `u2` if:
+* Their base unit factorizations are equal.
+
+Examples:
+- `"N"` is not convertible to `"m/s2"`, since they have different base unit factorizations.
+- `"s"` is convertible to `"ms"`, since they differ by base unit scaling.
+- `"K"` is convertible to `"degC"`.
+- `"kN"` is convertible to `"W.s/mm"`.
+
+`empty` units and `undefined` units are never convertible to each other, themselves or any `well-formed` units.
+
+## Unit inference
+
+### Modified Hindley-Milner
+
+The original Hindley-Milner algorithm is designed to infer types, and consists of building a set of substitutions that returns the type of any expression of a given program.
+Applying this algorithm to perform unit inference in Modelica comes with two important differences:
+  * Not all variables must have a unit in a given model.
+  * There are operations on meta-expressions, that is, not all constraints are of the form  _`var1.unit` is equivalent to `var2.unit`_.
+
+#### Solvability of constraints
+
+After meta-expression evaluation and gathering of variables in the single-sided form, a constraint's solvability can be determined using:
+* A set `V` of unit variables present with non-zero exponent.
+* A set `D` of unit variables, present inside a `der` meta-expression.
+
+With this information, a variable `var.unit` can be solved from a given constraint if:
+* `var.unit` is present in `V`, but not in `D`.
+
+If a constraint has such a variable, the constraint is solvable.
+
+#### Conditional constraints
+
+One notion that doesn't exist in the original Hindley-Milner algorithm is that of a conditional constraint.
+In Modelica, errors that are in unused part of a simulation model should typically be ignored (e.g., removed conditional components).
+In the context of unit inference, some Modelica constructs generate constraints that are predicated on certain expressions having been evaluated or not.
+The constraint conditions are conjunctive, in other words, if even a single condition evaluates to `false` the constraint should be discarded.
+
+#### The algorithm
+
+The Hindley-Milner algorithm modified to perform unit inference in Modelica:
+* Traverse the flattened equation system and collect constraints before any evaluation has occured.
+* After evaluable parameters have been evaluated, and expressions have been reduced to values when possible, evaluate the constraints, as well as their conditions. (This propagates `empty` and `undefined` units to the top of the constraints.)
+* Discard any constraints of the form _`u` must be equivalent to empty unit_, or _`u` must be equivalent to undefined unit_, as they are trivially satisfied.
+* Discard any constraints having at least a condition that was evaluated to `false`.
+* Represent all constraints in their single-sided form.
+* Start with an empty set `S` of substitutions.
+* Loop:
+    * Select a solvable constraint or one that can be checked, if no such constraint exists exit the loop.
+    * If the constaint is in the form of just a `well-formed` unit, check that it is equivalent to `"1"`, it is an error otherwise.
+    * If it can be solved for `var.unit`:
+        * Replace the constraint by the substitution _`var.unit` => `u`_, where `var.unit` is not present in `u`.
+        * Apply the substitution to the right-hand side of the substitutions already in `S`.
+        * Add the substitution to `S`.
+        * Apply the substitution to all remaining constraints.
+* The unit of a variable for which there is no substitution in `S` is unknown.
+* For a variable `var` that has a substitution `var.unit` => `u` in `S`:
+    * If `u` is a `well-formed` unit, then this is the unit of `var`. (Given that no unit errors have been detected, a variable with a `unit`-attribute will get the given unit.)
+    * Otherwise, the unit of `var` is unknown.
+
+## Unit constraints of a Modelica model
+
+The following rules describe the unit meta-expression of a given Modelica expression, where it makes sense.
+They also provide the constraints that arise from different Modelica constructs.
+
+When it is specified that _`u1` must be equivalent to `u2`_, the corresponding constraint should be collected.
+
+In this section, the unit meta-expression of expression `e` is called `e.unit` and conditions of conditional constraints are highlighted with [].
+
+### Variables
+If `var` has a declared `unit`-attribute, `var.unit` must be equivalent to it.
+
+`var.unit` must be equivalent to the unit of the following attributes if present:
+ * `start`
+ * `min`
+ * `max`
+ * `nominal`
+
+(`var.unit` should be convertible to the `displayUnit`-attribute of `var` if it is present, but there is no corresponding constraints for the unit inference.)
+
+Consider the expression `e` of the form `var`, where `var` is a Modelica variable.
+* If `var` doesn't have a declared unit attribute, and has constant component variablity, `e.unit` is the `empty` unit.
+* Otherwise, `e.unit` is `var.unit`.
+
+### Literals
+`Real` literals have `empty` unit.
+
+### Binary operations
+Consider an expression `e` of the form `e1 op e2`.
+
+#### Additive operators
+* `e.unit` must be equivalent to `e1.unit`.
+* `e.unit` must be equivalent to `e2.unit`.
+
+Note that this requires introducing an intermediate variable to represent `e.unit`.
+This allows unit propagation when one of the operand has `empty` unit.
+
+#### Multiplication
+`e.unit` is `e1.unit * e2.unit`.
+
+#### Division
+`e.unit` is `e1.unit * (e2.unit ^ -1)`.
+
+#### Relational operators
+`e1.unit` must be equivalent to `e2.unit`
+
+#### Power operator
+* `e.unit` must be equivalent to `e1.unit ^ e2`.
+* If [`e2` wasn't evaluated or is a `Real` expression], `e1.unit` must be equivalent to `"1"`.
+
+Note that this requires introducing an intermediate variable to represent `e.unit`.
+Technically, `e2` is a Modelica expression rather than a rational number, which means that `e1.unit ^ e2` cannot be represented as a unit meta-expression.
+In practice, if the condition of the second constraint is verified, `e1.unit ^ e2` is `"1"` and if it isn't verified, then it can be represented as a meta-expression.
+
+(If the exponent was not evaluated or is a `Real`, the unit of the base should be `"1"`.)
+(It is up for discussion, when `e2` is `Real`, whether `e2.unit` should be equivalent to `"1"`. It could be handled in a similar way as transcendental functions. See below.)
+
+### Function calls
+Consider the expression `e` of the form `f(e1, e2, …, en)`.
+* If the output of the function has a declared unit, `e.unit` is the declared unit.
+* `e.unit` is `undefined` otherwise.
+
+If function input `i` has a declared unit, `ei.unit` must be equivalent to this unit.
+
+The natural generalization to functions with multiple outputs applies.
+
+### Transcendental functions
+As examples of transcendental functions, consider `sin`, `sign`, and `atan2`.
+Other transcendental functions can be handled similarly.
+
+Consider expression `e` of the form `sin(e1)`.
+* If `e1.unit` is `empty`, then so is `e.unit`.
+* If `e1.unit` is not `empty`, then it must be equivalent to `"1"` and `e.unit` is `"1"`.
+
+Note that some of these constraints can only be processed once `e1.unit` has been determined.
+This avoids introducing a unit `"1"` in the inference algorithm.
+
+Implementation note: The rule above can be implemented as making `e.unit` equivalent to `e1.unit`, and if `e1.unit` is `well-formed` after completed unit inference, then verify that it is equivalent to `"1"`.
+
+Consider an expression `e` of the form `sign(e1)`.
+* If `e1.unit` is `empty`, then so is `e.unit`.
+* If `e1.unit` is not `empty`, then `e.unit` is `"1"`.
+
+Consider an expression `e` of the form `atan2(e1, e2)`.
+* If `e1.unit` must be equivalent to `e2.unit`.
+* If `e1.unit` or `e2.unit` is `undefined`, then so is `e.unit`.
+* If `e1.unit` and `e2.unit` are `empty`, then so is `e.unit`.
+* If `e1.unit` or `e2.unit` is not `empty`, then `e.unit` is `"1"`.
+
+Implementation note: The rule above can be implemented as making `e.unit` equivalent to both `e1.unit * e1.unit^-1` and `e2.unit * e2.unit^-1`.
+
+### Operator der
+The unit of the expression `der(e)` is `der(e.unit)`.
+
+### If-expressions
+Consider the expression `e` of the form `if cond then e1 else e2`.
+If [`cond` was not evaluated]:
+* `e.unit` must be equivalent to `e1.unit`.
+* `e.unit` must be equivalent to `e2.unit`.
+
+If [`cond` was evaluated], `e.unit` must be equivalent to the unit of the selected branch.
+
+Note that this requires introducing a intermediate variable to represent `e.unit`.
+
+### Equations
+Both sides of binding equations, equality equations and connect equations must be unit equivalent.
+
+## Modelica operators on units
+
+The following operators facilitate writing unit-consistent models.
+
+### `withUnit($value$, $unit$)`
+Creates an expression with unit `$unit$`, and value `$value$`.
+Argument $value$ needs to be a `Real` expression, with `empty` unit.
+
+One application of this operator is to attach a unit to a literal.
+
+### `withoutUnit($value$, $unit$)`
+Creates an expression with empty unit, whose value is the numerical value of `$value$` expressed in `$unit$`.
+Argument `$value$` needs to be a `Real` expression, with a well-formed unit.
+The unit of `$value$` must be convertible to `$unit$`.
+
+### `inUnit($value$, $unit$)`
+Creates an expression with unit `$unit$`, whose value is the conversion of `$value$` to `$unit$`.
+Argument `$value$` needs to be a `Real` expression, with a well-formed unit.
+The unit of `$value$` must be convertible to `$unit$`.
+
+## Possible extensions and current limits
+
+### Units with offset
+The current proposal doesn't allow distinguishing `"K"` and `"degC"`.
+In order to do that one needs to keep track of whether a variable is meant to represent a difference or not.
+We have a proof of concept for such a feature, and the mechanism is similar and orthogonal to the one described here.
+
+### Builtin operators and functions
+The current state of this proposal does not cover the unit checking of all Modelica builtin operators and functions.
+
+### Arrays
+We don't try to specify how this would work on arrays, although the current proposal works straight-forwardly with element-wise operators.
+We are confident that it could be extended to matrix computations too, but haven't a proof of concept for that part.
+
+### Constants
+This proposal takes a stance regarding how the unit of constants should be handled but we recognise that this is still very much up for discussion.
+It is also somewhat orthogonal to the rest of the proposal.
+
+### Functions
+The Hindler-Milner algorithm provides a way to infer unit attributes of the inputs and outputs of functions.
+Concretely, it would imply computing the bundles of constraints from the body of each functions and adding them to the algorithm, after adequate substitutions, when processing a function call.
+
+### Variable initialisation pattern
+A common pattern used in the MSL is the following:
+```
+model M
+  Real d(unit = "s") = 12;
+  Real v(unit = "m/s") = 0.1 / (3 * d);
+end M;
+```
+where a modeler knows how to express a variable with unit as a function of another, with help of literal values that should really carry a unit.
+The way to fix that, with this proposal, is to attach a unit to the literal values using `withUnit`.
+
+### Syntax extension
+We could extend the Modelica language to add syntactic sugar for `withUnit`.
+The following variants have all been successfully test implemented:
+* `0.1["m"]`
+* `0.1 'm'` (or as `0.1'm'` to show more clearly that the quoted unit belongs to the literal)
+* `0.1."m"`
+
+### unsafeUnit operator
+Another way to deal with the pattern described above would be to provide an unsafe operator that effectively drops any constraints generated in its subexpression.
+The whole expression would have `undefined` unit.

RationaleMCP/0027/ReadMe.md

@@ -0,0 +1,34 @@
+# Modelica Change Proposal MCP-0027<br/>Units of Literal Constants
+Francesco Casella, Henrik Tidefelt
+
+**(In Development)**
+
+## Summary
+The purpose of this MCP is to allow more unit errors to be detected by giving more expressions the unit `"1"` instead of having an undefined unit.
+The problem with undefined unit is that it gets in the way of carrying out checking of units (which tools tend to deal with by not checking units at all where this happens).
+
+## Revisions
+| Date | Description |
+| --- | --- |
+| 2022-10-04 | Henrik Tidefelt. Filling this document with initial content. |
+
+## Contributor License Agreement
+All authors of this MCP or their organizations have signed the "Modelica Contributor License Agreement".
+
+## Rationale
+FIXME
+
+## Backwards Compatibility
+As current Modelica doesn't clearly reject some models with non-sensical combination of units, this MCP will break backwards compatibility by turning at least some of these invalid.
+
+## Tool Implementation
+None, so far.
+
+### Experience with Prototype
+N/A
+
+## Required Patents
+To the best of our knowledge, there are no patents that would conflict with the incorporation of this MCP.
+
+## References
+(None.)