Re: [Axiom-developer] Re: [Aldor-l] RE: Axiom domains and Aldorreturntypes

[Martin Rubey]

William Sit writes:

 > The idea is: Since in creating domains, we are in effect creating a
 > function(the domain constructor PPF is a function of sort, or functor) and
 > the compiler can take dependent types in its signature, structurally:

 >   PPF(n:PositiveInteger)==PrimeField(n) with foo

 > so it should be able to compile something like g by lifting it to the
 > package level.
 > 
 > So here is another way using package.
 > 
 > )abbrev package FOO Foo
 > Foo(n:PositiveInteger, k:PositiveInteger):T==C where
 >   T == with
 >        point:()->PrimeField(n)
 >   C == add
 >        point()==k::Integer::PrimeField(n)
 > 
 > After compiling, we can use
 > 
 >   point()$Foo(n,k)
 
Yes, this is the "good" way. Marcus, maybe you want to try this? In fact, the
signatures of the functions in a package may depend in complicated ways of the
parameters of the package. I posted the following example to axiom-math
recently:

)abbrev domain BAR Bar
Bar(p:Integer): Exports == Implementation where
  Exports == Join(FiniteFieldCategory,FiniteAlgebraicExtensionField($),_
    ConvertibleTo(Integer))

  Implementation == InnerPrimeField(nextPrime(p)$IntegerPrimesPackage(Integer)_ 
                                    pretend PositiveInteger)

William: Marcus has an excellent example where things like this are needed: He
wants to define a function as follows:

> I am trying to do the following, which is a common procedure when dealing
> with Artin-Schreier extensions:
> 
> 1. Input is a Laurent series f with coefficients in a field K of
> characteristic p>0. If f satisfies one of the following conditions:
> A.  f has no terms with negative order, or
> B.  the leading term of f is of order -m where m>0, and m is not 
>     divisible by p,
> then stop and return f.
> 
> 2. Otherwise we can find a p-th root of the leading coefficient of f in a
> suitable extension field L of K, and hence a monomial w such that f + w^p - w
> has a pole of smaller order than f.
> 
> 3. Replace f by f+w^p-w and K by L, and go back to 1.
> 
> So I am trying to do a sequence of field extensions of K.
> 
> The result will be a Laurent series over one of these repeated extensions,
> which I would like to return.

Martin