axiom-developer
[Top][All Lists]
Advanced

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

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


From: Martin Rubey
Subject: RE: [Axiom-developer] Axiom domains and Aldor return types
Date: Fri, 14 Jan 2005 12:10:45 +0100

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.

 > Of course from a programming point of view we do know how to interpret the
 > Aldor construction and apparently Aldor knows how to compile it. But I do
 > not think that this necessarily makes it desirable in a language that is
 > primarily intended to be efficient and accurate in the definition of
 > mathematical concepts.

I don't think that this is an efficiency problem, neither a problem of
accuracy. 

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


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

Well, if it would be only encouragement... However, there is no way to do it
differently! I'm sure it is not too difficult to come up with an example where
the solution above won't work.

There is another, different point I'd like to make:

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.

Martin





reply via email to

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