[adastra22]

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.

[kragen]

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'

[adastra22]

Yes, ok I agree with this.