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

[Stephen Wilson]

Bill, Martin, *

On Fri, Jan 14, 2005 at 12:10:45PM +0100, Martin Rubey wrote:
> Bill Page writes:
> 
>  > From a mathematical point of view I think this "signature limitation" in
>  > Axiom is natural and that Aldor goes too far in allowing a construction 
> like
>  > 
>  >   g(n:Integer,k:Integer):PrimeField(n)
>  > 
>  > when defining functions. The reason is that I do not see how it is possible
>  > to interpret PrimeField(n) as a domain in the normal ("categorical") sense,
>  > in this context where the value of n is not known.
> 
> I agree that the limitation looks natural. However, if you look closer at
> Aldors design, it couldn't be clearer.

I agree here with Martin. In my experience with aldor, the use of
dependent typing is very practical, very `close' to the math. It is
essential in many algorithms to move from one computational domain to
another which depends upon a result calculated at runtime. 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 :).


>  > > should be able to compile something like g by lifting it to the package
>  > > level.
> 
> 
>  > Yes! I think you are exactly right. And it is politically correct from the
>  > Axiom perspective to refer to this construction as a "functor". I think it
>  > is a *good thing* that Axiom's syntax encourages one to make this
>  > distinction.

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. 


> Aldor has been designed to be "cleaner" than Axioms internal language. Not 
> that
> much has changed, it seems that they were very careful, and it's quite certain
> that these were very clever people. I think it would be wiser to adopt Aldor
> (which won't break much) rather than to try to extend Axioms own language and
> let the two languages diverge. I simply don't see the point.
> 
> A different issue is whether we can live with the fact, that Aldor does not
> seem to be entirely free. I don't know how to get it's source. Therefore I'd
> argue to make changes to Axioms compiler in a way that makes it *more*
> compatible with Aldor. In fact, for the time being, I wouldn't make any
> changes, however, I could imagine to post a challenge to comp.lang.lisp to
> extend Axioms compiler to become Aldor -- in common lisp. There are very 
> clever
> people out there, maybe we can get them interested.

Personally, the issue of aldors licence is a show stopper. Trying to
make axioms spad compiler compatible with a closed system will be
futile. Maintaining compatibility with a moving target is always hard,
let alone one you cant see.

I do think a new compiler/language is something the Axiom project
should aim for, but as a long term goal. I believe we should be trying
to lift all of the things which both spad and aldor can teach us, and
think about how we can incorporate more modern ideas in programming
language design. Integration with theorem provers will likely demand
compiler support. `indeterminate objects' have been discussed before,
and we can probably learn a lot about how to implement such structures
by studying the work which has been done in `lazy evaluation'. The
very design of axioms algebra seems to demand a language which
supports recursive structures. None of these things exist in spad or
aldor.

A new compiler will likely take years to write. We should not forget
the spad compiler. We should learn as much as we can from it -- and in
the process help maintain, improve, and document it. 


Sincerely,
Steve