axiom-developer
[Top][All Lists]
Advanced

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

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


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

Martin,

On Wednesday, January 12, 2005 8:30 AM you wrote:
> Bill Page wrote:
> > 
> > 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) }              
>

Ok, I will work with this example. Yes, it is better.
  
> Another example is Marcus Better's problem, more examples
> are in expr2ups.spad, where Any is used a lot.

Ok.

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

That is still now clear to me, at least when it is possible
to use a Union.

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

That does not look like a *signature* to me. What is the
value of n? If you can't tell me, then how can I interpret
`PrimeField n'? A signature should specify the domains of
the function, but `PrimeField n' is not a domain until `n'
is replaced with some PositiveInteger. The only interpretation
of `PrimeField n' as a domain that I can think of would be
to claim that it represents some kind of Union over the
primes.

  Union(PrimeField n for n=1.. | prime? n)

But of course we can't write it quite this nicely right now
in Axiom...

This is similar to Axiom's insistence that

  A:Integer

can not be used in the expression

  A+1

until A is assigned a value. I this case I think it should
be ok to say that if A has no assigned value then it
represents the domain

  {+/-n for n=0..}
 
> > 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.

But as you said, `Any' is used extensively in expr2ups.spad.

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

I would write it something like this:

(2) -> h:(PositiveInteger,PositiveInteger)->Union( _
PrimeField(2),PrimeField(3),PrimeField(5),PrimeField(7))
                                                 Type: Void
(3) -> h(n,k)==k::PrimeField(n)
                                                 Type: Void
(4) -> x:=h(7,2)

   (4)  2
                                  Type: Union(PrimeField 7,...)
(5) -> trace x

   (5)  2
                                             Type: PrimeField 7
> 
> 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.

I will take a closer look at the emails from Marcus.

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

I agree that Any throws away too much information, except
in the interpreter where it tries to do a better job. But
I think even there Any is (usually) not a good choice for
the domain.

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

I agree that that is ugly. Using an explicit "streaming Union"
(iterator) domain would be my (future) choice. Unfortunately
for now:

(6) -> Union(PrimeField(i) for i in 1..10)
   Local variable or parameter used in type
   We will attempt to interpret the code.

   Category, domain or package constructor COLLECT is not available.
(6) -> Union(PrimeField(i) for i in 1..)
   Loading C:/Program Files/axiom/mnt/windows/algebra/UNISEG.o for
      domain UniversalSegment
   Loading C:/Program Files/axiom/mnt/windows/algebra/INCRMAPS.o for
      package IncrementingMaps
   Loading C:/Program Files/axiom/mnt/windows/algebra/ITUPLE.o for
      domain InfiniteTuple
   Loading C:/Program Files/axiom/mnt/windows/algebra/STREAM.o for
      domain Stream
   Local variable or parameter used in type
   We will attempt to interpret the code.

   Interpret-Code mode is not supported for stream bodies.
(6) ->

Regards,
Bill Page.




reply via email to

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