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

[Ralf Hemmecke]

Unfortunately, I've sent this mail only to Martin, so here it comes to 
axiom-developer together with an explanation of why there is this 
strange output.

(Well, that is my interpretation. I might be wrong so if anybody with 
more inside into the internals is on the list, feel free to correct me.)

Here you go...
---------------------------------------------------
On 03/09/2006 05:08 PM, Martin Rubey wrote:
> I am satisfied now:

Believe me, you are not.

Unfortunately, my Axiom now gives me the error message

(1) -> Integer has MyMonoid(Integer, *)

   >> System error:
   Cannot open the file 
/home/hemmecke/software/Axiom/mnt/linux/aldor/lib/runtime.o.

,.. so I demonstrate it with pure Aldor.

Basically, if you replace "ArithmeticType" by "Ring" it should work with
  #include "axiom"
and inside Axiom.

-- mymonoid.as
#include "aldor"

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

MyInteger: ArithmeticType == Integer add;
extend MyInteger: MyMonoid(MyInteger, *$MyInteger) == add;
extend Integer: MyMonoid(Integer, *$Integer) == add;
-- end mymonoid.as

--mymonoidtest.as
#include "aldor"
#include "aldorio"
#library MyMon "mymonoid.ao"
import from MyMon;
macro {
    Z == Integer;
    M == MyInteger;
}
main(): () == {
  stdout << "1: " << (Z has MyMonoid(Z, *$Z)) << newline;
  stdout << "2: " << (Z has MyMonoid(Z, +$Z)) << newline;
  stdout << "3: " << (M has MyMonoid(M, *$M)) << newline;
  stdout << "4: " << (M has MyMonoid(M, +$M)) << newline;
}
main();
--end mymonoidtest.as

Compile with

aldor -fo -fao mymonoid.as
aldor -grun -laldor mymonoidtest.as mymonoid.o

and try to explain the output.

1: T
2: T
3: T
4: T

It's clear, isn't it?

Ralf
---------------------------------------------------

OK, and now the explanation. One would like the output (T, F, T, F), rigth?

Now look at MyInteger. It has type

with {
  ArithmeticType; -- includes +, *, 0, 1
  MyMonoid(MyInteger, *$MyInteger);
}

Well, but MyMonoid is a **function**. So the type is (nearly)
with {
  ArithmeticType;
  square: MyInteger -> MyInteger;
  default {square(t: MyInteger): T == (*$MyInteger)(t, t)}
}

You see, the * is hidden behind the == sign. The actual exports are that 
of ArithmeticType together with "square". It should be clear that then
2 and 4 from above also return true.

HOWEVER, remove the line

  extend Integer: MyMonoid(Integer, *$Integer) == add;

and try to compile "aldor -fasy mymonoid.as". Then look at the generated 
"mymonoid.asy". Look at the exports of |MyInteger|. Under |domExports| 
right at the bottom of the file, we find

        (|Declare|
          %%
          (|Apply| |MyMonoid| |MyInteger| (|Qualify| * |MyInteger|))
          ((|default| . 1)
            (|symeNameCode| . 51482908)
            (|symeTypeCode| . 366734318)))

That's interesting. The compiler would have a way to tell
that "MyInteger has MyMonoid(MyInteger, +$MyInteger)" is false.

Can someone explain that compiler design?

Well, mathematically thinking, I would say that (T, T, T, T) is OK, 
since "MyMonoid(Z, +$Z)" stands for the value that MyMonoid gives when 
applied to the arguments Z and +. There would be no way to guess the 
arguments from the value.

Well, this discussion is getting more and more into the internals...
I hope we all learn from that.

Ralf