Re: [Axiom-developer] Re: SPAD and Aldor again

[Peter Broadbery]

On Fri, 2006-11-17 at 08:43 +0100, Martin Rubey wrote:
> C Y <address@hidden> writes:
> 
> > I think we should make the decision as a project not to wait any longer for
> > Aldor, and commit to improving SPAD - up until now I think there has been
> > hesitation to commit serious effort to SPAD due to the possibility of Aldor
> > becoming available and making such work unnecessary.  To my mind the first
> > step to improving SPAD is to decide what SPAD should be, since right now it
> > doesn't have a formal language definition.
> 
> For me this is totally clear: SPAD should become a free implementation of the
> Aldor language. It would not make sense to have to different languages around.
> 
> And, as you know, in my opinion the first step in making this happen is to 
> make
> the Axiom interpreter (!) understand Aldor generated code, i.e., dependent
> types.
> 

This is currently stymied by the aldor compiler not being able to generate .asy 
files 
where there are dependent types in signatures (try 'foo: (R: Ring, t: R)').  
The .asy 
generation code enters a loop, which is a bit poor.  

Even once you've got your dependent signatures into axiom, it has to 
(presumably) be 
able to interpret them, which will need a more complex type matching process 
than 
what currently exists (I think).  On the plus side, doing this is a good step 
towards a 
real compiler. 


> Peter Broadbery is currently making Aldor extend work in Axiom. That's a giant
> step, in fact! Unfortuantely, it seems that support for dependent types is 
> even
> more difficult. One would have to understand how aldor and axiom work
> together. As far as I know, there are only very few people around who know
> about this already. 

The mechanism is fairly simple - just fake up objects that look like
aldor domains and categories in axiom (interop.boot does this), and on
the other side interpret asy files as defining axiom types (daase.lisp).
Unfortunately this doesn't add any aldor semantics into axiom, or the
other way round.

Peter


> 
> 
> _______________________________________________
> Axiom-developer mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/axiom-developer