[Aldor-l] semantics of has

[Martin Rubey]

"Stephen Watt" <watt at scl.csd.uwo.ca> writes:

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

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

well, you guessed right anyway...
 
> 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.

great!

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

wonderful!

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

superb!

I must say, I admire the design of Aldor.  Congratulations to those
responsible :-)

Now, it remains to fix that bug.  Any chance?  Actually, in FriCAS it seems to
be mostly working, mostly, because, after

-------------------------------------------------------------------------------
)abbrev category MYM MyMonoid
MyMonoid(T: Type, op: (T, T) -> T): Category == SetCategory

)abbrev category MYA MyAddMonoid
MyAddMonoid: Category == with 
        _+: (%, %) -> %
        MyMonoid(%, _+$%)

)abbrev domain MINT MyInteger
MyInteger: MyAddMonoid == Integer 
-------------------------------------------------------------------------------

MyInteger has MyMonoid(MyInteger, _+$MyInteger)

gives false...


Martin