[Axiom-developer] Re: BINGO, Curiosities with Axiom mathematical structures

[Martin Rubey]

Dear all,

as Ralf pointed out to me, my construction does have a problem in current Aldor:

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

#include "axiom"

MyMonoid(T: Type, m: (T, T) -> T): Category == with {
   monoidSquare: T-> T;
   default {monoidSquare(t: T): T == m(t, t)}
}

MyWord: with { 
   coerce: String -> %;
   c:(%, %) -> %;
   d:(%, %) -> %
}
   == add {
   Rep == String;
   import from String;
   coerce(a: String): % == per(a);
   c(a: %, b: %):%  == coerce(concat(rep(a), rep(b))$String);
   d(a: %, b: %):%  == a }

import from MyWord;
extend MyWord: MyMonoid(MyWord, c) == add;

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

(3) -> MyWord has MyMonoid(MyWord, c)

   (3)  true

(4) -> MyWord has MyMonoid(MyWord, d)

   (4)  true

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

Unfortunately, this messes everything up. However, I think that this problem
should be correctable.

There is a related, more serious problem, I overlooked, namely with multiple
inheritance. To make things clearer, I continue the example from above -- even
though it does not work the way I intended.

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

MyInteger: Category == with {
   +: (%, %) -> %;
   *: (%, %) -> %;
} == add { bla bla 
}

   (a: %) ^ (b: NonNegativeInteger): % == monoidPower(a, b }

import from MyInteger;
extend MyInteger: MyMonoid(MyInteger, +) with {   
  double: % -> %; }
== add {
  double(a:%): % == monoidSquare(a); }

extend MyInteger: MyMonoid(MyInteger, +) with {   
  square: % -> %; }
== add {
  square(a:%): % == monoidSquare(a); }


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

The good news: we do have our natural notation back. Instead of "double", we
would have "*", instead of "square" we would have "^" and instead of
"monoidSquare" we would have "monoidPower" in real life, of course. I.e., in
the base category, names of derived operations would have to be generic, since
the will be available in all domains that stem from this category, and it would
be very strange to have some additive structure, but having to use "square" for
doubling. I think the name "monoidSquare" is just good enough, although one
could maybe think of a better name.

Now the (very) bad news (indeed):

Since MyInteger is derived from MyMonoid, "monoidSquare" will be available. But
what will it do? Well, in fact, this construction is not even allowed
currently:

Bottom of Page 120 of the Aldor User Guide says:

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

  If two extensions have intersecting categories, then they may not be imported
  in the same scope.

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

I do have an idea, but this will obviously involve changes in the
language. What I'm thinking of is as follows. Instead of having to extend the
domain, we should be allowed to write:

-------------------------------------------------------------------------------
MyWord: with { 
   coerce: String -> %;
   c:(%, %) -> %;
   d:(%, %) -> %;
   MyMonoid(%, c)
}
   ==  add {
   Rep == String;
   import from String;
   coerce(a: String): % == per(a);
   c(a: %, b: %):%  == coerce(concat(rep(a), rep(b))$String);
   d(a: %, b: %):%  == a }
-------------------------------------------------------------------------------

Currently this yields: 
  Compiler bug...Bug: gen0Syme:  syme unallocated by gen0Vars

Finally, if we have two colliding signatures, none of them should be exported
"directly". i.e, given

-------------------------------------------------------------------------------
MyStruc: with { 
   coerce: String -> %;
   c:(%, %) -> %;
   d:(%, %) -> %;
   MyMonoid(%, c);
   MyMonoid(%, d)
}
-------------------------------------------------------------------------------

monoidSquare(x)$MyStruc 

would yield an error. Instead, 

if MyStruc has MyMonoid(MyStruc, c) then 
  newop(a:%):% == monoidSquare(a)

would work, and yield the monoidSquare from MyMonoid(MyStruc, c).


(In fact, I do believe that similar problems would arise if we were to follow
Nicolas Doye.)

Martin