[Aldor-l] exports and constants

[Christian Aistleitner]

On Fri, 21 Jul 2006 10:05:36 +0200, Ralf Hemmecke <ralf at hemmecke.de> wrote:

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

I fully agree. That's just the way i'd expect it. You probably wanted to  
show the implementation of the "add" statement demolishes established  
types. But I do not think so. The "add" may cut off fields from "Fraction  
Integer" not necessary for Ring. The fact that "Fraction Integer" is cut  
off, because it is not needed to be a Ring. If you need it, why don't you  
tell the compiler about it:
X: Ring == (Fraction Integer add)@Field;

With this line you again get 1/2 and you can add things in the add  
statement.

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

I have not enough experiences with "extend". I just used it.

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

I fully agree that the compiler does not match the user guide.

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

I think you could achieve such behaviour without "Ident: SomeType == "  
meaning two different things. You just need a clever "add" operator. The  
add operator has to be able to check which type is has to meet and can  
then cut off accordingly.


  My question is whether
>
> B has CatB: T
>
> should be considered a bug in the compiler or a feature of the language.

I'd go for the feature. Otherwise, I'd go bananas.

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

Because the type of A has CatX and CatA. X has the same dynamic type as  
A--CatX and CatA. But X has a different, static type, which is CatX  
WITHOUT CatA.

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

Ja.

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

Ja. But hopefully the need to @CatX goes away in future versions of the  
compiler. That's a weakness of the compiler to determine the type a.k.a. a  
bug.

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

This would render has useless, because X cannot have any further thing  
than CatX.
The if R has Field in

func( R: Ring, ... ):() == {
   if R has Field then
   {
      ...
   }
}
would always be false. You really want that? I don't.


--
Kind regards,
Christian