Re: [Axiom-developer] types as values

[Ralf Hemmecke]

> 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