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