Re: Dimensionality Checking (Ada 20XX)

[Stephen Leake <stephen.a.leake.1@gsfc.nasa.gov>]

"Nick Roberts" <nickroberts@adaos.worldonline.co.uk> writes:

> In an effort to get back to Ada a bit ;-) I'll describe what I see logs and
> exponentiations of units meaning, and how I see them working.

Ok!

> In my view of the proposed scheme, a 'unit' has two essential
> attributes: a dimensionality; a scaling factor.
> 
> A 'dimensionality' is a factor (a real number) for each of a set of
> dimensions.

Hmm. In physics, dimensionality is an integer. 

> For a certain dimensionality, a 'scaling factor' is the factor (also
> a real number) by which a value in the unit must be multiplied to
> convert it to some (actual or notional) canonical unit for that
> dimensionality.

Ok.

> Supposing our set of dimensions is {Mass, Length, Time}. The unit
> 'Meter' would have the dimensionality (0, 1, 0), and let us choose
> for it the scaling factor 1. The unit 'Foot' would then have the
> same dimensionality, and a scaling factor of 0.3048 (approx.). A
> certain measurement, let us call it 'NJRH' (my height), might be
> 5.95 foot. I intend that the Ada conversion Meter(NJRH) would be
> predefined, and have the value 1.813 (approx.), as well as the
> conversion Foot(Meter'(1.813)), having the value 5.95 (approx.).

Ok, but I'm not clear how to declare these in your new Ada.

> We could imagine a unit (and I don't know whether this corresponds
> to custom in physics) called, say 'Log_Foot', which is intended to
> represent the natural logarithm of feet. 

Nothing like this in physics; there is no need for it. But I'll keep
reading :).

> It would have the dimensionality (0, 1/e, 0) and a scaling factor of
> our choosing, let us choose 1. The value of NJRH in log feet would
> be 1.783 (approx.).

I'm not clear why a "dimensionality" of 1/e corresponds to the log of
feet, but then I don't know what log of feet means, so I guess you get
to define it. 

> I do not intend that the Ada conversion Log_Foot(NJRH) would be
> permitted, nor Foot(Log_Foot'(1.783)). To achieve these conversions,
> it would be necessary to use Log and Exp functions explicitly. Thus,
> instead of Log_Foot(NJRH) we write Log(NJRH), and instead of
> Foot(Log_Foot'(1.783)) we write Exp(Log_Foot'(1.783)).

But, how does the poor compiler know which conversions to allow, and
which to (pre)define?

> Assuming (and this may be an assumption that has to be dropped)
> units are built into Ada by means of -- having added an extra 'unit'
> attribute (in the notional sense as well as actually adding the
> attribute 'Unit) to all scalar types -- permitting the unit to be
> specified for fixed point types, 

Why are we still stuck on fixed point types? 

> it would be necessary to provide a package such as this:
> 
> 
>    generic
>       type Proportional_Type is delta <>;
>       type Logarithmic_Type is delta <>;
>       Base: constant some_real_type := e;
> 
>    package Ada.Numerics.Generic_Logarithmic_Functions is
> 
>       function Log (X: in Proportional_Type) return Logarithmic_Type;
>       function Exp (X: in Logarithmic_Type) return Proportional_Type;
> 
>    end;
> 
> 
> This package would check, upon instantiation, that the dimensionalities of
> Proportional_Type and Logarithmic_Type -- (Mp,Lp,Tp) and (Ml,Ll,Tl)
> respectively, let's say -- are related in the correct way: Mp=Ml/e; Lp=Ll/e;
> Tp=Tl/e. Typically, it should be possible for this check to be done at
> compile time.

Ok, sounds like you could make it consistent.

> According to our example units, this package would be instantiated
> something like this:
> 
> 
>    package Foot_Log_Functions is
>       new Ada.Numerics.Generic_Logarithmic_Functions(Foot,Log_Foot);
> 
>    use Foot_Log_Functions;
> 
> 
> Now, having discussed this matter with my dad (a physicist), we still
> couldn't agree whether this interpretation is correct, so I'd be really
> grateful for any kind of (more) authoritative comment.

Well, "correct" is a loaded term. I still maintain that, in physics,
log (meters) is _meaningless_, and _never_ occurs in a real-world
problem. So attempting to define its meaning in Ada is simply not
useful. You can define something that is self-consistent, but it won't
match physics.

I don't think you'll find a physics text that actually states "log
(meters) is meaningless and forbidden", because it seems obvious, but
I'll look in mine tonight. Maybe a high school text, where they
introduce the notion of measurement, would discuss this (I only have
my college text).

-- 
-- Stephe