[Axiom-developer] Re: Axiom domains and Aldor return types

[Martin Rubey]

Dear Bill,

Page, Bill writes:

 > > #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?

The above is an example. Perhaps, more convincing:

Foo: with { g: (n: PositiveInteger, k: PositiveInteger) -> PrimeField(n) } 
   == add { g(n: PositiveInteger, k: PositiveInteger ): PrimeField(n) ==     
              k::Integer::PrimeField(n) }              
 
Another example is Marcus Better's problem, more examples are in
expr2ups.spad, where Any is used a lot. The type tells you in what domain to
interpret the value. But sometimes, the type will have to depend on a parameter
of the function, as above.

 > 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

Yes you can: Aldor does it. The signature is

   f: (n: PositiveInteger) -> PrimeField n

 > 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)

Because you cannot use it in compiled code and because you are using all of the
type information, which is the main point of Axiom. Of course, the example you
just gave doesn't make any sense, the result is always zero, but given the
function

Bar: with { h: (n: PositiveInteger, k: PositiveInteger) -> Any } 
   == add { g(n: PositiveInteger, k: PositiveInteger ): Any ==     
              k::Any }

you cannot use this function in compiled code anymore. The interpreter can deal
with it, not the compiler.

Look at Marcus code for a really convincing example: He wants to construct
recursively an algebraic extension of a ring, adding elements one at the
time. At the end of the process he wants to return an element of the final
ring. It is tricky to do this in Axiom currently.

Note, for example, if you have a signature

  f: Integer -> Any

but really, f returns a SimpleAlgebraicExtension of some ring, you cannot do
any calculations with the result in compiled code anymore, unless you know
*exactly* the defining polynomial of the ring.

So one way out -- in this specific case -- would be to return a record
containing the result of type Any and the defining polynomial. I hope you admit
that this is ugly.

Martin