[Axiom-developer] Re: [Aldor-l] exports and constants

[Ralf Hemmecke]

>   Has expressions
>
>   A ``has'' expression has the following form:
>
>       dom has cat
>
>   where dom is a domain-valued expression, and cat is a category-valued
>   expression. A ``has'' expression may be used in any part of a program,
>   but is most often used to conditionalize domains and categories. The
>   result of the expression is a Boolean value which will be true if dom
>   can be shown to **satisfy** the category, and false otherwise.
>   ...
>   The evaluation of this expression is made at run-time, ...
>
> ** my emphasis. Type satisfaction is defined in section 7.7: 
>
>   "We say that a type S satisfies the type T if any value of type S can
>   be used in any context which requires a value of type T."

The compiler seems to have problems with that specification. I had a 
discussion about this with Antoine Hersen today.

---BEGIN aaa9.as
#include "aldor"
#include "aldorio"
define CatA(s: String): Category == with;
A(s: String): CatA(s) == add;
stdout << (A("x") has CatA("x")) << newline;
stdout << (A("y") has CatA("x")) << newline;
---END aaa9.as

>aldor -grun -laldor aaa9.as
T
T

Now let's replace
String <-- PrimitiveType
"x"    <-- String
"y"    <-- Integer

---BEGIN aaa10.as
#include "aldor"
#include "aldorio"
define CatA(s: PrimitiveType): Category == with;
A(s: PrimitiveType): CatA(s) == add;
stdout << (A(String)  has CatA(String)) << newline;
stdout << (A(Integer) has CatA(String)) << newline;
---END aaa10.as

>aldor -grun -laldor aaa10.as
T
F

I hope that someone agrees with me that this is a bit confusing.

We had a similar thing when we discussed about "Dom has Monoid(*, 1)".

Ralf