Re: [Axiom-developer] Unit package question

[Ralf Hemmecke]

Dear C Y,

I think most of the answers you find in the Aldor User Guide.
http://www.aldor.org/AldorUserGuide/
http://www.aldor.org/docs/HTML/index.html

But let me perhaps say a few things in my own words.

> > Mass(R: Ring): Ring == add { ... }

That is nothing else than the definition of a function Mass.
See http://www.aldor.org/docs/HTML/chap6.html
Remember (almost) everything in Aldor is a first class object. So Aldor
allows you to take domains as a parameter and to return a domain. Ring
is a category (in the library Algebra distributed with Aldor) and it is
the type of R. So whenever you want to call Mass(SOMETHING) this
SOMETHING must be of category Ring. That means it has to export all the
functions that show up in the definition of Ring.
(Look for the definition here:
http://www-sop.inria.fr/safir/WHOSWHO/Manuel.Bronstein/algebra/index.html)

> > Mass(T: with { +: (%, %) -> %; *: (%, %) -> %; ... })(R: T): T ==
> > add { ... }

That one is in fact a bit more complicated. It is a function that
returns a function that returns a domain. I think, it would have also
worked if I had written

Mass((T: with {
   +: (%, %) -> %;
   *: (%, %) -> %;
   ...
}, R: T): T == add { ... }

(A function with two parameters that returns a domain...)

That goes in Aldor under the name of "dependent type".
http://www.aldor.org/docs/HTML/chap7.html#4

> Units(R: Field): Exports == Implementation where U == Fraction
> Polynomial Integer
>
>
> 1)  The syntax (R: Field) - what does this actually denote?  R I
> guess is all Rings?  I don't know how to parse this statement - is :
> a separator, an indicator that R is being restricted to Field
> (whatever that is) or what?  Why is it there at all - I'm assuming it
> has something to do with letting Axiom know about the existence of
> the idea of <something>*Units?

Well that code is from Martin, I guess. But yes, it is intended to say
that this <something> is an element of type R and such an R must at
least have all the field properties (ie the signatures of Field).

That parametrization makes the code more flexible. You could leave out
this (R: Field) stuff and restrict to use Float all over, but then you
would have to implement another domain if you come to the problem that
instead of floats you would also like to allow variables.

> 2)  Exports == Implementation - what is actually being exported here,
>  and where is it being exported to?

Exports and Implementation come later in the code. You have not given
them here.

> 3)  U == Fraction Polynomial Integer  I'm assuming this is part of
> the Export - I'm also guessing the $U at the end of the units.spade
> file somehow ties off the domain definition?

coerce((x::Rep).units)$U means "call a function (here coerce) from the
domain U". That is simply to help the compiler. Sometimes it happens
that there is a function f: A->B from domain D1 and f: A->B from D2 in
scope. You would not like the compiler to choose for you. (Aldor would
reject compilation in such a case. You would have to make your
intentions clear by saying f$D1 or f$D2.)
Look for $ on the page http://www.aldor.org/docs/HTML/chap7.html

> 4)  What is the significance of "%" within a domain definition?

Simply translate it to THISTYPE. If you say

Foo(T: with {random: () -> %}): with {random: () -> %} == add {
  Rep == T;
  random(): % == per random();
}

then you could use Foo(Integer) and Foo(MachineInteger) and the % would
in the first occurence be like T (ie Integer or MachineInteger) and in
the second occurence like Foo(T) (ie like Foo(Integer) or
Foo(MachineInteger)). Think of it as a placeholder.

The line
random(): % == per random();
basically says:
in order to define random for Foo(T) use the function random from T.

> 5)  Is there a file in the mnt/linux/doc directories somewhere that 
> gives a detailed description of the syntax of Axiom's spad code?

Well, unfortunately, spad syntax is not exactly the same as Aldor
syntax. It is reasonably close, but there are things that the Aldor
compiler does not allow. (Which is good.)

Take for example the line
x * y  == [(x::Rep).expr  * (y::Rep).expr,
           (x::Rep).units * (y::Rep).units]

As spad code that would be OK (I have not checked it), as Aldor code it
is unacceptable. You have to give the types for x, y and the return
type, ie you would have to write

(x: %) * (y: %): % == ...

You might say, the compiler should be smart enough to fill in missing
information if it is extractable from the environment. Well, sometimes,
for example, for polynomials you migth want to have a function

(x: R) * (y: %): % ==

where R would be the type of coefficients. Now you have two * functions
and reading the code would be quite confusing if both these functions
start via "x*y==...". I think it is good practice too be a bit more
explicit. (Sometimes it's humans that read the code.)

> What does it mean to define "Exports" from a Category or Domain?

I am not quite sure that I understand the question. In the definition of
> Units(R: Field): Exports == Implementation where

the Exports are the functions/constants you see when Units(...) comes
into scope. I think that is called "expose" in Axiom terms. In Aldor you
would say "import from Units(...);" and then you can use the functions
from Units, ie, its exports without using the $Units(..) syntax.

> Are Exports visible to the user on the command line or do they 
> manifest themselves in the parent Category?

What is the parent Category here?

> Each "unit" domain (or more properly, dimension domain that defines a
>  non-basic dimension) needs to know enough about the other domains to
>  spot significant unit combinations, if we add derived units like
> Force into the picture. (We need to for any non-trivial use of a
> serious Units package.)  So if we define a Mass domain, a Length
> domain, and a Time domain can we somehow define a derived domain
> which recognizes and handles the combination Mass*Length/Time^2 as
> Force?

I would opt for a general Unit domain instead of a domain for Mass, 
Length, etc. I somehow fear that Mass*Length (id Domain times Domain) is 
hard to work with. Implementation should be no problem, but I fear to 
convert from such a form into Force could lead to problems. Anyway, such 
a Metadomain would know about combinations of the basic domains and you 
have a Unit domain again which knows about all units.

Ralf