Lambda the Ultimate

" length / length is dimensionless"

That is one of the things I've very often disagreed with, they aren't dimensionless, they are unit invariant. You can use the number in any unit system you want. But it's still arc-length / radius. To me that indicates a slight brokenness in how we deal with units. A unit is a vector, you have a property like distance, and a standard, like meters. When you apply the unit to something, the value is applied to the property, but not the measurement standard.

So 100 m/s x-axis / 200 m/s y-axis != .5 dimensionless. It's 0.5 x-axis (distance) / y-axis (distance)

A classic is saying Gc is 32.2 ft/s^2; It's not.

Let me elaborate a little more on what I mean by dimensions being arbitrary, because I think this example fits into that just fine. In a program that doesn't make use of dimensions we might have a variable vx that's the velocity of the ball along the x-axis in m/s. What happens when you introduce units into your language is that you reify part of that context. So we could now have vx is the velocity of the ball along the x-axis, in which case the 'm/s' bit is reified and belongs to vx. Or, we could go further and reify the 'along the x-axis' bit as well. That gets us the unit tags that you've suggested.

That might be useful or might be annoying. You'll have to explain why sqrt(vx^2 + vy^2) makes sense with your units. My point is that not having the extra reified context isn't wrong. Nor is the axis tag the only context you might want. If you're going to be multiplying by mass later to get momentum, you might want to reify "of the ball" so that you can check that you're multiplying by the mass "of the ball".

So there is no right or wrong here. It's a question of cost/benefit analysis. Reifying more context can avoid new classes of mistakes, but can also require annoying casts everywhere as you discard irrelevant context.

I think that's getting close to the issue. But here's another datapoint. Consider the scale of a map; perhaps I'm currently showing the map at 5 cm/km. You might say that value is dimensionless and unitless. But suppose the map is plotting low-level ozone concentration, which might at some point be 42 nmol/mol. That's also dimensionless and unitless. Now, whatever the justification might be for maintaining separate types for measures of distance (centimeters, say) and amount of ozone (nanomoles) should apply mutatis mutandis to the scaling factors. It is just as meaningless to add a centimeter to a nanomole as it would be to multiply a mole by 5 cm/km.

In your terms, the scaling factors must have reified the dimension to which they apply, so in some sense they do have dimensions even though they are unitless. (And even the unitlessness is debatable, since it would logically show up as a default output format.)

Isn't this just another case of wanting to reify more context? It sounds like you want the map dimensions to be (5 cm mcs / km wcs) where mcs is "map coordinate system" and wcs is "world coordinate system". Similarly, you want (42 nmol ozone / mol air). If all you reify is meters, then 5 cm / 1 km really does equal 0.00005.

Sure, I think I said that above. It's just reifying more context, if you like. Or it's modelling the world more precisely.

The question which strikes me as interesting about the scaling issue is that the (unitless) scale still has some sort of phantom dimension. That is, it suggests that length/length is not exactly the same as, say, count, because length/length is certainly not the same as volume/volume.

All of the dimensional modeling systems I've seen (including one I wrote, years ago) assume that you can just do simple dimensional analysis and add units, done. But after trying to write such a system, and looking at frink, I started to wonder if that is really true, or if dimensional modeling is just searching where the light happens to be shining. Ray Dillinger's radian/hertz example is another great example.

I must be growing old. I just remembered that I raised this exact issue quite a few years ago, right here on LtU.

My point is that I don't think these phantom dimensions exist with the original units. They only exist within the context that you're modeling with the units.

It is just as meaningless to add a centimeter to a nanomole as it would be to multiply a mole by 5 cm/km.

A pipe of uniform thickness is a kilometer long and contains a mole of some gas. How much gas is in 5 cm of that pipe?

You have an implicit conversion of length to volume in that question, so I don't regard it as a counter-example.

You could just as well ask about adding the length of pipe to a reservoir of 100 megalitres, but you'd still need to convert it to a volume if you were using dimensional types.

You could ask about applying the length scaling factor to the volume, but I'd argue that it shouldn't type-check either: it's ambiguous whether you're scaling just the length of the pipe (which is pretty well meaningless) or scaling each dimension of the reservoir (which is meaningful, but involves a cube).

You have an implicit conversion [...] so I don't regard it as a counter-example.

I think the reason you consider it incorrect to multiply a mole by 5 cm/km is because "5 cm/km" isn't a fully accurate description of the value you're considering. It isn't really the unitless scale you say it is. It's probably shorthand for 5 (cm on the map)/(km on the territory), and to take it at face value (0.00005) is an implicit conversion.

I took care to not make a firm claim about 5 cm/km being unitless, but that's a side issue. Certainly you are right that if the scaling factor retains/reifies both co-ordinate systems, as Matt M suggested, then I get my desired type error.

