Re: [Axiom-developer] Unions in Spad

[Bill Page]

> > "Bill Page" <address@hidden> writes:
> > ...
> > >
> > > I think mixed union constructions should be consider syntax errors.
> >
> Stephen Wilson wrote:
> > I personally agree as well.  Unfortunately, the current Spad parser
> > is, well, difficult to change.  I can check the uniformity of Union
> > branches at a post-parsing stage to at least get the assertion into
> > the system.  Perhaps in time my new parser could be used as a full
> > replacement for the current one.
'> >
>
On 7/9/07, Waldek Hebisch wrote:
> A little nitpick: if mixed union constructions are considered errors
> for me it is clearly a semantic error.  I think it is better to catch
> such errors on a post-parsing stage.  Why this may matter: syntax
> errors frequently leave parser in a confused state, making hard to
> detect other errors.   Also for users is seem easier to have simple
> syntax + set of semantic constraints than to encode constraints
> in syntax.

On reflection, I am inclined to agree that it should not be a syntax
error but perhaps for different reasons. Aldor defines a uniform
concept not in Spad called a "keyword argument". Among other things
keyword arguments can be used when calling a function. E.g. the
definition:

  f:(x:Integer)->Integer

allows f to be called like this:

 f(x==10)

Syntactically a construct like "x:Integer" can be used anywhere the
name "Integer" can be used. It associates a "keyword" or tag with a
type but otherwise remains the specification of a type.

So really in Aldor when writes

 Union(x:Integer, y:String)

one is using the same conventions. So as Waldek implied, the fact that
Aldor currently does not allow

 Union(Integer, String)

is not really a syntactic issue but rather a semantic one.

Thinking out load: Perhaps this use of ':' should be given explict
operator semantics so that it could be considered as just a pretty
form of type constructor, e.g.

 Keyword(x:Symbol,T:Type): ... with KeywordCategory ...
   == T add ...

(not withstanding that it's usage here is recursive). Then as a type
it would be easy to insist that a parameter to a constructor be of
this type by requiring KeywordCategory.

Does this make sense?

Regards,
Bill Page.