Lambda the Ultimate

It looks to be doing pretty much the same thing, but using an external system to validate the correctness. The beauty of the C++ system is it's internal, i.e. it uses only the C++ compiler for verification.

It's true, the two systems have different aims. Osprey was designed to work on existing C code, and the utility of that decision might compensate for any perceived ugliness.

Osprey uses the Gaussian-elimination technique Tudor Antoniu and I
developed for spreadsheet unit inference in XeLda some time back.
There's more to that story that I've never written down ... someday.

I, for one, would be very interested in any additional references or writings you might have on this subject!

Huh? The first thing is exactly what they do. The second is easily accomplishable in both C++ and Haskell, and just about any language with abstraction capabilities.

[edit]
No, I'm wrong about the former; I just realized what you said. Luckily, the solution to the latter also works for the former.

However, is does not need to be complete to be helpful (though, that'd be nice). I can just as easily add a length and width on paper, and doing dimensional analysis accurately still won't help me but it is still helpful.

Well, actually there's nothing stopping you using this system to give length and width different dimensions. There's a whole world of multidimensional dimensional analysis (now there's a confusing term) that this technique can be applied to. Of course you'd only do this if your problem domain required it.

No it doesn't catch all errors. However it is very likely to catch the errors you are likely to make. It doesn't provide any kind of proof that your equations are correct (you're expected to do that yourself), but it will very probably show that you've typed them in correctly.

I might point to a previous Fortress discussion here where we discussed some of the things that dimensional analysis can and can't check easily, about ambiguities when mapping common usage of units of measure into unambiguous, computer-parseable syntax, about weirdnesses in expected order of operation when manipulating units, about following the rules of the International System of Units (SI) for writing and parsing units, etc.

There's another discussion where we discuss some of the design issues and unexpected behaviors introduced by Fortress and the Google calculator that try to perform "do what I mean" fixups that don't follow standard mathematical notation or precedence.

That looks like quote from my documentation! :)

Yes, Frink does track units of measure through all calculations. Every single function and mathematical operator in Frink is units-aware, and can handle units of measure any place you can have a number. Frink programs are expected to contain their units of measure explicitly, and the language makes sure that dimensions are tracked properly and units are mixed transparently. Of course, not every case makes sense, like taking sin[3 days], in which Frink will generate an error.

Frink is also intended to follow standard mathematical notation when possible, and to make using units of measure as transparent as possible, that is, to follow standard orthography (as compared to, say, Mathematica, which makes you write Kilo Meter when you mean kilometer or km.)

Frink also validates that units of measure are conformal as soon as possible at runtime. For example, adding 1 foot + 1 meter works fine, but 1 foot + 1 day fails immediately. (Compare this again to Mathematica, which will let you add them and not flag an error until you try to convert them to other units.)

It also contains a large standard data file of common (and uncommon) units of measure and information about things like planets, subatomic particles, fundamental constants of the universe, elements, etc., to allow you to do most calculations without digging up reference books, or remembering how many joules are in a calorie, or look up the current value of Planck's constant.

All of this is checked at run-time, not compile-time.

You can look at some of Frink's sample calculations to give you an idea of what calculations look like.

For example, if a function takes as argument a length, and returns a length, and there are no other dimensionful values involved, then we know that the code can do only one thing: multiply the input by a dimensionless constant.

Are you referring to a particular implementation of dimensioning? I would expect that the function f x = x + 1 meter could be typed as Length -> Length . IIRC, Fortress requires the conversion between all units of a particular dimension to be defined, so I'd have guessed that Fortress would allow this typing.

I said "and there are no other dimensionful values involved" whereas you have introduced a dimensionful constant "1 meter".

There's a very interesting phenomenon in physics: there are very few constants with dimension. For example, take a fluid dynamics simulation. This might involve many thousands of lines of code and yet there'll only be a handful of dimensionful constants: the fluid densities, the fluid viscosities, maybe some dimensions coming from the size of the elements the simulation is based on and a couple more. This is part of where the power of dimensionful types comes from: you know that there aren't going to be new constants like 1.2345 meters introduced in every other line of your code. Most constants that do crop up will tend to be dimensionless.

Consider, for example, this physical problem: we bend a wire into the shape of a sine wave oriented horizontally so that it follows y = l*sin(x/l) (l is a scaling). We place a bead on the wire at the midpoint between a peak and a valley (ie. on y=0). We now release the bead. How long does it take for the bead to hit the bottom of a valley, assuming no friction? You can probably see there is going to be a pretty messy bit of differential equation solving involved in getting the answer out. I've no idea what the exact answer is but but we can say immediately that it must take the form a*sqrt(l/g) where a is some dimensionless constant and g is the acceleration due to gravity, because that is the only expression that has the right dimensions. In a language that enforced type safety, if we wrote a function of type length -> acceleration -> time, and knew not to introduce dimensionful constants (maybe the compiler should warn us if we try to), we would be forced to write a*sqrt(l/g) simply because it would be the only thing that compiled.

Thanks, that makes plenty of sense. I interpretted "and there are no other dimensionful values involved" to mean that there are no other dimensionful parameters passed. My mistake :).