Tuesday, August 28, 2007

Units and reversable computation

Since we don't want space probes written in Factor to crash because of calculations on mismatching units, Doug Coleman wrote a units library:
10 feet 30 inches d+ 56 s d/

It can add, multiply and divide dimensioned quantities while converting on the fly and making sure all the units make sense (10 miles 30 teaspoons d+ is a runtime error).

There was one problem with this library though, and it was that converting a dimensioned quantity back to a scalar required some boilerplate; for example, we have the following code:
: inches ( n -- dimensioned ) 2.54 * cm ;
: inches> ( dimensioned -- n )
dup 0 { m } { } =dimensions?*
dimensioned-value 100 * 2.54 / ;

The inches word converts a number of inches to centimeters; cm in turn converts it to meters, which is the canonical representation of distances, then creates a dimensioned quantity. However the inches> word is ugly, and it is all boilerplate since the defintion of inches has all the required information.

Let's take a look at cm:
: cm centi m ;

And its auxilliary words:
: centi 100 / ;
: m ( n -- dimensioned ) { m } { } <dimensioned> ;

As you can see, <dimensioned> is the canonical constructor.

Now, enter Daniel Ehrenberg's inverse library. While Dan originally intended to use it for pattern matching, this library is a perfect fit for auto-generating words for converting dimensioned quantities back to scalars.

Indeed, out of the box, it cannot invert <dimensioned>, because it calls natural-sort which is not an invertible operation. However, we can explicitly define an inverse for <dimensioned> (not an inverse in the mathematical sense, since the original function is not one-to-one; strictly speaking, this is a section, that is, a function which satisfies only one of the two conditions of an inverse).

And now, everything works; here, undo is Dan's inversion combinator:
  100 cm [ inches ] undo .
5000/127

So 100 cm constructs a dimensioned object, after converting the dimension to canonical form (meters in the case of distance):
  100 cm .
T{ dimensioned f 1 { m } { } }

And [ inches ] undo takes a dimensioned quantity, and works backwards in order to obtain a number, which when passed to inches, would give the original quantity:
  [ inches ] undo .
5000/127

Lets take a look at the code generated by [ inches ] undo:
  [ inches ] [undo] .    
[ >dimensioned< { } =/fail { m } =/fail 100 * 127/50 / ]

It takes the dimensioned quantity apart, makes sure it is a distance (and not a time, etc), then multiplies the quantity itself by a conversion factor.

So we can convert a scalar represented by unit to any other unit in this way; we can also do stuff like:
  10 miles 30 km d+ [ yards ] undo .
19205600/381

What is shorter, a quarter of a mile or 400 meters?
  1/4 miles 400 m d< .
f

We also support compound units, such as miles per second, miles per second squared, etc. How many teaspoons in a liter plus a tablespoon?
  1 L 1 tablespoons d+ [ teaspoons ] undo .
77937/379

For volume units, the canonical representation is meters cubed:
  15 teaspoons .
T{ dimensioned f 379/5120000 { m m m } { } }

Here is a unit with a denominator:
  20 knots .
T{ dimensioned f 463/45 { m } { s } }

The inverse library automatically guards against invalid conversions:
  30 km 10 s d/ [ teaspoons ] undo .
Unification failed

This is seriously cool stuff. The implementation of units is very simple and elegant, too; only half of the code has to be written, because we can use inverse!

The inverse library depends on two things; the simple mapping between syntax and semantics (the composition of two functions is their concatenation, therefore the inverse of a concatenation of two functions is a concatenation of their inverses!) and it also depends on quotations being sequences rather than opaque code blocks. Two qualities which are unique to Joy dialects such as Factor.

5 comments:

Unknown said...

That's cool that it works out like that. But, I have to tell you, a somewhat similar system has been worked out in Haskell, see http://citeseer.ist.psu.edu/337368.html . And, guess what? It uses monads.

Anonymous said...

Cool exercise but runtime is too late if the error occurs when you are about to land on Mars.

dh said...

Hi Slava,

I really enjoy reading your posts on Factor; it's interesting to see what you are concerned with and what kind of interesting solutions and implementations you provide. I think, it's also your enthusiasm on your on creature (Factor), which is infecting. So far, I just played around a little bit with Factor -- but please, keep on sharing your thoughts.

Dominikus

Anonymous said...

Curious that my reply was not published.

The gist of it was that runtime is too late when the probe is landing on Mars.

Slava Pestov said...

Your reply was published. I publish all commments except for spam (which seems less of a problem these days; maybe I can disable moderation soon).