Ashley Yakeley after Tom Pledger:
The main complication is that the type system needs to deal with integer exponents of dimensions, if it's to do the job well.
Very occasionally non-integer or 'fractal' exponents of dimensions are useful. For instance, geographic coastlines can be measured in km ^ n, where 1 <= n < 2. This doesn't stop the CIA world factbook listing all coastline lengths in straight kilometres, however.
More unit weirdness occurs with logarithms. For instance, if y and x are distances, log (y/x) = log y - log x. Note that 'log x' is some number + log (metre). Strange, huh?
From the practical point of view they are very useful in order to avoid making silly programming errors, I have applied them several times while coding some computer algebra expressions. Dimensions were "just symbols", but with "reasonable" mathematical
When a week ago I mentioned those dollars difficult to multiply (although some people spend their lives doing it...), and some dimensional quantities which should have focalised some people attention on the differences between (*) and (+), I never thought the discussion would go so far. Dimensional quantities *are* a can of worms. properties (concerning (*) and (/)), so factorizing this symbolic part was an easy way to see whether I didn't produce some illegal combinations. Sometimes they are really "dimensionless" scaling factor! In TeX/MetaFont the units such as mm, cm, in etc. exist and function very nicely as conversion factor. W.L.I.III asks:
If you (or anyone else) could comment on what sorts of units would be appropriate for the result type of a logarithm operation, I'd be glad to hear it. I don't know what the result type of this example is supposed to be if the units of a number are encoded in the type.
Actually, the logarithm example would be consider as spurious by almost all "practical" mathematicians (e.g., physicists). A formula is sane if the argument of the logarithm is dimensionless (if in x/y both elements share the same dimension). Then adding and subtracting the same log(GHmSmurf) is irrelevant. == But in general mathematical physics (and in geometry which encompasses the major part of the former) there are some delicate issues, which sometimes involve fractality, and sometimes the necessity of "religious acts", such as the renormalization schemes in Quantum Field Theory. In this case we have the "dimensional transmutation" phenomenon: the gluon coupling constant which is dimensionless, acquires a dimension, and conditions the hadronic mass scale, i.e. the masses of elementary particles. [[[Yes, I know, you, serious comp. scist won't bother about it, but I will try anyway to tell you in two words why. A way of making a singular theory finite, is to put in on a discrete lattice which represent the phys. space. There is a dimensional object here: the lattice constant. Then you go to zero with it, in order to retrieve the physical space-time. When you reach this zero, you lose this constant, and this is one of the reasons why the theory explodes. So, it must be introduced elsewhere... In another words: a physical correlation length L between objects is finite. If the lattice constant c is finite, L=N*c. But if c goes to zero... Now, programming all this, Haskell or not, is another issue.]]] == Fractals are seen not only in geography, but everywhere, as Mandelbrot and his followers duly recognized. You will need them doing computations in colloid physics, in the galaxy statistics, and in the metabolism of human body [[if you think that your energy depenses are proportional to your volume, you are dead wrong, most interesting processes take place within membranes. You are much flatter than you think, folks, ladies included.]]. Actually, ALL THIS was one of major driving forces behind my interest in functional programming. I found an approach to programming which did not target "symbolic manipulations", but "normal computing", so it could be practically competiting against Fortran etc. Yet, it had a potential to deal in a serious, formal manner with the mathematical properties of the manipulated objects. That's why I suffer seeing random, ad hoc numerics. Björn Lisper mentions some approach to dimensions:
Andrew Kennedy has basically solved this for higher order languages with HM type inference. He made an extension of the ML type system with dimensional analysis a couple of years back. Sorry I don't have the references at hand but he had a paper in ESOP I think.
I think the real place for dimension and unit inference is in modelling languages, where you can specify physical systems through differential equations and simulate them numerically. Such languages are being increasingly used in the "real world" now.
ESOP '94. Andrew Kennedy: Dimension Types. 348-362. There are other articles: Jean Goubault. Inférence d'unités physiques en ML ; Mitchell Wand and Patrick O'Keefe. Automatic dimensional inference; and *hundreds* (literally) of papers within the Computer Algebra domain about dimensionful computations. I wouldn't say that the issue is "solved". !!!!!! There is MUCH MORE in modelling physical (or biologic or financial) world than just the differential equations. There is plenty of algebra involved, nad *here* the dimensional reasoning may be important. And such systems as Matlab/Simulink, etc. ignore the dimensions, although they have now some OO layer permitting to define something like them. Jerzy Karczmarczuk Caen, France