Re: [Axiom-developer] "has" and "with" (was curious algebra failure)

[Ralf Hemmecke]

Dear Bill,

You have added the Aldor version of the test code to

> | http://wiki.axiom-developer.org/AnonymousCategories

For test3()

    -- QQ is a category-valued constant
    define QQ:Category == with { +:(Integer,Integer)->Integer }
    ttest3():Boolean ==
      Integer has QQ

you say:  -- should be true

I don't agree with that. QQ is a (named) category (which you also could 
have defined outside. Domains belong to categories by assertion. You did 
not say

  extend Integer: QQ == add;

and QQ was not known before, so the aldor compiler is right to produce 
code that returns false.


I have some more comments on this thread.

A with B is (or should be) completely equivalent to:

   with {A; B}

(see Aldor User Guide). And perhaps that is also a hint to the 
named/unamed problem. What appears inside with will be recorded 
internally. Take the following file:

---BEGIN aaa.as
#include "aldor"
define QQ: Category == with {
        PrimitiveType;
        foo: MachineInteger -> ();
}
---END aaa.as

and say

aldor -fasy -laldor aaa.as

What you will get out, looks like

---BEGIN aaa.asy
((|Declare|
    qq
    (|Define|
      (|Declare| (|Label| qq ()) |Category|)
      (|With|
        |PrimitiveType|
        (|Declare|
          |foo|
          (|Apply| -> |MachineInteger| (|Comma|))
          ((|symeNameCode| . 314869119) (|symeTypeCode| . 626472089)))))
    ((|symeNameCode| . 51496308)
      (|symeTypeCode| . 624244337)
      (|catExports|
        (|Declare|
          =
          (|Apply| -> (|Comma| % %) |Boolean|)
          ((|symeNameCode| . 200102) (|symeTypeCode| . 21900315)))
        (|Declare|
          ~=
          (|Apply| -> (|Comma| % %) |Boolean|)
          ((|default| . 1)
            (|symeNameCode| . 51509389)
            (|symeTypeCode| . 21900315)))
        (|Declare|
          %%
          |PrimitiveType|
          ((|default| . 1)
            (|symeNameCode| . 51482908)
            (|symeTypeCode| . 34294859)))
        (|Declare|
          |foo|
          (|Apply| -> |MachineInteger| (|Comma|))
          ((|symeNameCode| . 314869119) (|symeTypeCode| . 626472089)))
        (|Declare|
          %%
          qq
          ((|default| . 1)
            (|symeNameCode| . 51482908)
            (|symeTypeCode| . 1066491663)))))))
(|Sequence|)
---END aaa.asy

Look in particular, inside (|catExports| ...). In addition to all 
exported functions you also find the exported symbol |PrimitiveType|. 
And you also find qq there.

What I believe "has" does, is to look inside the |catExports| and checks 
whether the symbol is there. If you say

  A has QQ

then it is enough to find QQ among the exports. For

  A has with {QQ; foo: () -> (); bar: Integer -> ()}

it has to find QQ and the foo and bar functions with the right signature.

I believe the "define" keyword in the current Aldor compiler has no 
effect. You can compile with and without it and the resulting C code is 
equal to the last bit. (At least in the cases that I have tested.)

Aldor does not allow

  A has "*"
  A has *

or anything else of the form

  A has B

where B is not of type Category. That seems to be different in Axiom, 
but I havent yet felt that this is insufficient.

Ralf