Re: [Axiom-mail] Spad and inductive types

[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

You may be right. But if there is a consistent way to add some better 
functional style to Aldor, why should that be bad?

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

Huh? The MkAdd also take specific elements of Expr. That is not 
different from an element of Integer. It's at the same level.

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

Well. What do you do with a data structure that has no accessor functions?

> > } == 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(%,%)
>      );

Could probably be done, but how is MkInt different from Integer?
What do you gain by introducing the domains MkAdd and MkMul?
If that is needed, it can be done as you showed at 
http://wiki.axiom-developer.org/SandBoxInductiveType .
But I thought that the Haskell

data Expr = MkInt Int
          | MkAdd Expr Expr
          | MkMul Expr Expr

is more like

Union(Cross(Tag, Int),
      Cross(Tag, Expr, Expr),
      Cross(Tag, Exrp, Expr)).

In Aldor the tags appear in front of : so the Cross would have one 
argument less (and I have replaced Cross by Record (which is probably 
not necessary).

> >     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 ?
>
> > }

I don't actually understand whether this is meant in a positive or 
negative sense. I would rather call my code a variation of yours.

The biggest difference probably is that you cannot produce that what was 
in file bbb.as, because in an "extend Expr" you would have no way to 
access the internal structure of Expr.

As I understood Gaby, he wanted to define just the data structure 
without any additional features like eval or coercion to OutputForm.

To such a data structure one could add features (= functions) later 
without changing or knowing the actual representation. That is a step to 
avoid a lot of (if not all) mutual recursion in the construction of the 
Axiom library.

Ralf