On the other hand, you can clearly go too far: I don't want to associate the scaling factor with a *specific* map (probably, I'd want the map to have-a scaling factor) because that would make it impossible to ask whether two maps have the same scaling factor. I don't even want the scaling factor to reify units, because I might have a model with multiple units.

For example, this lovely walk above the city of Zurich. (Sorry for not having an English version; it's a scale model of the solar system using a scaling factor of 1mm/1000km; both the distance between the sun and planets and their diameters -- but not their volumes -- are scaled by the same 10^-9, and a comment from the astronomer who designed the walk points out that this scaling makes the scaled speed of light 30 cm/sec, allowing us to stroll along the model at about twice the speed of light.)

Anyway, I'm happy to accept the premise that the way to make scaling factors work the way I think they should would be to explicitly reify the "axes", but I don't know how far that goes towards clarifying the semantics of a reified dimensional expression.

That is, if I have a scaling factor of 1 mm model / 1000 km solarSystem, I would expect the dimensional infrastructure to reduce that to 10^-9 (model length)/(solarSystem length), thereby deleting the units but not the dimension, and to be prepared to generate the equivalent 10^-27 (model volume)/(solarSystem volume). What sort of beast, then, is "model volume"? And is it model^3 length^3, or just model length^3? Or do I have to explicitly spell out the axioms of my 'ad hoc' dimensions/labels/whatever when I declare them?

As one more datapoint, there is little difference between a scaling factor and a unit conversion factor. Indeed, all the scaling factors I've mentioned in this discussion have included unit conversions. Strictly speaking, unit conversions don't normally change the canonical value of a dimensioned quantity, but in some systems, applying a unit conversion to a value may result in its default output format changing.

That is, if I have a scaling factor of 1 mm model / 1000 km solarSystem, I would expect the dimensional infrastructure to reduce that to 10^-9 (model length)/(solarSystem length), thereby deleting the units but not the dimension, and to be prepared to generate the equivalent 10^-27 (model volume)/(solarSystem volume). What sort of beast, then, is "model volume"? And is it model^3 length^3, or just model length^3? Or do I have to explicitly spell out the axioms of my 'ad hoc' dimensions/labels/whatever when I declare them?

For this particular example, I think the best answer would be that "Model Length" is an instantiation of the concept of Length. Volume being being cubic length would be a part of that concept and would come along for free. Note that you may or may not want to have the same units for those dimensions in this new system.

I don't want to associate the scaling factor with a *specific* map (probably, I'd want the map to have-a scaling factor) because that would make it impossible to ask whether two maps have the same scaling factor.

I didn't really understand this. Also, from your last paragraph, think we may be thinking of units a little differently. If you declare there to be three dimensions, World Length, Map1 Length, and Map2 Length, then values of those different dimensions are incomparable. The idea of a "scaling factor" doesn't make sense unless the map also exists at a specific size in the world, which it may not. For example, if the map is displayed on various size screens, then you don't have any fixed "scale factor". If you do have a conversion in mind (1 map inch / world inch), then you can just multiply by that conversion factor. There wouldn't have to be implicit conversion.

If three dimensions -- World Length, Map1 Length, Map2 Length -- are incommensurate, then so are the fractions Map1 Length / World Length and Map2 Length / World Length. This incommensurability prevents me from asking the question: "Is Map1 higher resolution than Map2?", which I think is meaningful even if the units of Map1 Length and Map2 Length are both pixels -- i.e. neither exists at a "specific size in the world" -- although I admit, I was thinking of maps and models which have a physical and not just luminous presence. Your intuition is undoubtedly more actualized than mine.

To compare them, convert to a common dimension like pixels or world inches. If you're assuming one world inch per map inch then multiply by that.

I took care to not make a firm claim about 5 cm/km being unitless, but that's a side issue.

Sorry, I didn't mean it was a firm claim. I was just targeting one half of the way you phrased "the (unitless) scale still has some sort of phantom dimension," trying to tip the ambivalence. :)

[...]impossible to ask whether two maps have the same scaling factor.

We could multiply or divide by a factor of 1 (map2 length)/(map1 length), which represents our ability to lay one map on another as a measuring tool.

Measuring a map with a map is a bit farfetched. Here's a slightly more practical example:

   20 (projected image length) in (hand lengths)
/ 0.5 (projector lens length) in (hand lengths)
-----
   40 (projected image length) in (projector lens lengths)

We may not be able to lay a projector lens on its projected image to do a comparison--at least not without changing the image we're trying to measure--but a mundane object in between can help. Usually(?) it's a dedicated measuring device, and we don't bother to mention it.

Back to the map example, the 1 (map2 length)/(map1 length) factor might not represent the fact that we physically use one map to measure the other, but that we can measure them both using the same measuring stick. Unlike the projector example, in this case we're going to measure distances on the maps' surface rather than currently assessing the maps' own overall size, so we're doing zero "measurements," and the resulting product has a coefficient of 1. Or something like that!

