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

[Christian Aistleitner]

Hello,

as this reply is only about the sample Aldor code, I stripped the CCs to  
the Axiom List and the Axiom people.

On Mon, 13 Aug 2007 13:36:53 +0200, Ralf Hemmecke <ralf at hemmecke.de> wrote:

> So let's do something in Aldor. "add" has to be replaced by "default",
> but this way it does not demonstrate what I wanted to show.
> Let's compile and run the program below.
>
> woodpecker:~/scratch>aldor -laldor -grun aaa.as
> has with {foo: ()->()} = T
> has with {bar: ()->()} = T
> has with {rhx: ()->()} = T
> has with {foo: ()->()} = T
> has with {bar: ()->()} = T
> has with {rhx: ()->()} = T
> MDom has rhx? T
>
> Ooops. I must say that is surprising. MDom exports foo, bar, ans, but
> not rhx.

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


I am sure you'd have expected to see "F" instead of the "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".

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

 From my point of view, "has" does not violate it's specification (Section  
7.9 in the AUG. Page 96).
But the specification is not too tight. So your interpretation of "has"  
would meet its specification as well.

With this knowledge of "has", I'd argue that what you experienced can be  
properly explained without assuming the Aldor compiler violates the Aldor  
specification of AUG.

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.

No problem with passing add parts or anything. Just plain "has" quirks.

Kind regards,
Christian

P.S.: Since the original posting is some days old, allow me to reproduce  
Ralf's original code:

> ---BEGIN aaa.as
> #include "aldor"
> #include "aldorio"
>
> Blah(S: with {foo:()->()}): with {
>      blahfoo: ()->Boolean;
>      blahbar: ()->Boolean;
>      blahrhx: ()->Boolean;
> } == add {
>    blahfoo(): Boolean == S has with {foo: ()->()};
>    blahbar(): Boolean == S has with {bar: ()->()};
>    blahrhx(): Boolean == S has with {rhx: ()->()};
> }
>
> MMM: Category == with {
>    foo: () -> ();
>    bar: () -> ();
> }
>
> MDom: MMM with {
>    ans: (with {foo:()->(); bar:()->()}) -> ();
> } == add {
>    foo(): () == {
>      stdout << "has with {foo: ()->()} = " << blahfoo()$Blah(%) <<  
> newline;
>      stdout << "has with {bar: ()->()} = " << blahbar()$Blah(%) <<  
> newline;
>      stdout << "has with {rhx: ()->()} = " << blahrhx()$Blah(%) <<  
> newline;
>    }
>    bar(): () == {}
>    rhx(): () == {}
>    ans(S: with {foo:()->(); bar: ()->()}): () == {
>      stdout << "has with {foo: ()->()} = " << blahfoo()$Blah(S) <<  
> newline;
>      stdout << "has with {bar: ()->()} = " << blahbar()$Blah(S) <<  
> newline;
>      stdout << "has with {rhx: ()->()} = " << blahrhx()$Blah(S) <<  
> newline;
>    }
> }
>
> main(): () == {
>    foo()$MDom;
>    ans(MDom)$MDom;
>    stdout << "MDom has rhx? " << (MDom has with {rhx: ()->()}) <<  
> newline;
> }
> main();
> ---END aaa.as