Re: Spad and inductive types

Ralf Hemmecke <[email protected]>
Newsgroups gmane.comp.mathematics.axiom.user
Message-ID <[email protected]>
> I think my example 'Expr2' at
> 
> http://wiki.axiom-developer.org/SandBoxInductiveType
> 
> satisfies your requirement, although on initial look it probably
> seems more complicated than what you might like. Some of this
> complication is merely interface for the Axiom interpreter. The
> essential definition of the inductive type is merely given by:
> 
>     Rep := Union(MkInt(Integer), MkAdd(%,%), MkMul(%,%))

> The definitions of MkAdd and MkMul as named types (domains) is
> sufficient to avoid the problem that this form of 'Union' is not
> disjunctive.

Bill, I like your way of approaching this inductive type thing. I only 
fear, in Aldor you have to add a few code snippets.
Your

       x case MkInt(Integer) => eval(x)$MkInt(Integer)

probably does not work in Aldor. (I haven't actually tested what the 
compiler does.) Probably in Aldor you would have to write

     Rep == Union(z: MkInt(Integer), a: MkAdd(%,%), m: MkMul(%,%))

and say

    x case z => ...

To me it looks like your approach is very much in line with what we do 
in Aldor-Combinat. The only difference is that basically you have

Expr2: ExprCat == Union(
     z: MkInt(Integer),
     a: MkAdd(Expr2, Expr2),
     m: MkMul(Expr2, Expr2)
) add {
     eval(x: %): Integer == ...
}

If I rewrite that code in along the lines of what we have in 
Aldor-Combinat, it would look like

Expr2: ExprCat == Plus(
                        MkInt Integer,
                        Plus(MkAdd(Expr2, Expr2), MkMul(Expr2, Expr2))
                   ) add;

and there would not be need to write anything behind "add", because the 
"Plus" construction knows about ExprCat. So in some way our "Plus" 
(which corresponds to a special form of "Union") is quite restricted.

And in general one cannot even generalize it to "Plus(ExprCat)(A,B)" to 
take the category into account since there is no generic way to 
implement all the functions. In fact that would require to ask for in 
implement functions at runtime. Note the type of Plus(ExprCat) would be

   (ExprCat, ExprCat) -> ExprCat

I don't see a way to implement that generically in Aldor.

So your way is the best one can get. What I like is, that it seems to 
show the desparate need for the "extend" operation.

Ralf
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.