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

[Ralf Hemmecke]

Hello Bill,

Thank you for your comments, but I don't seem to agree with everything.

Let's keep this programm since I'll refer to its output.

> > ---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.

The "B has CatB" result is not about static or dynamic. If you read the 
code above. Would you immediately be able to tell that the Type of B is 
NOT CatA (as "H: CatA" might suggest), but the same as the type of Dom?

> > 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.

I know that the html version of the user guide at aldor.org is a little 
different from the .pdf version, but it seems 7.7 and 7.8 are OK.
Looking at the pdf version, I cannot find good explanations of what

H: CatA == Dom;

actually means.

The constant assignment

H == Dom;

is clear, though. H inherits type and value of Dom.

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

If Ident *is* Dom then what do you think the ": SomeType" is for?

> > > > 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.

First and second is not so clear to me now. Can you repeat your 
statement. In particular I don't understand your last sentence.

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

> No, I don't think that is true.

Well, the compiler behaves according to "provides at least" if you write

H: CatA == Dom;

That would compile, whereas

H: CatC == Dom;

would not.

> > > > 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.

Bill you should have tried the following piece of code.

---BEGIN aaa5.as
#include "aldor"
define CatA: Category == with;
define CatB: Category == with;
define CatX: Category == with;

A: Join(CatX, CatA) == add;
B: Join(CatX, CatB) == add;
#if ADD
import from MachineInteger;
X: CatX == if odd? random(10) then (A add) else (B add);
#else
X: CatX == if true then A else B;
#endif
---END aaa5.as

>aldor -fx -laldor -DADD aaa5.as

compiles without any complaints. Now try without the ADD assertion.

>aldor -fx -laldor aaa5.as
"aaa5.as", line 14: X: CatX == if true then A else B;
                    ...........^
[L14 C12] #1 (Error) Have determined 0 possible types for the expression.
  Subexpression `A':
        Meaning 1:
                Join(CatX, CatA) with
                    ==...
  Subexpression `B':
        Meaning 1:
                Join(CatX, CatB) with
                    ==...
  The context requires an expression of type CatX.


Are you now a bit more puzzled?

Random things are not the problem. Obviously "A" and "A add" are not 
(treated) identical by the compiler.

Now if we assume that

X: CatX == if true then A else B;

yield an X of the type of the domain on the right hand side then the 
compiler has to match the types of A and B (they have to be equal).
Try to replace B by A in the code above and the compiler will not 
complain anymore.

And to make you even more happy...

---BEGIN aaa6.as
#include "aldor"
#include "aldorio"
macro I == MachineInteger;
define CatX: Category == with {foo: () -> I}
A: CatX == add {foo(): I == 0;}
B: CatX == add {foo(): I == 1;}

import from MachineInteger;
X: CatX == if odd? random(10) then A else B;

main(): () == {
        import from X;
        stdout << foo() << newline;
}
main();
---END aaa6.as

woodpecker:~>aldor -fx -laldor aaa6.as
woodpecker:~>aaa6
0
woodpecker:~>aaa6
0
woodpecker:~>aaa6
0
woodpecker:~>aaa6
0
woodpecker:~>aaa6
0
woodpecker:~>aaa6
1
woodpecker:~>aaa6
1

It's only the type of X that must be clear at compile time. But maybe 
even that is just a current restriction of the compiler. Categories are 
first class values and they should be computable at runtime. But I won't 
go into detail since there are certain problems that occur if categories 
are truly "first class".

The interesting part of aaa6.as is that now if one writes

X: CatX == if odd? random(10) then (A add) else (B add);

(with the "add"), the program does not compile anymore in contrast to 
aaa5.as above.

>aldor -fx -laldor aaa6.as
"aaa6.as", line 13:         stdout << foo() << newline;
                    ..................^
[L13 C19] #1 (Error) There are no suitable meanings for the operator `foo'.


> > ---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).

I don't understand.
A is of type Join(CatX, CatA) and you are saying that this is not a 
subtype of CatX??? Similar for B.

> > ---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.

That is completely wrong. If "isA?()" would be computed at compile time,
I would be really amazed. X is a parameter to MyPkg. How should the 
compiler be able to evaluate "X has CatA" at all?

> > 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.

Maybe I don't quite understand your "static", but I believe that what I 
have demonstrated above shows that Aldor just requires that types are 
constant in a certain context, but otherwise one can do quite a lot with 
them.

My feeling is that categories are not really "first class" in Aldor 
(which is certainly another issue). I haven't seen any reasonable 
program that computes a category and then creates a domain that belongs 
to that category. That the compiler cannot handle computed categories, I 
can understand, but I don't even know whether it would be useful to 
treat categories as "first class citizens".

Ralf