[Aldor-l] semantics of has

[Stephen Watt]

Hi Martin.   Answers, or at least responses, below following =====s  -- Stephen

On Sat, Aug 16, 2008 at 11:03 AM, Martin Rubey
<martin.rubey at univie.ac.at> wrote:
> 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.
=============================
Sorry, I don't understand what you are asking here.

If we have

   define C(a:T): Category == ...
   D: C(e) == add ...

then D has the export %%: C(e) and the test   D has C(e)  can be done
by looking up the single export %%: C(e).   This should be
independent, e.g., of whether T is Integer or Ring.

>
> 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)
===================================

SquareMatrix(2, Integer)  has SquareMatrixCategory(2, Integer) should
succeed but NOT the above, supposing

   SquareMatrix(n: Integer, R: Ring): Join(SquareMatrixCategory(n, R),
....) ==  add ..

because the n gets substituted with 2.  So this returning TRUE is a bug.

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

===========================
In the Aldor type system, this would be disallowed.

>
> 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();
>
> -------------------------------------------------------------------------------
>
>
>