On Thu, 26 Aug 1999, Christian Sievers wrote:
> Anatoli Tubman wrote:
>
> > I once wrote a C++ template library that did exactly that. Arbitrary
> > units, rational exponents -- you can have (m^(3/2)/kg^(5/16))
> > dimensioned value. All at compile time, without runtime checking
> > whatsoever.
>
> Is there any sense physically in rational exponents?
Physically? Probably not much, other than if you get them, you might have
made a dimensional error (which could be caught, as you suggest below).
Well...actually, I take a bit of that back. There are occasional "rules
of thumb" that relate various physical quantities in "natural" situations.
So, for example, the speed of a fish is more or less proportional to the
square root of its length (assuming fish of some reasonably "fishy"
shape).
Other situations come up with "real" data where you're doing a regression
analysis (or something similar) and the limitations of the technique
require a data transformation in order for to you fulfill statistical
model assumptions. Not a pleasant business...
But in both cases it's not clear how (or that) you want to enforce
dimensional correctness.
> If not, we could use this extra information for less permissive type
> checking, for example only allowing a square root from an argument
> that has only even exponents.
And I can see that logarithmic data transformations are really going to
shake your world view. :-)
But getting back to Haskell (or functional programming), I did take a look
at the suggested Kennedy papers on "Dimension Types". Boy, does this
problem turn out to be subtle; I was in over my head in no time. But, in
addition to the solution he proposes there (which, by the way, would
handle the square root problem you mention), he discusses Wand and
O'Keefe's attempt to do a similar thing with an ML-like type system.
This is not as general, but might be good enough for some purposes. What
you do there is fix the number of base dimension at N and express
dimension types as N-tuples, so that if you had dimensions M, L, and T,
then Q (n1,n2,n3) represents [M^n1 L^n2 T^n3] in dimensional speak. The
"fun" here begins with things like sqrt which can have type Q (n1, n2, n3)
-> Q (.5*n1, .5*n2, .5*n3). Oh, and the type inference algorithm requires
Gaussian elimination.
jking
