[Axiom-developer] Re: Dimensions as types...

[C Y]

--- Ralf Hemmecke <address@hidden> wrote:

> Hi Cliff,
> > Well, I think it's just that I'm not thinking clearly enough yet in
> > Aldor.  I was thinking maybe something like (warning, pseudocode,
> maybe
> > even conceptually wrong)
> > 
> > define Dimension: Category == with {
> >      "*" : (%,%) -> %
> > }
> > 
> > DerivedDimension: AbelianGroup with {
> >      "*": (A: Dimension, B: Dimension) -> C: Dimension
> >      "^": (D: Dimension, E: Integer) -> F: Dimension
> > } == add{
> >      ***Some A*B operation that returns C according to Abelian
> rules***
> > }
> 
> First of all, forget these double quotes around * an ^. We are
> speaking Aldor here.

OK.

> Then I actually see no reason for adding the "C:" and "F:" above.

I think I got ahead of myself - I was thinking about what I wanted to
happen at the unit level.  I agree that a dimension * a dimension is a
dimension, so C and F aren't needed.

Looking ahead to units:

Let's say I multiply meters:Length and seconds:Time together.  I want
to end up with meters*seconds:Length*Time, which is both a new unit and
a new dimensional type.

For this to work and generate the new type Length*Time, but not in
general allow Length*Anything as a new type, both Length and Time must
in turn be of type Dimension. (meter:Length:Dimension?)  So from the
point of view of meters*seconds, the resulting type is different from
BOTH of the input types and cannot be predicted - it must be
calculated.  So I'm not sure what the *: (%,%) -> % should look like
for units, because the type of none of the inputs to * are determined
in advance.  All that is known in advance is the type of the types of
the inputs - the types actually operating at the level of the *
operation are not known until the computation is made.

Manipulating Length*Time in dimensional analysis is much simpler - they
are both constants of type Dimension and return an expression that is
also of type Dimension, in the same way that 1*2 are integers and
return a result of type integer.  But meters*seconds is not so simple,
because meters of type length and seconds of type time multiply to give
meters*seconds of type length*time.  The governing behavior of the
legality of * for units is not the type of the unit but the type of the
dimension of the unit, and I'm not sure how to specify that.  That was
why I had *: (A: Dimension, B: Dimension) -> C: Dimension (which should
have been in the unit entry not the DerivedDimension entry), as a way
to try and express that the demand for type correctness is not at the
level of A, B and C (length, time and length*time) but that the type of
any type input into or returned out of the * operation must be of type
Dimension.  Otherwise, there are no constraints on the types that may
be multiplied, which would seem to be the same as saying that you can
multiply 1:Integer*2.0:Float*(2/3)Fraction as long as they are all
Numbers, and Integer*Float*Fraction would then become a new numerical
type for the value 4/3. (Note that this is different from the +
operator, which will need to enforce type not at the type of the type
level but at the A,B,C level -> length+time will fail, as will
length+anything where anything is any type other than length, whether
or not anything is of type dimension.)

Sorry if I'm saying this incorrectly, but hopefully my concern is
clear.

>  > Quantities then would have a rep of
> > a value (integer, float, what have you) and a Unit, and the type of
> a
> > Quantity would be Union(Float,Dimension) or something of the sort.
> 
> Why would the type of a quantity be a union of Float and Dimension?
> You are not telling me that you must model dimensionless constants?
> These constants should be modelled as being of type Dimension. You
> did the same thing in your text. That is the dimension <1>. Am I 
> wrong?

I'm not sure - I might have said that wrong.  I would argue that a
dimensionless constant has two components - the numerical value of the
constant, which has some numerical type, and the dimensional type <1>. 
The dimensional type <1> is what has the type Dimension - <1> is itself
a type as well - the type of a dimensionless constant *as a whole* is
<1>.  At least, I would like it to be - I had assumed that since the
numerical type of the constant number must be retained that would wind
up with the expression of the constant being some combination of the
two, but maybe that doesn't have to be the case.

> >>> Does Aldor permit this "types having types" behavior?
> >> Of course.
> 
> > Thanks!  I will study what you have done in more detail.  Am I
> > correct in that you are not actually "multiplying" dimensions in
> > the Abelian group sense but are combining the names of the types
> > and the "*" character?
> 
> That was for simplicity reasons. Of course, what I called Unit should
> be an multiplicative Abelian group. Also Dimension should be
> modelled a bit differently than what I did. Maybe one needs an extra
> wrapper domain that models the abelian group behaviour.

That could be.

> The problem is that it is not so terribly easy to construct a 
> commutative type constructor. But one can certainly do it.

Yes, I think that is one of the challenges of this task.  The Sun team
deliberately chose dimensions and units to look at because they are a
challenge to represent in conventional type systems in most languages
(actually, impossible might be a better word - Sun basically made a new
one).  I am hopeful that Aldor can do it but it certainly will require
some not-normal ways of working with and generating types.

Cheers,
CY

__________________________________________________
Do You Yahoo!?
Tired of spam?  Yahoo! Mail has the best spam protection around 
http://mail.yahoo.com