[Axiom-developer] RE: [Aldor-l] exports and constants

[Page, Bill]

Ralf,

Thanks for continuing your discussion on the list. I hope
my comments below further the discussion and do not appear
overly "final". I admit that thinking deeply and correctly
about Aldor's (and Axiom's) type system is quite difficult
and I may well still be making some errors below. Please
bare with me while I try to give my current understanding
below. :)

On Thursday, July 20, 2006 7:12 AM you wrote:
> 
> Sorry, but Christian and me started that discussion in German,
> but we now think that it might be interesting for all other
> Aldor people.
> 
> So let me start with a little program that shows some strange 
> behavior.
> 
> ---BEGIN aaa.as
> #include "aldor"
> import from String, TextWriter, Character;
> 
> define CatA: Category == with { }
> define CatB: Category == with { }
> define SomeCat: Category == with { CatA; CatB; }
> Dom: SomeCat == Integer add;
> 
> A == Dom;
> B: CatA == Dom;
> H: CatA == Dom add;
> 
> stdout << "A has CatA: " << ( A has CatA ) << newline;
> stdout << "A has CatB: " << ( A has CatB ) << newline;
> stdout << "B has CatA: " << ( B has CatA ) << newline;
> stdout << "B has CatB: " << ( B has CatB ) << newline;
> stdout << "H has CatA: " << ( H has CatA ) << newline;
> stdout << "H has CatB: " << ( H has CatB ) << newline;
> ---END aaa.as
> 
> You get...
>  >aldor -grun -laldor xxx.as
> A has CatA: T
> A has CatB: T
> B has CatA: T
> B has CatB: T
> H has CatA: T
> H has CatB: F
> 
> In particular, that "B has CatB" is a bit surprising, isn't it?
>

I think you are dealing here with two separate but related issues:
1) *static* typing, and 2) inheritance rules. All types in Aldor
are static (or at least *nearly static*) meaning that they must be
resolved during the compilation phase.

