[Aldor-l] semantics of has

[Martin Rubey]

Martin Rubey <martin.rubey at univie.ac.at> writes:

> Stephen, I think you said at the workshop that "has" would actually check
> 
> * the explicit exports
> 
> * plus the implicit export %% (actually, one for each category from which the
>   category inherits).
> 
> Now, what I do not understand: how much information does this implicit export
> %% contain?  From the example below, one might come to the conclusions that
> "type parameters" are implicit, while "values" aren't.

I thought I'd send two examples which makes my intent a little clearer, see
below.  (one of them is due to Ralf, and has been discussed before)

I meanwhile also realized (actually, recalled) that there is the fundamental
problem of equality of parameters and the possibility of multiple instantiation
of domains.

Oh yes, and meanwhile (i.e., a few hours later) I also digged up the old
threads, along with interesting contributions by Christian Aistleitner and you,
mainly:

http://lists.nongnu.org/archive/html/axiom-developer/2006-05/msg00204.html

(Trying to summarise: expressions in type context must contain only names that
are constant over the scope in which the type occurs.  If two "expanded type
expressions" obtained by fully resolving each type etc. are syntactically
equal, then their types are statically equivalent.)

So, if I understand correctly, this allows me to write

a: SquareMatrix(2, Integer) := ...
b: SquareMatrix(2, Integer) := ...
a+b

and reject

a: SquareMatrix(2, Integer) := ...
b: SquareMatrix(3, Integer) := ...
a+b

(given appropriate definitions)
-------------------------------------------------------------------------------

However, I still do not understand, why 

  SquareMatrix(2, Integer) has SquareMatrixCategory(3, Integer)

Wouldn't "syntactically equal" apply here, too?  Moreover, I actually do not
understand what "syntactically equal" really means.  Would

a: SquareMatrix(2^100, Integer) := ...
b: SquareMatrix(2*2^99, Integer) := ...
a+b

be allowed (well, theoretically, of course :-) -- after all, we cannot
guarantee that the two numbers are the same.  I guess (actually, hope) not.

It would be great to understand that.  And even better, to know that

  SquareMatrix(2, Integer) has SquareMatrixCategory(3, Integer)

returning true would be a bug that could be fixed...

Many thanks, (and good luck with the licensing talks)

Martin

----------- dirprod.as
#include "aldor"
#include "aldorio"

define DirProdCat(n: Integer, R: Type): Category == with;

DirProd(n: Integer, R: Type): DirProdCat(n, R) == add {
}

main(): () == {
   macro Z == Integer;
   import from Z;
   stdout << "2 has 2: " << (DirProd(2, Z) has DirProdCat(2, Z)) << newline;
-- gives T
   stdout << "2 has 3: " << (DirProd(2, Z) has DirProdCat(3, Z)) << newline;
-- gives T, but I'd prefer F
}

main();
--------end dirprod.as
---------- trying to implement general monoids---------------------------------
define MyMonoid(T: Type, op: (T, T) -> T): Category == with;

define MyAddMonoid: Category == with {
        +: (%, %) -> %;
        MyMonoid(%, +);
}

define MyMulMonoid: Category == with {
        *: (%, %) -> %;
        MyMonoid(%, *);
}

MyInteger: MyAddMonoid with {
        *: (%, %) -> %;
        } == Integer add;

main(): () == {
        import from Integer, Character, TextWriter, Boolean;

        stdout << (MyInteger has MyAddMonoid)@Boolean << newline;
-- gives T
        stdout << (MyInteger has MyMulMonoid)@Boolean << newline;
-- gives F
        stdout << (MyInteger has MyMonoid(MyInteger, +$MyInteger))@Boolean << newline;  
-- gives T
        stdout << (MyInteger has MyMonoid(Integer, *$Integer))@Boolean << newline;          
-- gives F
        stdout << (MyInteger has MyMonoid(MyInteger, *$MyInteger))@Boolean << newline;  
-- gives T, although I'd like it to give F
}
        
main();

-------------------------------------------------------------------------------