Re: Dimensionality Checking (Ada 20XX)

["Mark Lundquist" <mlundquist2@attbi.com>]

"Nick Roberts" <nickroberts@adaos.worldonline.co.uk> wrote in message

news:9v0crt$bo2bi$1@ID-25716.news.dfncis.de...
> I'm liking this idea a lot!
>
> Supposing the revision adds a package:
[snip]

Would you not prefer a solution in which no particular set of units was
built in to the core language?  That is, I think it would be fine if the
standard library had a package Ada.SI_Units or whatever, written in ordinary
Ada 20xx (a unit-aware language), just to save everyone the trouble of
writing it themselves, but I don't think that the core language itself
should have any intrinsic units.  Please comment!

>
>
> We can declare our own units, e.g.:
>
>
>    Foot: constant Ada.Units.Unit_Type := Meter * 0.3048;
>

I think that units should be their own entity in the language, not fudged up
with a magic type and magic quasi-values.  The language in the RM defining
the semantics of names, values, types and objects is pretty carefully
constructed, and it seems like your syntax would really gum it up :-).  That
is, he definitions of type, value, and constant object, and just about
everything else in the RM that these things touch, would all have to be
qualified and special-cased to accomodate the quasi-type, quasi-values and
quasi-constant-objects that support your magic.

You'd rather want to write something like this:

    unit Meter;    -- a base unit

    unit Meters_Squared is Meter ** 2;    -- a derived unit

(Of course the names there are not the point).  But, you get the idea,
right?

Then,

    type Length is range 0.0 .. whatever;
    for Length'Units use Meter;

The declaration of Length is an ordinary type definition (and it's my very
own type so I can call it whatever sucky name I want -- the name here is not
the point, it's just an example).

>
> I don't believe unit specification (and therefore dimension checking) is
> applicable to floating-point types.

Why in the world not?

> They may be used for various purposes
> (perhaps often when a fixed-point type ought to be used), but a
> floating-point number is conceptually a ratio, and therefore implicitly
> unitless (and dimension-indeterminate).

whaaaaaaahhhh?

Nick, did you drop a little too much acid, back in the hippie days? :-)

Bet seriously... you're gonna have to explain that one to me (your theory
about numbers -- not about the acid! :-)

>
> There's the question of private types. I feel that the requisite
conversions
> and other mixed operations should be provided for a private type
explicitly
> (in its package spec), and that these operations should do the requisite
> conversion and checking, which may well be more complicated than mere
> scaling and dimensionality. The unit facilities would, of course, be
> applicable to those components which were of unit-specific (fixed-point)
> types.

I'm not sure quite what you're getting at there, but it sounds like it might
be related to an issue I've been thinking about, which is that these units
currently would not be able to work with "quasi-numeric" abstractions such
as people define for things like rational numbers, infinite-precision
arithmetic, etc.  However, fixing only that would be gold-plating the turd,
since these types would still have all the current problems of quasi-numeric
types as I summarized in a recent post (in response to Richard Reihle).  It
seems like the complete solution would be to add language support for
quasi-numeric types, i.e. something in the spec says "this type is private,
but it has certain properties such that you can treat it as a numeric type".
I think this is do-able within reason.  The scheme would have to involve
certain required attribute definition clauses (e.g. to specify conversion
functions to and from true numeric types).  I haven't really thought this
part through yet.

Here's some other things I've thought about so far on the unit stuff...

1) You have to be able to handle logarithmic units... that's easy, for a
unit U:

    U'Log (B)    -- denotes the log to the base B of U
    U'Exp (B)    -- denotes B to the power U


2) There's a bad problem with generics.  Unit-safe programming totally
destroys the generic contract model.  For example... given this:

    generic
        type T is digits <>;
    function F (X, Y : T) return T;

How can you tell if this is legal?:

    type T is [whatever...];
    for T'Unit use [whatever...];        -- T is a dimensioned type
    .
    .
    .
    function Ft is new F (T);

You can't!  (It's much easier to ID the ends of a CatDog spinning in an
inertial frame of reference :-).  If F looks like this

    function F (X, Y : T) return T is
    begin
        return X + Y;
    end T;

then we're as happy as clams, but if it is this:

    function F (X, Y : T) return T is
    begin
        return X * Y;
    end T;

then we've got trouble!

I think I can see my way through to figuring out how to do the actual proof
checking on the units, but still the idea of a semantic dependency of an
instance on a body is unprecedented.  The Powers That Be would have to
decide that unit-safe programming is Worth It to allow this when generics
are instantiated on dimensioned types.  In terms of the implementation, you
would have a legality check that actually takes place after everything is
compiled!  It would have to be done by the "prelinker" or whatever tool is
first exposed to all the units that are going to compose the partition being
run.

3) Checking that the system of units established by the currently visible
set of unit definitions is self-consistent.

>
> Three further notes need to be made.
>
> (1) I am not sure if the (seven) SI units I have presented are the
complete
> set of basic units required in reality.

Doesn't matter, specific units should not be built in...

>
> (2) Dimensional analysis could extend (from the basic MLT) to temperature,
> amount of matter, and electrical current. But I don't know if it would be
> practical for these 'extra' dimensions (or any others) to be included in
the
> checking.
>

See above :-)

> (3) I have not provided for units that are offset from the SI units' zero
> points (which are presumably all at the corresponding 'physical' zero
> point). I believe some other post suggested that this tends to be a fairly
> cosmetic matter anyway.
>

No problem:

    Unit_B is Unit_A + Bias;


I think you are on the right track though, as far as what we need units to
do for us: fully static, compile-time checking with inference of derived
dimensions, and automatically reversible and composable unit conversions.
Let's keep our thinkin' caps on... :-)

Cheers,
Mark Lundquist