[...]I would expect the dimensional infrastructure to reduce that to 10^-9 (model length)/(solarSystem length), thereby deleting the units but not the dimension[...]

I agree with this. It shouldn't matter if we specify it as 10^-9 (model miles)/(solarSystem miles).

[...]and be prepared to generate the equivalent 10^-27 (model volume)/(solarSystem volume).

We could "generate" that manually by taking the cube of the scaling factor, but would it really make sense for the language to infer exponents? If the point is to highlight unit errors, this means we're letting certain errors slip by.

But if we want to take advantage of unit notation to do unit-directed computation, then it makes sense that we could set up ambient conversion factors and then apply several of them all at once with a cast. A length factor like this could apply multiple times, letting us convert volumes.

And is it model^3 length^3, or just model length^3?

If it were model^3 length^3 as though they were separate units, then we could start with 10^-9 (model length)/(solarSystem length) and get 10^-9 (model mass)/(solarSystem mass). So it isn't that.

I agree with this. It shouldn't matter if we specify it as 10^-9 (model miles)/(solarSystem miles).

Precisely. (unitless) but still not a scalar.

We could "generate" that manually by taking the cube of the scaling factor

Yes, that's what I meant. And if we simply cube the scaling factor, it should turn into volume scaling, just like cubing a distance turns into volume. So we should now be able to apply the cubed scaling factor to a volume.

pipeL = 1 km
pipeGas = 1 mol
segL = 5 cm
segGas = pipeGas * segL / pipeL -- Error:  Illegal sleight of hand

Seriously, though, I don't think you want an error there. This calculation is dimensionally and semantically correct. What would you write for line 4 instead? Are you saying we should bake into the language some assumption about moles being proportional to volume?

Construct a meaningful example for 1 mmol / mol + 5 cm / km ;-) Note the + not *.

You have two processes for producing a unit of a certain compound. The first process requires a mol of reagent and you have only 1 mmol. The second process requires a kilometer of cord and you have 5 cm. How many units of the compound can you produce?

Sorry to jump in, but I don't see how this is a counterexample. It was my understanding of your proposal that you want to require explicit multiplication by the (1 unit-of-end-product / mol) and (1 unit-of-end-product / km) scale factors that are implicit in the proposed problematic example?

Yes, but these scale factors cancel out in Matt's example? i.e. it doesn't force them to appear.

OK, sometimes a scaling factor is just a scaling factor. But please don't use map scales to dilute your medicines, ok? Sometimes the difference is important, too.

Specifically, in your example you're really computing:

volume of pipe = length * cross-section
moles in the pipe = (moles / volume) * volume of pipe
moles in the subpipe = moles in the pipe *
((subpipe length * subpipe cross-section) /
(pipe length * pipe cross-section))

The second of the computations is pipegas, if I understand you correctly. So it already had an implicit volume/volume phantom component (in my admittedly idiosyncratic terminology). The third one explicitly states that the cross-section is consistent for the subpipe. If you didn't put that in the code, you'd have to put it in a comment, because it's important.

Admittedly, I'd probably be annoyed about having to insert the cross-section twice (although it will be hypothetically be optimized away by the hypothetical compiler) but I can think of equally annoying things I've provided to real compilers in order to demonstrate my typesafe credentials.

is a perfectly good dimension, so you can add (units/resourceA) * (quantity of resourceA) + (units/resourceB) * (quantity of resourceB). In this case, the resource/resource really should disappear.

I honestly don't know what the answer to the question of when units should really cancel out, and when they should leave behind some trace; if it were an easy question, it wouldn't be worth talking about.

I haven't seen yet in this discussion the mention of the Buckingham Pi theorem. This proves how in any system of measurements that a certain number of measurements can be considered dimensionless, while the others must have some dimensions to be orthogonal. I see much of the discussion leading up to this, but no mention of the fundamental theorem.

My paper Abstraction and Invariance for Algebraically Indexed Types with Bob Atkey and Patricia Johann that I presented last week at POPL'13 considers this idea.

For a readable introduction to previous work on units-of-measure, including scale invariance, see Types for Units-of-Measure: Theory and Practice. You can try this for real in the F# programming language.

I haven't finished reading the paper in detail yet, but I certainly will. That's exactly what I was looking for and this would make my life so much easier! Do you have any thoughts on typing angular functions in this framework like cos, sin, complex exp?

This comes down to a mathematically very subtle question about "are radians angles or dimensionless?" I can give you many many mathematically deep arguments that radians are dimensionless. They are a length (around a circle) divided by a length.

In the case you mention before about torque and energy, the two are very closely related. A torque applied through an angle (measured in in radians) (again, radians are dimensionless) is exactly an energy, dimensionally and measurably. That is (torque*angle = energy) So the units are indeed conformal in a system where radians are dimensionless.

