[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-mail] AXIOM documentation
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-mail] AXIOM documentation |
Date: |
Thu, 21 Jun 2007 10:40:13 +0200 |
User-agent: |
Thunderbird 2.0.0.4 (X11/20070604) |
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