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

[Gabriel Dos Reis]

Waldek Hebisch <address@hidden> writes:

| 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 agree.  I don't believe that the goal of improved SPAD shall be a
clone of Aldor.  

[...]

| OTOH design of dependent types in Aldor can be criticised.  One thing
| is "Type : Type" (personaly I find this reasonable design choice).

This choice must be explored and studied carefully.  Improved SPAD
must ideally have a formal semantics (but, in reallity I suspect we
will only approximate it) and the implications of Type:Type must be
understood, especially since people has expressed many times
connection with proof theory.  I don't consider use of "pretend" a
good solution.

| 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'm fine with undecidable type checking in general , as long as we
have identified a large subset where it is decidable.

We must also look at how to convince the compiler to do delta
conversion without getting in a blackhole.

-- Gaby