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

[Waldek Hebisch]

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

I am affraid we will have two different languages: there are legal reasons
and technical ones: I do not see why we should limit ourselfs to capabilites
present in Aldor and (assuming that we want this) implementing _all_
capabilities of Aldor is likely to take long time.  I do not want to
underestimate big things (dependent types) but getting little details
100% compatible would probably take more time.

I do not want to diverge just for beeing different, but agreeing that
we just one _some_ Aldor features in Axiom language is IMHO a better
way: we will not waste time trying to be 100% compatible.

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

I tend to think that adding dependent types to compiler is easier: compiler
has to do typechecking and probably some runtime support (the rest should
work the same).  Interpreter needs more runtime support and type 
inferencing.  Inferencing is harder. And of course there is added burden
of keeping thing Aldor compatible.

OTOH design of dependent types in Aldor can be criticised.  One thing
is "Type : Type" (personaly I find this reasonable design choice).
Another is using unevaluated parameters (not doing beta convertion)
for typechecking (more precisely for deciding type equivalence).  However,
"Type : Type" + equivalence after evaluating parameters would make compile 
time typechecking undecidable.  I think that we should use evaluated
parameters for deciding type equivalence, but postpone some checking to
runtime.

> 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. 
> 
> I guess it's Peter. Laurentiu says he doesn't know about the axiom side, but I
> know he knows foam. Tim, do you know about that stuff?  Gaby, Waldek, did you
> dig into this connection yet?
> 

I looked at extend first: after reading Aldor doc I think that compiler
part should be easy.  Namely, Aldor requires that you import an extension
before you use it.  So basically, all you need is to patch compiler
symbol tables after importing an extension (AFAIU Spad compiler alredy
have needed functionality, to support recompilation in a single image).

More tricky is allowing dynamic loading of extensions: start interpreter,
stash few instances of a type in datastructres, then extend it.  In fact,
this is not very hard if you use double indirection (element -> unique
proxy -> type), but AFAICS Spad uses only single indirection (element
-> type).  I am not sure how well extension works in Aldor interpreter.
My impression is that Aldor uses single indirection and lazyness,
which should work nicely for loading at startup but may have problem
if you load new extensions in the middle of the run.

-- 
                              Waldek Hebisch
address@hidden