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

[Ralf Hemmecke]

> Consider for example 'DirectProductCategory'
>
> http://wiki.axiom-developer.org/axiom--test--1/src/algebra/VectorSpad/tangle
> ?submit=tangle&chunk=category+DIRPCAT+DirectProductCategory
>
> It's paramters are:
>
>   DirectProductCategory(dim:NonNegativeInteger, R:Type)
>
> but 'dim' does not appear in the signatures of the list of exports
> as one can verify with:
>
>   ')sh DIRPCAT
>
> In fact 'dim' only to the right of the == some default functions
> such as 'dimension' and 'size'.
>
> One might predict using your analysis above that 'DIRPCAT(2,INT)'
> and 'DIRPCAT(3,INT)' would be treated identically. But try this:
>
> (1) -> DIRPROD(2,INT) has DIRPCAT(2,INT)
>
>    (1)  true
>    Type: Boolean
>
> (2) -> DIRPROD(2,INT) has DIRPCAT(3,INT)
>
>    (2)  false
>    Type: Boolean
>
> -------
>
> How does Axiom know that (2) is false?

Because Axiom tries to be smart. It uses information it does not have.

And the behaviour above is not inherent to the interpreter. Otherwise 
the following function call "foo()" would not return "true+false".

Look further below and you find that dirprod.spad and dirprod.as are 
programs where the spad and the aldor compiler produce code with 
different semantics. TOO BAD!!!


-- begin dirprod.spad
)abbrev domain MYDOM MyDom
)abbrev category MYDPC DirProdCat
)abbrev domain MYDP DirProd

DirProdCat(n: Integer, R: Type): Category == with
  fst: % -> R


DirProd(n: Integer, R: Type): DirProdCat(n, R) == add
  Rep := List R -- dummy implementation
  fst(x: %): R == first(x pretend List(R))$List(R)

MyDom: with
  foo: () -> OutputForm
 == add
  foo(): OutputForm ==
    b2: Boolean := (DirProd(2, Integer) has _
      DirProdCat(2, Integer))
    b3: Boolean := (DirProd(2, Integer) has _
      DirProdCat(3, Integer))
    (b2::OutputForm) + (b3::OutputForm)
-- end dirprod.spad

Well, as I said at the bottom of my "explanation mail" 
http://lists.nongnu.org/archive/html/axiom-developer/2006-03/msg00097.html, 
 the information seems to be available also in a compiles Aldor 
library, but it is not used.

And in some way I would not really like it to be used, because then I 
would not understand the concept of a function application anymore.

So although the output of the following program might seem strange at 
first sight,

aldor -laldor -grun dirprod.as
2 has 2: T
2 has 3: T

it can be understood with my previous explanation.

If you look at DirProdCat as a function then clearly
  DirProdCat(2,Z) = DirProd(3,Z) = with{first:%->Z}
so why would one want another output?

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

define DirProdCat(n: Integer, R: Type): Category == with {
  first: % -> R;
}

DirProd(n: Integer, R: Type): DirProdCat(n, R) == add {
  Rep == List R; -- dummy implementation
  import from Rep;
  first(x: %): R == first(rep x);
}

main(): () == {
  macro Z == Integer;
  macro DP == DirProd(2, Z);
  import from Z;
  stdout << "2 has 2: " << (DP has DirProdCat(2, Z)) << newline;
  stdout << "2 has 3: " << (DP has DirProdCat(3, Z)) << newline;
}

main();
--------end dirprod.as