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

[William Sit]

Stephen Wilson wrote:

> Lifting everything to the package level is an example of how one will
> rapidly diverge from the math. For example, what if instead of a
> functor `PPF(n:PositiveInteger)==PrimeField(n) with ...' we want
> something more general, like, say, given any commutative ring R and a
> maximal ideal M in R we want the quotient field R/M. In a package
> like:
> 
>      RESCLASS(R: CommutativeRing, M: MaximalIdeal(R)): Field with ...
> 
> RESCLASS is going to need to know about *every* commutative ring in
> the algebra. If R is the integers, and M a prime < 2^32, then it needs
> to know the field can be represented as machine integers, for example.
> 
> But with dependent typing one can achieve this generality, since the
> required function is a categorical export, which each individual
> domain satisfies in its own way. It becomes possible to write
> extraordinarily generic algorithms given such a language facility.

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.  (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.) For a specific ring, such as the Integers, yes, we
know, and there you can implement an efficient R/M if you also know that M <
2^32.  But I do not follow how this has to do with signature issues.

> If you cant
> write foo(n:INT):PrimeField(n), then programmers will define functions
> like mod_+(arg1:INT,arg2:INT,modulus:INT):INT and throw away the
> mathematical meaning of their types. Might as well be programming in
> C ( almost :).

The solution I proposed in package FOO:

> --%Foo
> )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)
> 
> )abbrev package BARTEST Bartest
> Bartest: T==C where
>    T == with
>         barrun: () -> Void
>    C == add
>         import FOO
>         barrun() == 
>           for k in 4..5 repeat
>             for n in [1,2,4,6]::List PositiveInteger repeat
>               print(point()$Foo(n+1,k)::OutputForm)$PrintPackage

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.

If one MUST use the signature for g (other than it is convenient), then you need
Aldor. But can someone supply such an example from Aldor?

William