[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## Re: [Axiom-developer] types as values

**From**: |
Ralf Hemmecke |

**Subject**: |
Re: [Axiom-developer] types as values |

**Date**: |
Mon, 26 Sep 2005 16:30:49 +0200 |

**User-agent**: |
Mozilla Thunderbird 1.0 (X11/20041206) |

But having defined the function tt2 in Aldor like this:
#include "axiom.as";
testtype2(): with {
tt2: (Integer) -> Type;
} == add {
tt2(x:Integer):Type == {
x=0 => Integer;
Float;
}
}
How can I use it in Axiom in a useful manner?

`tt2 returns a domain of type "Type". So in order to be useful it would
``be necessary to know which functions it exports. However, one cannot
``look into Type. Your function tt2 would perhaps be more interesting if
``its return type were a category with some neat functionality. For
``example, replace Type above by ArithmeticType. Now, at least you know
``what functions you could call on values of type tt2(0). Though you would
``probably still need functions to coerce a known value into tt2(0) and back.
`

For example,
if I write:
(1) -> n:tt2(0)
Axiom says:
"Category, domain or package constructor tt2 is not available"
which is true of course because it is 'testtype2' which is
the name of a **domain**. But even if I this:
(2) -> intx := tt2(0)
(2) Integer
Type: Type
(3) -> a:intx
intx is not a valid type.

`I have the impression that the result of (2) is misleading. Axiom prints
``"Integer" and its type is correctly "Type". This is, of course,
``different from the real Integer domain whose type is
`
Integer: Join(IntegerNumberSystem, ConvertibleTo String, OpenMath) with
random : % -> %
++ random(n) returns a random integer from 0 to \spad{n-1}.
canonical
++ mathematical equality is data structure equality.
canonicalsClosed
++ two positives multiply to give positive.
noetherian
++ ascending chain condition on ideals.
infinite
++ nextItem never returns "failed".
The "Integer" from (2) is the same as MyInt in
MyInt: with == Integer;
it has no exports. I am not really sure whether
MyInt: Type == Integer;

`should be allowed to compile. Who could tell just from the left side of
``the == sign whether MyInt is a domain or a category?
`
Ralf