If you can come up with a system where radians are not dimensionless, it would be interesting. I'll give the example of the Taylor series for sin[x]. Try to work out the dimensions of a radian in the Taylor series where sin[x] = x - x^3/3! + x^5/5! - x^7/7! + ... You have to invent a system where x - x^3 works dimensionally. The only obvious solution is to make the radian dimensionless.

Hint: You cant add/subtract x and x^3 unless x is dimensionless.

Edit: fixed signs in Taylor series and wording to match.

If you define radians as length/length, then they're dimensionless. If you postulate a new dimension "angle" that has radians as a unit of measure, then they aren't dimensionless.

Mathematicians usually take the former approach, but I suspect the latter approach is superior for most everyday programmers using angles. The definition of sin by Taylor series in this system is then given by sin[x rad] = x - x^3/3! + x^5/5! - x^7/7! + ... + x^odd/odd! + ... with the only difference from your formula being the pattern match on x.

Let rad be a unit such that rad^2 = 1. Now sin x works!

I'm not saying that energy (or work) and torque aren't conformal: they are. What they aren't is mathematically interchangeable: a scalar is not a vector. IOW, conformality is not tantamount to interchangeability.

Doesn't this complaint prove too much? What if I have a Taylor series approximation to some function in my problem domain, f, that takes a distance and returns a mass? Won't I have the same dimensional problem?

I think this problem arises because the Taylor series coefficients were derived from a chain of derivatives, and the derivatives carried the units that would have canceled out with the units from the increasing powers of x. But it seems to me that this is the case regardless of whether we are talking about sin :: Radian -> Dimensionless or f :: Distance -> Mass.

The Taylor series is actually sin[x] = (1 rad^-1) x + (-1/3! rad^-3) x^3 + (1/5! rad^-5) x^5 + ... (modulo whatever operator precedence mistakes I made). At least I think it is consistent to see it that way, and potentially useful because angles as a statically tracked dimension really do prevent a lot of silly forgot-a-180-over-pi-someplace errors.

The Taylor series is actually sin[x] = (1 rad^-1) x + (-1/3! rad^-3) x^3 + (1/5! rad^-5) x^5 + ... (modulo whatever operator precedence mistakes I made).

In fact, I think that it is even more useful to view it as sin(x) = \sum_{i = 0}^\infty (-1)^i\prod_{j = 1}^{2i + 1} (x/(j rad)). I can't think of one off the top of my head, but I'm willing to bet that there is an interpretation of that formula (probably inclusion–exclusion flavoured; see http://www.cut-the-knot.org/arithmetic/combinatorics/CombinatorialPyth.shtml) that says something quite interesting about sines.

It is also not reasonable to assume that if two numbers have the same representation type, they are necessarily interchangeable. What type systems try to guarantee is always necessary, but never sufficient, to exclude the possibility of error.

That said, I think you've placed a finger on the pulse of what is capital-W Wrong with angles as being dimensionless.

Energy is scalar and Torque is vector, because Torque is constrained by a direction. And the constraint of direction is at the root of the difference between dimensionless and angular radians.

Radians are not just a ratio of lengths. They are a ratio of a length to a quantity that has a particular direction relative to that length. If the "length" along the arc was not curved in precise proportion to the length along the radius, then the ratio would not represent an angle. And while a distance can be characterized simply by its endpoints, a distance along an arc cannot be defined without reference to both its endpoints and its center of curvature. If you construct an arc around a different center point, you change the length of the arc just as surely as if you had constructed it with a different end point.

So one of these "lengths" has the usual meaning of absolute location-independent separation in space, and the other "length" has a different meaning of separation around some particular point of rotation. When you divide one by the other, the units ought not not cancel. When you multiply the quotient by a scalar, you get a vector not another scalar.

So ... what relationship does dimensional analysis indicate that the location of a point (the extra information needed to define the length of the arc) has to the definition of a rotational direction (the extra information needed to define the vector of torque)?

Ray

When you add angles that are defined in different planes, the convention is that means scalar addition.

This scalar/vector distinction is a red herring. Torques are vectors, but "torque magnitude", a scalar, is a useful concept in its own right, just as speed is useful as a scalar. In fact, when people say "torque" they often mean "torque magnitude". So, should torque magnitude be interchangeable with energy?

Radians are not just a ratio of lengths. They are a ratio of a length to a quantity that has a particular direction relative to that length. If the "length" along the arc was not curved in precise proportion to the length along the radius, then the ratio would not represent an angle. And while a distance can be characterized simply by its endpoints, a distance along an arc cannot be defined without reference to both its endpoints and its center of curvature. If you construct an arc around a different center point, you change the length of the arc just as surely as if you had constructed it with a different end point.

I think you'll have trouble formalizing anything coherent along this line of reasoning.