Re: [Axiom-developer] "has" and "with" and bug

[Ralf Hemmecke]

On 08/13/2007 05:18 PM, William Sit wrote:
> Ralf Hemmecke wrote:
>
> > 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.
>
> Why does that surprise you? Even though rhx is not exported,
> it is recorded as part of |catExports|, because according to your
> quote from AUG:
>
> > 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.

OK, but MDom is different. I defined

MDom: MMM with {
  ans: (with {foo:()->(); bar:()->()}) -> ();
} == add { ... }

And this construction says that the type of MDom is

  MMM with {ans: (...) -> ()}

where

MMM: Category == with {
  foo: () -> ();
  bar: () -> ();
}

Do you see "rhx" there? So MDom does not export rhx. It simply does not 
matter what "add {...}" exports. The type of the "add {...}" 
construction must implement foo, bar, and ans, that would be enough.

In the file I gave, the type of "add {...}" exports rhx, MDom doesn't.

Ralf