axiom-mail
[Top][All Lists]
Advanced

[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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]