Hacker News new | ask | show | jobs
by kragen 948 days ago
the classic problem for such number systems is linear algebra https://yosefk.com/blog/can-your-static-type-system-handle-l...

the issue is that each column and each row of a matrix can have different units. worse, gauss-jordan elimination chooses which rows to operate on dynamically. there is eventually a solution to this problem in c++ far down the comments thread

i don't see anything in https://numbat.dev/doc/type-system.html about aggregate types such as vectors, matrices, maps, arrays, lists, trees, records, etc., though it does have a suggestively named scalar type. i wonder how it handles this sort of thing

2 comments

No, we do not have aggregate types in Numbat yet. But it is definitely something I would like to support.

Note that it is possible to construct a type system solution to this problem (vectors/matrices with non-uniform units). A colleague of mine has an excellent talk on this: https://www.youtube.com/watch?v=SLSTS-EvOx4

By 'Scalar', in the document you referenced, we mean a dimensionless quantity. Not a scalar in the scalar-vector-matrix-tensor sense. Maybe I should rethink that notation.

thanks, i'll take a look

i know it's possible (even in c++ apparently) but so far it seems difficult

Interesting article... though to be honest, I'm not sure I buy the premise.

In the article, he states: "Let's call the matrix of all (xi 1) `X` and let's call the vector of all yi `Y`", and then states that the units of `X` are (m 1).

But if you instead say the units of `X` are just m, the "1" is in units "m", then the problem goes away, the whole matrix has the same units ("m"), and everything works fine.

I'll be honest in that I've never thought of a matrix having multiple units per column... and I can't think of any example where you aren't just putting the units in the wrong place. Let me know if you have a concrete example that might work.

If you multiply by a transform where the first entry is 1, the second entry is d/dx, the third entry is d^2/dx^2, etc. You will get a different unit for each entry of the vector.

Also most of economics consists of linear systems with non homogeneous units. The first entry could be bushels of wheat, the next demand for steel, etc.

One way to think of this is that there are always multiple ways to break up the units when moving a system of equations into matrix form. What I’m trying to say is that there is always one way to break up the units that leads to matrices and vectors with a consistent unit.

Transform vectors like you mentioned can have an implicit 1 with the right units in them in order to make the vector have a consistent unit.

> Also most of economics consists of linear systems with non homogeneous units.

The system of equations needs to have some sort of unit consistency. Which means there is some way to split up the units to keep the matrices and vectors with consistent units or the math doesn’t actually make sense.

I don't understand the point you are making. These systems are intrinsically non-homogeneous in their typing.

In input-output analysis in economics, for example, the elements of a vector represent the amounts of a commodity (coal, steel, electricity, etc.), and the columns of the demand matrix represent how much of each commodity is required to produce one unit of that commodity as output. So the type of row 1 is "kg of coal", the type of row 2 is "kg of steel", the type of row 3 is "kJ of energy", etc. Given this matrix and a vector representing the starting quantities, you can do some linear algebra to get a matrix representing how much of each quantity to allocate to each sector, and a vector representing the resulting output. The type of these vectors are "[kg Coal, kg Steel, kJ electricity, ...]"

I don't now how you can "have an implicit 1 with the right units in them in order to make the vector have a consistent unit" given this setup.

being implicitly non-homogeneous doesn't mean they're logically intractable

you can still imagine some kind of static analysis that gives you an error if you accidentally write an algorithm that might add kgs of steel to kilojoules, and which is sufficiently powerful to accept at least the commonly-used numerical algorithms; not just matrix multiply but, in your example, probably the simplex algorithm

(we could call that analysis a 'type system', but perhaps obviously, it is significantly different from the type systems we're most familiar with)

i agree that this doesn't end up with vectors of homogeneous types, but it does end up with vectors of the correct type, which might be what was meant by 'consistent'

Yes, ok I agree with this.
> there is always one way to break up the units that leads to matrices and vectors with a consistent unit.

maybe i don't understand what you're saying but it sounds like you don't understand the problem

it's not that the units are inconsistent in the sense of adding kilograms to kilojoules; they're just inhomogeneous

you have a potentially large matrix in which potentially every cell has different units. so type systems that require the matrix cells to all be of the same type aren't helpful unless that type is something machine-oriented like `real*8`

moreover this is intrinsic to the problem, or at least the decision to use linear algebra on the problem

an additional difficulty for things like *gemm or lu factorization is that you want them to be applicable to matrices of any size with any type of units of measurement, as long as they're consistent; so they're parametrically polymorphic over units of measurement

i hadn't thought of it either before auditing an introductory numerical methods class, but in retrospect the page i linked does explain this, repeatedly, in the comments; i just didn't understand it at the time

basically it's very very common