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

[Ralf Hemmecke]

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.

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

> 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?

> > > 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.

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

Ralf