Re: [Axiom-mail] Spad and inductive types

[Ralf Hemmecke]

> An inductive type is a kind of union whose members are
> inductively defined (like the kind of combinatorial thing you're
> doing with Ralf).  Here I took a very simplistic datatype, that of
> an arithemtic expression over integers:

>     An arithmetic expression over integer is:
>       * an integer, or 
>       * addition of two expressions over integer, or
>       * multiplication of two expressions over integer.

I somehow fear that none of the code on

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

makes you happy. Or does it?

The equation

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

actually is just a way to form the data structure without any 
functionality. Just the inclusion functions

Expr: with {
  MkInt: Integer -> %;
  MkAdd: % -> % -> %;
  MkMul: % -> % -> %;
} == add {
  Rep == ...
}

It is not so obvious that the Rep should become a Union, or is it? That 
depends a bit on the fact whether one wants to see this in a lazy or 
non-lazy fashion. You probably want the lazy way. But Aldor is not lazy, 
so one must simulate it.

Going the Aldor-Combinat way, there would be need to define general 
constructors. Our Plus

http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu23.html#x37-550008.10

is something like the top-level constructor on the right hand side. (It 
does, however, only take 2 arguments not 3 that are separated by |.)

In Aldor it is not possible to replace something like that "Plus", by 
the built-in Union constructor, since Union does not export very much.
In Aldor the nearest thing you get would look like

Expr: with {...} == Union(z: Integer, a: %, m: %) add {...}

i.e. with the need of "add". However, of course z, a, m, are just tags 
and not constructors of Expr. It's a bit hard to translate the Haskell 
code literally into Aldor.

Note that in Aldor-Combinat, the "Plus" constructor is *not* inherent to 
the language. Furthermore, it is not flexible in general. For us it is 
enough that it returns something of type CombinatorialSpecies(L). But 
that is not a general-purpose-type.

Are you intending to add such kind of inductive type definition to SPAD?
What actually bothers me most is the resulting type. I can imagine that 
something like

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

could be added to Expr, but then an "extend Expr" is vital, since not 
everything can be put into the above equation. In fact, the definition 
of "eval" would already live in an extension. No? Otherwise, I fear the 
definition wouldn't look so nice like in the Haskell example.

Ralf