Typed variables

[Happypig375]

The variables we have right now can represent a number or a statement. However, they will undergo incorrect replacement if they get substituted with a matrix as we assume commutativity and unified cross and dot products (they are the same as scalar product for scalars). In mathematics we would write vector variables with an arrow on top and matrix variables with bolded uppercase letters, so that they are distinguished from normal variables, with cross product and dot product operations enabled, but with commutativity and implicit invertibility disabled.

How we want to represent this nuance (and where we write the shape of the variable e.g. RR^2), and whether function variables fall into this proposal, are pending analysis by the agent.

Will we have a proper design that lets quaternions and more be considered correctly?

[Rafael-SOWNet]

Units as a test case for this design

A suggestion about the shape of the type rather than a feature request: whichever way this goes, it seems worth checking the design against physical dimensions, because they are the smallest thing that forces the type to be composable rather than a closed list of variable kinds.

The point is that a unit should probably not be another hard-coded kind sitting beside "vector" and "matrix". A scalar carries a dimension, and the operations derive the rest algebraically:

x : m        t : s
x / t : m/s
x * t : m·s
x + t        rejected — m ≠ s
x + 2 m      fine

Nothing has to enumerate Velocity, Force or Energy: L/T and M·L/T² already are those. What the type has to be able to express is a product of base symbols with integer exponents, plus rules for how +, *, /, ^ act on it — and the same machinery answers "sin, exp, ln want a dimensionless argument".

Two consequences that would be worth deciding early:

• Dimension is not unit. m, cm and km are one dimension with different scales, so conversion is a scale factor while dimensional agreement is the check. x + 2 cm is well-typed even though the numbers need converting; x + 2 s never is.
• It is orthogonal to shape. A quantity's dimension and its shape multiply rather than compete — a velocity vector is RR^3 and L/T. So what fits is a product of independent axes attached to a node, not one enum of variable kinds. That is also what keeps Codomain (a narrowing constraint on values) a third, separate axis from either of them.

That last point is why this belongs on this issue rather than its own. If the answer to "what does a variable carry" is a closed list (scalar | vector | matrix | function), then units can only be added later as a second closed list beside it, and quaternions as a third. If it is a small record of independent composable attributes, units become a consumer of the design instead of a fork of it — which makes them a fairly cheap test of whether the type system can express derived types at all.

There may also be something in it for the derivation/soundness side of #746: a dimension check is cheap, decidable and independent of values, so "the dimension of the result equals the dimension of what was matched" is a necessary condition any rewrite must preserve. A rule that breaks it is wrong whatever it was trying to do, and that is the kind of check that can be run over the rule sets mechanically rather than argued per rule.

For what it is worth this is not a hypothetical consumer: Docs/Usage/Comparison.md records physics / units as absent here and present in SymPy, where sympy.physics.units splits Dimension from unit in roughly the way above, and #717 lists it.

None of this is implemented and I am not proposing an API — the question for this issue is only whether the type a Variable carries should be composable enough that dimensions could be one of the things composed.

[Happypig375]

Units of measure would formally be quantity calculus. We'd need to handle separately units that don't support multiplication from those that do.