[Aldor-l] exports and constants

[Ralf Hemmecke]

Hi again,

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

> Maybe I completely lost my point now (probably), but isn't it good that 
> B has CatB?

Well, I would have no problems with that semantics, but in my 
experiments I had the impression that this is not always the case.
There is need to write up (as Martin suggests) one program that shows 
all the peculiarities. That should become a testcase for the compiler.
But in order to do this, it would be good to learn how the language (not 
the compiler) is supposed to behave.

> If B would not have CatB, things like
> 
> func( R: Ring, a: R, b: R ): R == {
>     if R has Field then
>     {
>         a / b;
>     } else {
>         a * b;
>     }
> }
> 
> would never allow to enter the true branch of the if statment.

See, that was the demonstration in the last part of my previous mail.
(See the line
   stdout << (if b then isA?()$MyPkg(A) else isA?()$MyPkg(B));
in that main function.)
If one passes a domain directly into a function (MyPkg in that case) 
then one would see the additional structure inside the MyPkg function.
If, however, you first say something like

X: CatX == if zero? #arguments then (A add) else (B add);

and pass X to MyPkg, then, of course in MyPkg you don't see more than a 
CatX structure. And that would be reasonable, since X is defined to be a 
new domain with declared exports CatX.

> Consider
>   func( Fraction Integer, 1, 1 )
> . It can be rewritten to
> 
> --creating new scope
> ...
> --fixing parameter values in new scope
> R: Ring == Fraction Integer;
> a: R == 1;
> b: R == 1;
> 
> --entering function body
> if R has Field then
> {
>     a / b;
> } else {
>     a * b;
> }
> 
> which connects it to our discussion. So I guess the fact "B having CatB" 
> is essential!

Nice. And I agree, but the point is if you say

X: Ring == Fraction Integer;
func(X, 1, 2);

or

X: Ring == Fraction Integer add;
funct(X, 1, 2);

probably makes a difference. In the first case I'd expect 1/2, in the 
second 2 as a result. Don't you agree?

> But why is "H has CatB" false?
> I (now) like that as well. So the add is kind of a "forget" operator.
> It allows you to chop off parts of a domain you do not need--or would 
> break the semantics.
> AdditivieButNotArithmeticInteger: AdditiveType == Integer add;
> 
> Then AdditivieButNotArithmeticInteger is not of type ArithmeticType.

Exactly. And that is perfectly fine, since it is exactly what you had 
written.
You explicitly declared a (new) domain AdditivieButNotArithmeticInteger 
to just export AdditiveType.

Without the "add" the exports would be that of Integer at the time the 
compiler sees Integer (?). I don't know what type

MyInt: AdditiveType == Integer;

would have if it is declared with just libaldor in scope and you later 
use it with libalgebra in scope. Remember that libalgebra "extend"s 
Integer with a few more signatures.

I am missing a clear definition of statements like for "MyInt" above.

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

> It's not a bug; it's a feature.

If it's a feature then
     it's a bug in the documentation
     or
     I am to blind to find it properly documented.

>>> 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?
> 
> I do not see a difference between 2 and 3. That is the point. I also do 
> not see a difference between "Domain" and "Domain add". Both are domains 
> (However different ones of course, just as 2 is not equal to 3).

Oh. Your point of view is interesting. "Domain" and "Domain add" are 
different domains. Hmmm, thinking about it, I must somehow agree, the 
"add" probably does something like "_copy_(Domain)" (funny syntax!), it 
creates a new domain. But there is a little difference. You remember 
"add" creates a type context.

http://www.aldor.org/docs/HTML/chap7.html#3

>>>   Ident: Category == Domain;
>>>
>>> and
>>>
>>>   Ident: Category == Domain add;
>>>
>>> . Of course, "Domain" and "Domain add" are different things. No doubt
>>> about that. However, this differenc should be the only difference.
>>
>> 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).
> 
> So you mean the "Ident: SomeType == " part means two different things, 
> regarding whether "Domain" or "Domain add" follows?

That is what we are talking about. Otherwise you wouldn't have the behaviour

 >> B has CatB: T
 >> H has CatB: F

from the program aaa.as above. My question is whether

B has CatB: T

should be considered a bug in the compiler or a feature of the language.

>> ---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 (*)?
> 
> I'd consider that a bug in comparison of exports. Replacing your (*) 
> line by
> 
>   X: CatX == if true then (A at CatX) else (B at CatX);
> 
> gives a working program with output
> 
>   X has CatA: T
>   X has CatB: F
>   X has CatX: T
> 
> . So the problem (wild guess) is that the compiler Has problems with 
> seeing that the if statement gives CatX in both branches of the if 
> statement. Mainly because the types of A and B aro not equal. However, 
> you can hint the compiler. My code is telling him "The if part gives 
> CatX and the else part gives CatX". Then the compiler can infer, that 
> the whole "if" statement gives CatX. And it is at least the type of X 
> (which is CatX). So it matches.

COOL! So without the "add" the compiler gives X the type of what it sees 
on the right of "==". Now you declare that through "@CatX" to be CatX.
But, hey, why then you get

    X has CatA: T

??? That looks like cheating. So "A at CatX" in fact means consider A to be 
of type CatX (which it is anyway) but don't forget the true type of A 
(which is Join(CatX, CatA)). So the whole "@CatX" stuff, ist just to 
help the compiler to figure out that the "if" construction above yields 
something that has at least type CatX.

I am really not sure whether I like that. For me constructions like

X: CatX == Dom;

and

X: CatX == Dom add;

should (nearly) behave in the same way. In particular X should be 
something of type CatX and nothing more.

I said "nearly", because one might like to define something like

Tree: TreeCat == MyUnion(Node, MyCross(Tree, Tree)) add;

and for that the "type context" stuff would be necessary.

> However, your (*) with the "add"s tells the compiler to build two new 
> domains. This is not giving hints to the compiler, but forcing it to do 
> extra work and forcing it to produce extra code. However, due to the 
> add, it (probably) tries to cut off all parts of A and B, it does not 
> need. The compiler knows (due to the type CatX of X) that the "if" 
> statement has to be of CatX. Therefore, both branches of the "if" 
> statement have to provide CatX. So A is cut down to CatX and so is B.

I agree. Have you tried

X: CatX == (if true then A else B) add;

? That does not compile. I probably have to add "@CatX" as you did above.

>> I am actually a bit amazed that your program runs and gives expected
>> results. But what about...
>>
>> ---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
>>
>> 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?
> 
> Of course. Again, be nice to the compiler. He is old. He is buggy. He is 
> a bit rusty on the edges. And he is locked in, in a jail of non-free 
> source code. But help him. Do not force him to do extra work. Tell him 
> what you know, if he noods to be told.
> 
> X: CatX == if zero? #arguments then (A at CatX) else (B at CatX);
> 
> does the trick for me:
> 
> LC_ALL=C /opt/aldor/bin/aldor -M no-abbrev -C args=-Wopts=-m32 -Fx 
> -lalgebra -laldor aaa3.as && ./aaa3 && ./aaa3 xx
> cc1: note: -fwritable-strings is deprecated; see documentation for details
> cc1: note: -fwritable-strings is deprecated; see documentation for details
> TT
> FF

You were lucky. Of course, I had tried the "@" stuff. But my code was a 
little different and I ran into segfaults. I guess there are lots of 
problems hidden here.

>> 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.
> 
> I hope we both deem my solution to be "nice" :)

Yes, if I am not forced to write an extra "@CatX". The compiler should 
do that.

I hope all these mails about "A: CatA == Dom" are not too long.

Ralf