Re: [Axiom-mail] Spad and inductive types

[Bill Page]

Quoting Ralf Hemmecke:

> ... 
> I know the definitions in aaa.as look quite lengthy, but it probably
> shows how one could generically generate appropriate Aldor code
> from a more concise Syntax. 

Since Aldor is already intended to be pretty concise, I don't think
it is a good idea in general to try to invent a new language and then
generate Aldor from it

 All the exports that appear are basically the
> exports of the Union (OK, Union still has a few more.)
>
> ---BEGIN aaa.as
> #include "aldor"
> #include "aldorio"
>
> define ET: Category == with; -- ExpressionType
> Expr: ET with {
>         MkInt: Integer -> %;

It doesn't look right to me that the MkInt constructor takes
a specific integer as a parameter while MkAdd and MkMul
take a type. 

>         MkAdd: (%, %) -> %;
>         MkMul: (%, %) -> %;
>         apply: (%, 'MkInt') -> Integer;
>         apply: (%, 'MkAdd') -> (%, %);
>         apply: (%, 'MkMul') -> (%, %);
>         case: (%, 'MkInt') -> Boolean;
>         case: (%, 'MkAdd') -> Boolean;
>         case: (%, 'MkMul') -> Boolean;

I think having 'apply' and 'case' appear as exports of Expr is
very undesirable. 

> } == add {
>         Rep == Union(
>             Mkint: Integer,
>             Mkadd: Record(left: %, right: %),
>             Mkmul: Record(left: %, right: %)
>         );

Why not write a Union of the constructors, instead of their
representation? I.e. something like:

        Rep == Union(
            Mkint: MkInt,
            Mkadd: MkAdd(%,%),
            Mkmul: MkMul(%,%)
        );


>         import from Rep;
>         MkInt(i: Integer): % == per union i;
>         MkAdd(x: %, y: %): % == per [Mkadd == [x, y]];
>         MkMul(x: %, y: %): % == per [Mkmul == [x, y]];
>
>         apply(x: %, t:'MkInt'): Integer == rep(x).Mkint;
>         apply(x: %, t:'MkAdd'): (%, %) == explode rep(x).Mkadd;
>         apply(x: %, t:'MkMul'): (%, %) == explode rep(x).Mkmul;
>
>         (x: %) case (t:'MkInt'): Boolean == rep(x) case Mkint;
>         (x: %) case (t:'MkAdd'): Boolean == rep(x) case Mkadd;
>         (x: %) case (t:'MkMul'): Boolean == rep(x) case Mkmul;

Why does this construction look so different from the
definition of Expr2 in

http://wiki.axiom-developer.org/SandBoxInductiveType ?

> }
> ---END aaa.as
> --------------------------------------------------------------------
> ---BEGIN bbb.as
> #include "aldor"
> #include "aldorio"
>
> #library EXPR "aaa.ao"
> import from EXPR;
>
> extend Expr: OutputType == add {
>         import from 'MkInt', 'MkAdd', 'MkMul';
>         import from Integer;
>         (tw: TextWriter) << (x: %): TextWriter == {
>                 x case MkInt => tw << x.MkInt;
>                 x case MkAdd => {
>                         (a, b) := x.MkAdd;
>                         tw << "(" << a << "+" << b << ")";
>                 }
>                 x case MkMul => {
>                         (a, b) := x.MkMul;
>                         tw << "(" << a << "*" << b << ")";
>                 }
>                 tw;
>         }
> }

The use of case above seems very unnatural to me. Is it
possible to extend each constructor (e.g. MkInt, MkMul, etc.)
separately. 

> 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 bbb.as

Ralf, these are just general comments about your approach and
aren't intended to be particularly critical. I think it is important to
try to understand how to write this efficiently in Aldor and your
work contributes greatly to this. 

Regards,
Bill Page.