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

[C Y]

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

> Hi Cliff,
> 
> I'll copy that to axiom-developer, because it might start another 
> discussion about dimensions in Axiom.

OK :-).
 
> > So what we need, in effect, is types that have types.
> 
> You have NOTHING in Aldor that has no type.

OK.

> > And we also need a * operation that can take two types that are
> > themselves of type Dimension and generate a new type (also of type
> > Dimension) as the output type, not determined in advance because
> > the output type is in fact GENERATED based on the input types.
> 
> Do you see a problem?

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***
}

where the return type of the "*" operation is C and defined by
multiplying A and B, but A, B, and C all must be Dimensions.  Then,
Unit would be a Rep with a name unit and a type of dimension Dim, and
multiplying units u1 and u2 would result in a name of 
unit1:String*unit2:String -> unit3:String with a type Dim1:Dimension *
Dim2:Dimension -> Dim3:Dimension.  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.

> > Does Aldor permit this "types having types" behavior?
> 
> Of course.
> 
> Analyse the code below and ask if something is unclear.
> I would very much like to see an upcoming dimensions package
> programmed along these lines. There are certainly lots of things just
> rudimentary, but as you can see, multiplying types to construct new
> types is not at all complicated. That is the power of having types as
> first class citizens.

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?  (/me winces at what is probably a horrible description).

> Enjoy.

Thanks again!
 
> Ralf
> 
> PS: I think it gets a bit complicated to convince Aldor to believe
> that Length*Time and Time*Length are not so different. With the code
> below these are different dimensions.

I think in an Abelian group aren't a*b and b*a the same?  I think
that's why the literature is more or less at a consensus that
dimensions should be modeled by Abelian groups over the multiplicative
operation.

CY

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