[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Ralf Hemmecke
Subject: Re: [Axiom-developer] Re: BINGO,Curiosities with Axiom mathematical structures
Date: Mon, 13 Mar 2006 14:33:34 +0100
User-agent: Thunderbird 1.5 (X11/20051201)

Consider for example '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 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", 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
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?

#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;


reply via email to

[Prev in Thread] Current Thread [Next in Thread]