Re: [Axiom-developer] B natural

[Gabriel Dos Reis]

On Mon, 5 Jun 2006, Martin Rubey wrote:

| Gabriel Dos Reis <address@hidden> writes:
|
| > On Mon, 5 Jun 2006, Martin Rubey wrote:
| >
| > | Gabriel Dos Reis <address@hidden> writes:
| > |
| > | > Also, I have been looking for the a formal grammar description of SPAD.
| > | > Where can I find it?  The AXIOM book seems silent about it....
| > |
| > | Forget about SPAD, go for Aldor.
|
| > The source code of the Aldor compiler is not available; SPAD's is.  I heard
| > there are talks tomove on that front, but how long we have to wait.  I 
cannot
| > tell my students to wait till next year or so.
|
| > Yes, of course I can initiate a mini project where where they will build an
| > Aldor-like translator, but I rather have them start with a base code and add
| > transformations or type system convenient features.
|
| A very useful project -- of course, I don't know whether it fits your needs --
| would be the following:

I think it is a good idea, given the current constraints.

| The Aldor interpreter is very weak, it segfaults quite often, it has no way to
| figure out "likely" types and so on.
|
| So maybe, you and your students could figure out how to make the axiom
| interpreter do the type guessing etc., but then call the aldor compiler,
| instead of using SPAD. (If this description is too vague, please complain!)

Yes, type inference is of the area that I was thinking of.  Aldor's
requirement of System F-style explicit polymorphism is way too heavy.
We should have syntaxes so that in the simple cases, the system infers
the type -- full type inference in unreasonable and foolish to seek for.

| The benefit would be that we would have Aldors power available at the
| interpreter level.

Agree.

| I guess you know already that SPAD has various shortcomings, the two
| major ones probably being:
|
| * Types are not first class objects (i.e., no Lists of Types),
|
| * SPAD doesn't have truly dependent types.

Yes, I agree.  However imperfect it is, it has the virtue that its
source code is available so that people can improve it.

-- Gaby