[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 "";
testtype2(): with {
    tt2: (Integer) -> Type;
} == add {
    tt2(x:Integer):Type == {
      x=0 => Integer;

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}.
      ++ mathematical equality is data structure equality.
      ++ two positives multiply to give positive.
      ++ ascending chain condition on ideals.
      ++ 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?


reply via email to

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