[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