Re: [Axiom-mail] AXIOM documentation

[Ralf Hemmecke]

Welcome Alan,

The first thing I'd like to support is Bill's suggestion that you should 
look at Aldor in order to understand the programming language. Axiom's 
SPAD (its compiler language) is a little different, but if you encounter 
differences and don't understand them, then it is probably better to ask 
again at the list (and maybe then write down some notes so that these 
differences become explicit --- best to do on a page at the MathAction 
(the Axiom wiki) http://wiki.axiom-developer.org/FrontPage . Replace 
"FrontPage" by some reasonable term and create that page. If you first 
would like to experiment with the wiki then start you term with Sandbox...

> > I am trying to understand the documentation.  Below are some notes
> > based on Chapter 5 of the book.  The system seems to be based on a
> > directed graph whose nodes are Axiom objects and whose edges are of
> > two sorts which could be called
> > member
> >    a is a member of b if b is a domain (or subdomain?) and a's type is b
> > refines
> >    c refines d if all members of c are members of d and in addition
> >                   all operations of c are operations of d.
> > Is this right?

[snip]

> > In the book, Figure 1 shows a bit of this graph for the "refines"
> > relation and for some basic domains of algebra.  Could someone please
> > draw a similar graph with nodes including
> >    Type
> >    Category
> >    Domain
> >    Any
> >    SetCategory
> >    Symbol
> >    Variable ?
> > These are the obscurest objects.  Someone has tried to explain them
> > in bookvol1 Chapter 5, but it is hard.  See the notes below.

As you will find in the Aldor User Guide everything has a type.
You can see at Aldor as a language that has 3 levels of things (well, I 
wanted to say "object", but that gets easily confused with that concept 
in OOP.

(Before anybody wants to complain that I am not totally correct, I'd 
like to say that I did this by intention in order to simplify the first 
steps for a new user/developer.)

Example (I don't refer to Axiom but rather to the library LibAldor so 
the names might not be know to Axiom):

1st level:  42              (is of type Integer)
2nd level:  Integer         (is of type IntegerType)
3rd level:  IntegerType     (is of type Category)

The first level I'd like to call "simple objects" (but they are 
*definitely not* objects in the OO sense).
The things at the second level are called "domains". (A "package" is a 
special domain.)
The things at the third level are called "categories".
The name "Category" is a special built-in name that denotes the type of 
a category (i.e. the type of things at third level).

The things at second level are formed using the "add {...}" construction.
The things at third level are formed using the "with {...}" construction.

The things at second and third level are called types.
The identifier "Type" is builtin. It is the type of any type, (Something 
like the set of all sets---don't think about Russel's paradox here.)

Think of the things at third level as something comparable to JAVA 
interfaces. (That is not completely exact, but quite near to my taste.)

There are different ways of inheritance.
Second level: single inheritance.

MyDom: with {
  0: %;
  foo: % -> %;
} == Integer add {
  foo(x: %): % == x;
}

The domain "MyDom" exports exactly 2 things, the constant 0 and a 
function foo. As you can see, I have not given a definition for the 
implementation of 0. That implementation is inherited from the domain 
Integer.

Third level. Since that is not connected to implementations, but rather 
only signatures of functions, multiple inheritance is allowed.

So if you have

define CatA: with {foo: %->%, bar: %->()}
define CatB: with {foo: (%, %)->%; bar: %->()}
define CatC: Join(CatA, CatB} with {baz: () -> %}

then the last definition is (nearly) equivalent to

define CatD: with {
  foo: %->%;
  foo: (%,%)->%;
  bar: %->();
  baz: () -> %
}

It simply forms the (non-disjoint) union of all the signatures.
I said "nearly" because in the definition

define CatC: Join(CatA, CatB} with {baz: () -> %}

CatC remembers that it inherits from CatA and CatB while in the second 
definition, there is no relation to CatA and CatB.

So if you define domains

DomC: CatC == add {...}
DomD: CatD == add {...}

and later use constructs like

  if DomC has CatA then ...

  if DomD has CatA then ...

then "DomC has CatA" is true while "DomD has CatA" is false.

Does this help a bit?

> > I have not yet worked out how to refine a domain.  There is a hint on
> > page 14 of the book: Complex(R) defines its exports with
> >    "Ring with ... if R has Field then Field ..."
>
> Complex is a domain constructor, i.e. a function that returns a domain
> as a result.

Yes, and it should be emphasized that things of first, second, and third 
level are all "first class citizens", i.e. each of them can appear as an 
argument to a function. For example "Complex" is such a function. It 
takes a domain (something of level 2) as argument and returns a domain.

In Aldor, you could also write something like

#include "algebra"
#include "aldorio"
mygcd(R: EuclideanDomain)(a: R, b: R): R == {
  R has Field => if zero? a and zero? b then 0 else 1;
  while not zero? b repeat { (a, b) := (b, a rem b) }
  return a;
}
Q ==> Fraction Integer;
import from Integer, Q;
g := mygcd Integer;
stdout << g(4,6) << newline;
stdout << mygcd(Q)(4::Q,6::Q) << newline;

Let me explain.

The signature of mygcd is

  (R: EuclideanDomain) -> ((R, R) -> R)

so it is actually a function that takes as input something of level 2 
and returns a function (something of level 1) whose type is

  (R, R) -> R

As you can see, the type of the output cannot be written down without 
knowing R. But R in this case is the *value* of the argument. Only the 
type of R is clear at compiletime (which is EuclideanDomain---something 
of level 3). The type of "mygcd" is called a "dependent type".

Note also the definition and use of g. g is a variable that has a 
function value, i.e. its signature is

  (Integer, Integer) -> Integer

and since that is a function type g can be applied to a pair of integers 
(4,6).

> > Please forgive me if these matters have simple answers.

Definitely not a problem. We all know that Axiom/Aldor *is* hard to 
learn. But when you come over the first hurdles you'll love the concepts 
that distinguish Axiom from all other CASs.

Ralf