[Aldor-l] "has" and "with" and bug

[Christian Aistleitner]

Hello,

On Thu, 16 Aug 2007 10:58:45 +0200, Ralf Hemmecke <ralf at hemmecke.de> wrote:

>> What you experienced in your code is not related to "add", "with" or  
>> function calls passing strange values, but is related to the inner  
>> workings of the "has" construct.
>>  Just take a look at this code:
>>    #include "aldor"
>>    import from String, TextWriter, Character;
>>    Dom: with {
>>   } == add {
>>      privateFunc(): () == {}
>>   }
>>    main(): () == {
>>      stdout << "Dom has 'privateFunc' ? " <<
>>        (Dom has with {privateFunc: ()->()}) <<
>>         newline;
>>   }
>>   main();
>>   Here goes the output:
>> ____________________________________________
>> caistlei at ibis
>> cwd: /scratch/caistlei/ralf_type_context
>> $ aldor -Fx -laldor demo.as && ./demo
>> Dom has 'privateFunc' ? T
[...]
>> "has" checks whether or not a domain can satisfy the type you give. In  
>> the above example "the domain" is the whole "add" expression. This  
>> includes "privateFunc".
>
> Oh, sorry, here I disagree. Your code says
>
>    Dom has with {privateFunc: ()->()}
>
> and not
>
>    add {privateFunc(): () == {}} has with {privateFunc: ()->()}
>
> . The first should give F, the second T.

Ok, the second should give T. For the first, let's consider what dom is  
and how it relates to Aldor's treatment of domains/identifiers.
To me "Dom" is an identifier referring to the domain built by the "add"  
expression (i.e.:
   add {
     privateFunc(): () == {}
   }
). However, the types of Dom and the domain built by the add expressions  
do not necessarily have to match. The "type of Dom" maybe a subtype of the  
"type of the add expression" (thereby making some functions invisible).

So (I assume) we agree, that the type of the add expression is:

   with {
     privateFunc: () -> ();
   }

while the type of _identifier_ Dom is

   with {
   }

. Therefore, the identifier Dom only knows of the "with {}" part of the  
domain created by the "add" expression. The identifier does not know about  
the "privateFunc" within the domain created by the "add" expression.

To me, the "has" keyword provides a possibility to check a domain's (in  
contrast to an identifiers) type.

But let us assume, I am wrong, and what you describe is a bug. "has" can  
only be used to check the type of an identifier. "has" cannot check the  
domain, the identifier refers to.
Consider the following piece of code.

   f( R: Ring ): () == {
     if R has Field then
     {
       --do something
     } else {
       --do something else
     }
   }
   f( Fraction Integer );

Within the function call to f, "R" is an identifier referring to a  
domain--just as we had in the above piece of code.
The identifier "R" is of type Ring. Now "has" within f's body can only  
check the type of the identifier--not of the domain the identifier refers  
to. So especially "R has Field" has to by false regardless of the value of  
"R", as "R"'s type is Ring and cannot satisfy Field.

Assuming, I am wrong, and what you describe is a bug, the "correct"  
behaviour of "has" would turn it rather ... useless.



>> This observation relates nicely to the type of the domain. The type of  
>> the add expression is
>>    with {
>>     privateFunc: () -> ();
>>   }
>>  . However, this is not the type of "Dom". The type of "Dom" is
>>    with {
>>   }
>>  . That's what relates to
>>
>>> AUG Chp. 7.8:
>>>
>>>    The type of the expression A add B is C with { x1: T1; ...; xn: Tn }
>>>    where C is the type of A, and x1,...,xn are the symbols defined
>>>    (using ==) in B, whose types are T1,...,Tn, respectively.
>
>> But only because "Dom" hides "privateFunc" does not mean that it's  
>> stripped off completely. The "has" function allows to check whether or  
>> not "privateFunc" can be found withing the domain.
>> "has" does not allow you to check whether or not it is in "Dom".
>
> Again, I disagree. In
>
>    Dom has with {privateFunc: ()->()}
>
> the "add" part is missing, so "A add B" matches A with Dom and the type  
> of Dom is "with {}"

No. The paragraph (AUG 7.8) you originally cited is about creating  
domains. The code you now give is about _using_ not creating domains: In  
your line
>    Dom has with {privateFunc: ()->()}
there is no domain creation. There is just domain usage (by referring to a  
domain using the identifier Dom). Hence, there is no parsing towards "A  
add B" involved here. Furthermore, for domain creation, the "add" part is  
not optional--the "add" part cannot be omitted.


> So let's replace your line by
>
>      (Foo has with {privateFunc: ()->()}) <<
>
> and add another definition:
>
> Foo: with {} == Dom add;
>
> at the top of the file.
>
> According to the quote above, we now truely have that the type of
>
>    Dom add {}
>
> is
>
>    with {}
>
> right?

Yes. That's the part you see and can easily observe. Still, "privateFunc"  
is within the domain the identifier "Dom" refers to. The function  
"privateFunc" cannot be killed.

> Or mor exactly
>
>    (with {}) with {}
>
> in order to match the pattern C with { x1: T1; ...; xn: Tn } from the  
> quote.
>
> That is the same exports as for Foo.
> Still, main() prints "T".

Yes, because still a function "privateFunc" can be found. That's ok for me.

>> The problem with your code is that you use "has" to check for the  
>> presence of a function with an anonymous category. The function is  
>> present (althoug invisible), hence the anonymous category can be  
>> fulfilled, therefore you obtain "T".
>> I'd suggest to use named categories instead.
>
> That cannot have to do anything with named or unnamed categories.

Maybe, I misunderstood your original posting.
In the above paragraph, I wanted to stress, that testing for anonymous  
categories is dangerous.

Consider testing for "with { /:(%,%)->% }" and not testing for Field. That  
way, you cannot assume "/" really is a division function.

Kind regards,
Christian