[Top][All Lists]

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

[Axiom-developer] Axiom domains and Aldor return types

From: Page, Bill
Subject: [Axiom-developer] Axiom domains and Aldor return types
Date: Wed, 12 Jan 2005 08:08:17 -0500


I have been thinking about your example code.

On Tuesday, January 11, 2005 9:44 AM you wrote:
> ... 
> I just tried another example, which is in fact the reason
> why I would love to have Aldor working. I did not expect
> it to work, and it does not, but it works *almost*. The
> code is as follows:
> #include "axiom"
> Test: with { f: (n: PositiveInteger) -> PrimeField(n) } 
>    == add { f(n: PositiveInteger): PrimeField(n) == 
>               10::Integer::PrimeField(n) }
> Note that such a construction -- the resulting domain 
> depending on the function parameter -- is currently
> illegal in Axiom. In Aldor it is fine.

I don't really understand when the use of parameterized
return types on functions would be useful. What information
is being returned as part of the type of the result that
is not already known because of it's value?

As I see it the concept does considerable damage to the
notion of the 'domain' of a function. How should we interpret
the expressioin `PrimeField(n)' when n is unknown? Does it
represent the Union over all values n? We can no longer
write the signature of a function in the simple form:

  f: PositiveInteger -> PrimeField

Can you explain again why you don't find the usual Axiom
solution to this situation acceptible? I.e. the use of
the `Any' domain:

 f(n) == n::PrimeField(n)

Perhaps in some cases the use of a Union might even be

   PrimeField(5), ...)
 f(n) == n::PrimeField(n)

The union allows a 'case' construction like this:

  f(3) case PrimeField(3)

In fact this sort of thing works in Axiom:

(1) -> f:PositiveInteger->Union(PrimeField(2),PrimeField(3), _
  f(n) ==  ( prime? n and n<=7 => n::PrimeField(n); "Failed")

   Function declaration f : PositiveInteger -> Union(PrimeField 2,
      PrimeField 3,PrimeField 5,PrimeField 7,Failed) has been added to
                                                      Type: Void
(2) -> f(2)
   Cannot compile conversion for types involving local variables. In
      particular, could not compile the expression involving ::
      PrimeField #1
   AXIOM will attempt to step through and interpret the code.
   Compiling function f with type PositiveInteger -> Union(PrimeField 2
      ,PrimeField 3,PrimeField 5,PrimeField 7,Failed)

   (2)  0
                                    Type: Union(PrimeField 2,...)
(3) -> f(3)

   (3)  0
                                     Type: Union(PrimeField 3,...)
(4) -> f(4)

   (4)  Failed
                                           Type: Union(Failed,...)
(5) -> f(5)

   (5)  0
                                     Type: Union(PrimeField 5,...)

(6) -> x:=f(5)

   (6)  0
                                     Type: Union(PrimeField 5,...)

(7) -> x case PrimeField(5)

   (7)  true
                                                    Type: Boolean
(8) -> x case PrimeField(3)

   (8)  false
                                                    Type: Boolean


Bill Page.

reply via email to

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