Re: [Axiom-mail] Spad and inductive types

[Ralf Hemmecke]

On 05/08/2007 05:21 PM, Gabriel Dos Reis wrote:
> One of the issues I have with many of the various alternatives is
> that they make definition of new functions operating on Expr
> also impossible (by a third person) without intimate knowledge
> of the representation of Expr, or modifying the Expr domain.

> In contrast, in Haskell or Boot codes, once I give that data type
> definition, people are free to add more operations without knowing
> more of the internal representations.

Hi Gaby,

I am not at all good at Haskell, but what I have found now looks a bit 
closer to the Haskell definition. Of course, the function names (MkInt, 
MkAdd, MkMul) have nothing to do with the tags (Mkint, Mkadd, Mkmul) of 
the union, but the can be called with identical name, i.e. add the macros

Mkint ==> MkInt;
Mkadd ==> MkAdd;
Mkmul ==> MkMul;

to the code.

Of course one can add "case" function and "apply" functions similar to 
those exported by Union. Unfortunately the exports of Union does not 
carry over to Expr, because the type of Expr is given by ET.

Unfortunately, I don't see a way in Aldor to carry over the exports of 
the Union on the right hand side to Expr.

Note in particular that the there is something like Union(a:X, b:X).

Ralf

-> aldor -fx -laldor -mno-abbrev -mno-mactext aaa.as
-> aaa
e1 = 1
e2 = 2
e3 = 3
a1 = (1+2)
m1 = ((1+2)*3)



---BEGIN aaa.as
#include "aldor"
#include "aldorio"

--Haskell:
--data Expr = MkInt Int
--          | MkAdd Expr Expr
--          | MkMul Expr Expr

--eval::Expr -> Int
--eval (MkInt i) = i
--eval (MkAdd x y) = (eval x) + (eval y)
--eval (MkMul x y) = (eval x) * (eval y)

define ET: Category == OutputType; -- ExpressionType

Expr: ET with {
        MkInt: Integer -> %;
        MkAdd: (%, %) -> %;
        MkMul: (%, %) -> %;
} == add {
        Rep == Union(
            Mkint: Integer,
            Mkadd: Record(left: Expr, right: Expr),
            Mkmul: Record(left: Expr, right: Expr)
        );
        import from Rep;
        MkInt(i: Integer): % == per union i;
        MkAdd(x: %, y: %): % == per [Mkadd == [x, y]];
        MkMul(x: %, y: %): % == per [Mkmul == [x, y]];
-- The following two lines work but I haven't found them documented.
-- For the above version see AUG.pdf p. 145.
--      MkAdd(x: %, y: %): % == per union([x, y], Mkadd);
--      MkMul(x: %, y: %): % == per union([x, y], Mkmul);
        (tw: TextWriter) << (x: %): TextWriter == {
                select rep x in {
                        Mkint => tw << rep(x).Mkint;
                        Mkadd => {
                                (a, b) := explode rep(x).Mkadd;
                                tw << "(" << a << "+" << b << ")";
                        }
                        Mkmul => {
                                (a, b) := explode rep(x).Mkmul;
                                tw << "(" << a << "*" << b << ")";
                        }
                        never;
                }
        }
}

main(): () == {
        import from Integer;
        e1: Expr := MkInt 1;       stdout << "e1 = " << e1 << newline;
        e2: Expr := MkInt 2;       stdout << "e2 = " << e2 << newline;
        e3: Expr := MkInt 3;       stdout << "e3 = " << e3 << newline;
        a1: Expr := MkAdd(e1, e2); stdout << "a1 = " << a1 << newline;
        m1: Expr := MkMul(a1, e3); stdout << "m1 = " << m1 << newline;
}
main();
---END aaa.as