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

[Stephen Wilson]

William,

On Fri, Jan 14, 2005 at 11:50:51AM -0500, William Sit wrote:
> I am not following your example. RESCLASS is already a domain constructor and
> dependent types for domain constructor is not a problem in Axiom. Since 
> RESCLASS
> is a categorical construct, the implementation must NOT know anything about R 
> or
> M other than that R is a commutative ring and M is a maximal ideal of R.  

Yes, I realize that this is already possible in axiom. My apologies,
I miss-wrote the the RESCLASS example. I hope what I write below will
be a bit clearer. 

> (By the way, MaximalIdeal(R) is also a categorical domain construction and I 
> wonder
> how one can characterize algorithmically the set of maximal ideals of an
> arbitrary commutative ring.) 

I know :) I wonder this too. Just wishful thinking I guess :)

> does not sacrifice the mathematical type structure of the original example 
> that
> Martin proposed:
> 
>    g(n:PositiveInteger, k:PositiveInteger):PrimeField(n)
> 
> It reflects exactly the same structure with the exception that there is no
> signature used and g(n,k) is replaced by the longer name 
> point()$Foo(n,k) as illustrated in the Bartest package. I do admit that Aldor 
> is
> nicer to allow that, so that such a wrapper is not necessary. But the wrapper 
> is
> straightforward and general and can even be automated.
> ...
>  But can someone supply such an example from Aldor?

The following is an example with a view towards generic modular
computations. Aldor has a category (approximately):

---------
 ModularComputation: Category == CommutativeRing with {
        residueClassRing: (p: %) -> ResidueClassRing(%,p);
        ....
 }
---------

So any domain satisfying Modular computation is a CommutativeRing R,
which exports a function which takes a representative p of R and returns
something which satisfies ResidueClassRing(R,p).

---------
ResidueClassRing(R: CommutativeRing, p: R): Category ==
   CommutativeRing with {
     modularRep: R -> %;
     canonicalPreImage: % -> R;
     if R has EuclideanDomain then {
       symmetricPreImage: % -> R;
       if R has SourceOfPrimes and prime?(p) then Field;
     } }
---------

Here we use the notion of SourceOfPrimes until someone figures out a
meaningful way to represent a MaximalIdeal generally:).

Aldor has an IntegerCategory, roughly:

---------
IntegerCategory: Category ==
    Join(IntegerType, CharacteristicZero, EuclideanDomain,
             ModularComputation, SourceOfPrimes,
             GeneralExponentCategory, Specializable, Parsable) with {
       ...
    default {
       residueClassRing(p:%):ResidueClassRing(%, p) == IntegerMod(%,p);
       ...
    } }
---------

And IntegerMod is an efficient implementation:

---------
   IntegerMod(Z:IntegerCategory, p:Z):ResidueClassRing(Z, p) == add { ... }
---------

Assuming this type of stuff is implemented in the library where it is
needed we can write very generic functions:

---------
   Foo(R: ModularComputation): with { ... } == add {
       bar(r: R, p:R): R == {

         elem : ResidueClassRing(R, p) := modularRep(r)$residueClassRing(p)
         
         -- hairy computation...

         canonicalPreImage(elem)
       } }
---------   


All of this depends on the fact that we can express a dependently
typed function residueClassRing(p:R), which can be implemented by any
given domain as appropriate. The Foo package knows all it needs to,
the Ring, and an element of the ring to get at the the quotient
ring. Of course, the bar function above could be more complex and
return an element of ResidueClassRing(R,p), etc.

How could one write the bar()$Foo above with the current axiom
language? All you can do is write a package/domain parameterized by a
commutative ring R and a representative of R, and write the exports
dependently on R's type via `if R has ...'  constructs. This is what
I meant in the previous email about having a RESCLASS package/domain
which needed to know too much about the algebra.


Sincerely,
Steve