Waldek Hebisch <[EMAIL PROTECTED]> writes: | Martin Rubey wrote: | > C Y <[EMAIL PROTECTED]> 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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer