[Axiom-developer] Axiom domains and Aldor return types

[Page, Bill]

Martin,

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:PositiveInteger->Any
 f(n) == n::PrimeField(n)

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

 f:PositiveInteger->Union(PrimeField(2),PrimeField(3),
   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), _
  PrimeField(5),PrimeField(7),"Failed")
  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
      workspace.
                                                      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
etc.

-------

Regards,
Bill Page.