[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-mail] Spad and inductive types
From: |
Ralf Hemmecke |
Subject: |
Re: [Axiom-mail] Spad and inductive types |
Date: |
Tue, 08 May 2007 08:56:46 +0200 |
User-agent: |
Thunderbird 2.0.0.0 (X11/20070326) |
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
- [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/06
- Re: [Axiom-mail] Spad and inductive types, Martin Rubey, 2007/05/07
- RE: [Axiom-mail] Spad and inductive types, Bill Page, 2007/05/07
- Re: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/07
- RE: [Axiom-mail] Spad and inductive types, Bill Page, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types,
Ralf Hemmecke <=
- RE: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Ralf Hemmecke, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Ralf Hemmecke, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/08
- Re: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/07
Re: [Axiom-mail] Spad and inductive types, Gabriel Dos Reis, 2007/05/07