Aldor has some rather complex inheritance rules because domains
and categories follow very different rules (the first involves
abstract set "membership" while the second involves "sub-types"
of abstract subsets.
 
> Has someone found a description in the Aldor UG of whether this
> is intended to be so or this should be considered a bug in the
> compiler?

No, I don't think it is a bug. This is all rather well (although
perhaps too tersely explained in the Aldor Users Guide, under
the heading of "Type Satisfaction", see section 7.7.

Unfortunately http://www.aldor.org is inaccessible :( again! ):
but you can get it from Google's cache:

http://72.14.207.104/search?q=cache:tXXWE6iGeLEJ:www.aldor.org

/docs/HTML/chap7.html+aldor+users+guide+type+satisfaction
&hl=en&gl=ca&ct=clnk&cd=1nces.

or from one of the other pdf versions:

www.ph.ed.ac.uk/~bj/paraldor/WWW/docs/documentation/axlugII.pdf

We have also discussed this a little before:

http://lists.gnu.org/archive/html/axiom-developer/2006-03/msg00140.html

and on static types in:

http://lists.gnu.org/archive/html/axiom-developer/2006-02/msg00065.html

> 
> Let me go on with answering Christian's mail...
> 
> On 07/20/2006 11:05 AM, Christian Aistleitner wrote:
> > On Wed, 19 Jul 2006 11:20:06 +0200, Ralf Hemmecke 
> <address@hidden> wrote:
> > 
> >>> i: Integer == 1;
> >>>  und
> >>>  i: Integer == 2;
> >>>  nicht gleich sind.
> >>
> >> Naja, hier muß man nur wissen, daß die Symbole 0 und 1 
> >> Ausnahmen in Aldor sind. Die kann man nämlich als Bezeichner
> >> verwenden, während das bei 2 nicht geht. Weil das einfach
> >> ein Symbol ist, das wie eine ganze Zahl aussieht, aber
> >> niemals ein Bezeichner sein kann. (Letzteres ist eigentlich
> >> auch eine Einschränkung, sonst könnte man "PowerSet(S)" 
> >> ganz einfach als "2^S" implementieren. OK, dann wäre der 
> >> Bezeichner allerdings "2^"... naja.
> > 
> > Sorry that was a bad example. What I wanted to point out is 
> > that from a user perspective,
> > 
> >   identifier: type == value
> > 
> > should always refer to the same language construct. So
> > 
> >   i: Integer == 2;
> > 
> > and
> > 
> >   i: Integer == 3;
> > 
> > should be the same language construct,
> 
> Where do you see a difference?
> 
>  > just as
> > 
> >   Ident: Category == Domain;
> > 
> > and
> > 
> >   Ident: Category == Domain add;
> > 
> > . Of course, "Domain" and "Domain add" are different things.
> > No doubt about that. However, this difference should be the
> > only difference.

"add" forms a "add expression". See especially sections 7.8 and
8.10.

The more I read (and re-read) the Aldor Users Guide, I am
beginning to believe that the entire definition of Aldor
is in fact very succinctly and consistently given here. But
I have never been able to read and appreciate it in just a
few linear readings of the text.

> 
> There is a difference in the semantic, but I cannot
> remember that I have found a proper explanation of what
> "Ident: SomeType == Dom" actually means (no "add" here).

In the above the value of 'Ident' *is* 'Dom' whereas in the
previous case 'Ident' is the name of a new domain whose
"parent domain" is 'Dom' - like the difference between



> 
> >> One cannot, however write something like
> >>
> >> CatC: Category == with { }
> >> H: CatC == Dom;
> > 
> > Of Course not, because Dom does not provide CatC.
> 
> >> Different from
> >>
> >> A: CatA == Dom add;
> >>
> >> the construct
> >>
> >> H: CatA == Dom;
> >>
> >> just means that H provides *at least* the exports of CatA, 
> >> and the compiler can tell, if Dom provides less.

In the first case you are defining a new domain A which
satisfies only CatA. In the second case you are saying
that H is identical to Dom, but the compiler knows that
is not true.

> > 
> > You can interpret both kinds as "provides at least".

No, I don't think that is true.

> > But the first statement does not give you any more than
> > CatA.

In the first case A is a member of CatA, in the second case
you are saying that type of Dom is a subtype of the type
of H (CatA).

> 
> >> It is going to be interesting.
> >>
> >> Take for example
> >>
> >> A: Join(CatA, CatX) == add {...}
> >> B: Join(CatB, CatX) == add {...}
> >> X: CatX == if odd? random() then A else B;
> >>
> >> It is clear that X cannot export more than CatX. In such 
> >> constructions the additional exports of A and B cannot be
> >> seen.
> > 
> > I am a bit puzzled right now. The line
> > 
> >> X: CatX == if odd? random() then A else B;
> > 
> > causes problems and does not compile. Furthermore, for
> > 
> >> X: CatX == A
> > 
> > X has both CatA and CatX, as expected ... Could you detail 
> > on that problem.
> 
> Sorry, I have not tested that line and I also cannot compile it.

The reason of course is because the expression 'odd? random()'
is not static - it does not have a well-defined value at the
time that the source is compiled. It is only later when the
code is run that we can know if the condition is true or false
in a particular instance. The Aldor compiler is not able to
compile *types* of this kind.

This might seem like a severe restriction, but section 7.8
ends with an example of a "conditional definition" in Zmod
where such static typing is still interesting. I think
understanding in what sense this is "static" (in comparison
to your "dynamic" typing example above) is very important
to understand Aldor's type system as a whole.

> 
> ---BEGIN aaa2.as
> #include "aldor"
> import from String, TextWriter, Character;
> 
> define CatA: Category == with;
> define CatB: Category == with;
> define CatX: Category == with;
> 
> A: CatX with { CatA } == add;
> B: CatX with { CatB } == add;
> 
> X: CatX == if true then (A add) else (B add); -- (*)
> 
> stdout << "X has CatA: " << ( X has CatA ) << newline;
> stdout << "X has CatB: " << ( X has CatB ) << newline;
> stdout << "X has CatX: " << ( X has CatX ) << newline;
> ---END aaa2.as
> 
> aldor -grun -laldor aaa2.as
> X has CatA: F
> X has CatB: F
> X has CatX: T
> 
> That is clear, but why does the compiler reject the program 
> without the "add" in line (*)?
>

It is because the types of A and B are not a subtypes of CatX.
But X can be a member of CatX defined by (A add) or (B add).

> > 
> >> R: GcdDomain == if iWantRationals? then Fraction Integer 
> >>                                    else Integer;
> >> computation()$MyPackage(R);
> >>
> >> Und in MyPackage haben wir sowas
> >>
> >> gcd(a: R, b: R): R == {
> >>    if R has Field then {
> >>        ... kann nur 0 oder 1 sein
> >>    } else {
> >>       ... implement Euclidean Algorithm
> >>    }
> >> }
> >>
> >> und computation() benutzt intern diesen gcd. Selbst wenn
> >> iWantRationals? = true
> >> wird nicht der einfachere Körperfall genommen. MyPackage 
> >> sieht also die zusätzlichen Exports nicht mehr. Blöd, was?
> > 
> > This puzzles me even more, because it works properly for me:
> > 
> > #include "algebra"
> > import from String, TextWriter, Character;
> > import from MachineInteger;
> > 
> > #if FIELD
> > firstIsField? == true;
> > #else
> > firstIsField? == false;
> > #endif
> > R: GcdDomain == if firstIsField? then (Fraction 
> address@hidden) else 
> > (address@hidden);
> > 
> > stdout << ( R has GcdDomain ) << newline;
> > stdout << ( R has Field ) << newline;
> 
> I am actually a bit amazed that your program runs and gives
> expected results. But what about...

Its static typing again!

> 
> ---BEGIN aaa3.as
> #include "aldor"
> import from String, TextWriter, Character, MachineInteger;
> 
> define CatA: Category == with;
> define CatB: Category == with;
> define CatX: Category == with;
> 
> A: Join(CatX, CatA) == add;
> B: Join(CatX, CatB) == add;
> 
> MyPkg(X: CatX): with {isA?: () -> Boolean} == add {
>       isA?(): Boolean == X has CatA;
> }
> main(): () == {
>       import from CommandLine, Array String;
>       X: CatX == if zero? #arguments then (A add) else (B add);
>       stdout << isA?()$MyPkg(X) << zero? #arguments << newline;
> }
> main();
> ---END aaa3.as
> 
>  >aldor -fx -laldor aaa3.as
>  >aaa3
> FT
>  >aaa3 1
> FF
>

Static type again: the value of 'isA()' is determined at
compile time and does not depend on #arguments.
 
> It is clear with the "add" in the definition of X that we will
> always see a F in the first column of the output. Can someone
> find a "nice" construction where X is defined by a similar "if"
> construction and the first F would turn into T?

This is not possible because as a domain X must be static.

> 
> Of course it would be easy to write
> 
> main(): () == {
>       import from CommandLine, Array String;
>       b: Boolean := zero? #arguments;
>       stdout << (if b then isA?()$MyPkg(A) else isA?()$MyPkg(B));
>       stdout << zero? #arguments << newline;
> }
> 
> and obtain TT and FF, but that is not a "nice" solution.
> 
> Imagine there were another 2 domains R and S that would take 
> a domain of type CatX as input and return a domain whose exports
> depend on the input. (A polynomial construction Dense/Sparse
> (for R and S) over some coefficient domain (for A and B) would
> be a common example.)

This is possible because as types domains are static in Aldor.

> 
> It's soon becoming quite cumbersome and unreadable if it is 
> done in the way the last main() function demonstrates.
> 

This is an argument for dynamic types, which certainly is
possible (e.g. Lisp), but efficient compilation is much more
difficult to achieve. One of the beautiful things about Aldor
is that it seems to do so much in spite of it's static
type system.

Regards,
Bill Page.