Re: [Axiom-developer] Axisp news

[Stephen Wilson]

Martin Rubey <address@hidden> writes:

> Stephen Wilson <address@hidden> writes:
> 
> > > Rather, PLEASE try to follow the Aldor User Guide.  Since Christian 
> > > Aistleitner
> > > wrote a parser for Aldor some time ago (in Aldor, sources being available 
> > > from
> > > himself, I believe), maybe you would like to get into contact with him.
> > 
> > Grammatically, Spad is fairly similar to Aldor, as you know.  I am actively
> > thinking about Aldor features that I would like to integrate with the
> > compiler down the road.  However, I am not commiting to cloning Aldor, as I
> > feel there are shortcomings/difficulties.
> 
> I would really like to know what shortcomings you mean here.  

Most of them are detailed in `The Aldor Type System' by E. Poll and
S. Thompson.

Another shortcoming relates to `first class types'.  One can generate
a new type at run time, but there is no elegant mechanism in place to
recover the exact type.  Consider:

          mkMod(n : Integer) : IntegerMod( ? ) ==
                                   IntegerMod(compute(n))

If domains and categories are truly first class, we need a way to
compute with them as such.  There needs to be a simple logic
associated with the type language which could help recover such
bindings lost to an inner scope.  Im considering ways of introducing a
form of pattern matching over type expressions which could accommodate
this situation.  See below.

In addition, IIRC (its been a while since I played with aldor), there
are real problems with how constants are treated.  In short, they are
not really constants.  I remeber seeing code such as:

        add!(r: %, s: %, t: %) : % == 
                 if one? % or zero? % then s + t else ...

To work around the fact that the destructive add would modify the
constants `0' or `1', leading to predictable surprises.  The
imperative aspect of the language needs to be more carefully
considered, IMHO, especially w.r.t the semantics of a types
parametrized over (possibly mutable) values.

One could say that a constant can only be used in a type expression,
but thats rather draconian.  Moreover, it does not play nice with type
constructing functions like `mkMod' above.

> I know of only
> very few, and these are - in my opinion - really difficult questions:
> 
> * the problem of needing both AbelianMonoid as well as Monoid.

Its been mentioned before that OBJ has a facility for defining these
kinds of relationships.  A solution is likely to derive from there.

> * certain difficulties transforming Tuples

I assume your talking about the issues raised in the article I
mentioned above?

> > I would be happy to dicuss some of my plans for enriching the compiler with
> > features familiar to Aldor if interested.
> 
> For a start (which will keep you busy the next few months I guess), there are
> the following features SPAD needs badly.  Top priorities first:
> 
> * types and functions should become truly first class objects.  Currently, 
> SPAD
>   distinguishes between functions within a domain or package (eg., + or
>   integrate) and domain constructors (like Fraction or Complex).  This
>   distinction has to go away.  For example, I need to have the following
>   signature allowed:
> 
>   Plus(
>     F: (L: LabelType) -> CombinatorialSpecies L,
>     G: (L: LabelType) -> CombinatorialSpecies L
>   )(L: LabelType): CombinatorialSpecies(L) == add {...}
> 
>   I.e., F and G are functions that produce domains, and Plus(F, G) returns
>   another such function.
> 
>   It goes without saying that I need full support for dependent types.

Yes.  I agree that these things are desirable.  I will be working on
adding such facilities.  Id like to improve the syntax a bit, though.
For example, its common to write things like:

           D(R : Ring, P : Polynomial R) : ... == ...

Id like to introduce the ability to do a form of `pattern matching' on
the types, so that the above would read:

           D(P : Polynomial (R : Ring)) : ... == ...

For such things to work, one would need to enforce case sensitivity on
values, domains and categories to separate value expressions from type
expressions.  The system I have in mind would be roughly based on the
`:' operator.  Quick examples:

         x : D        -- Bind x to a value of domain D.  We know x is a
                         value of a domain as it is lowercase.

         D : C        -- Bind D to a domain of category C.  We know D
                         is a domain as it is uppercased.

         x : D : C    -- Bind x to a value of domain D, D to a domain of
                         category C.

You could have wildcards to ignore certain values, so `x : _ : C'
would bind x to the value of _some_ domain which has category C.

Such basics would allow one to give a type to the mkMod function
above:
       
          mkMod(n : Integer) : IntegerMod(_) ==
                                   IntegerMod(compute(n))

Here the return type contains an explicit wildcard variable.  If
IntegerMod were an overloaded function, one might write `IntegerMod(_
: Integer)' to remove ambiguity.

Such things could allow one to use a form of pattern matching over
types in order to recover a binding for the dynamic component. 

> * Currently exports may be conditional, but only in a very narrow sense: only
>   "has" and "is" statements are allowed in the condition.  This is too
>   restrictive, as the example of the "Complex" constructor shows, where we 
> want
>   to export "Field" only if -1 is not a square root in the ground ring.

I have not spent a terrible amount of time on this issue.  However
arbitrary expressions lead immediately to undecidability.  Again, we
need to find ways to lift runtime properties back into the static type
system in a graceful manner.  

> * It should be possible to define types recursively, as detailed in the Aldor
>   User Guide

Agreed.  My work on the compiler will be taking this into account.

> * Generators

This will not be much of an issue, as the semantics are quite clear
and not difficult to implement.  I really would like to see
generators.

In addition, we also need exceptions, as they provide an important
runtime mechanism to enforce invarients that the compiler could not
statically check.

> > I would certainly like to encourage anyone to contribute their thoughts on
> > what an `ideal' language should be.
> 
> I'm afraid that attempting to have an ideal language results in yet another
> useless language in the end.  Too many people tried to do that, and only very
> very few, very very gifted people succeeded.  Aldor is a pretty good language
> for doing mathematics.

Yep, its pretty good.  I may not be the sharpest knife in the drawer,
but I'll take a stab at improving it.  I know that `ideal' is a
pipe-dream.

> 
> Martin

Cheers,
Steve