Re: [Axiom-mail] Spad and inductive types

[Gabriel Dos Reis]

On Mon, 7 May 2007, Ralf Hemmecke wrote:

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

Ralf --

  You captured so accurately many of the aspects of this issue that
I have almost nothing to add to your analysis.


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

Yes.


[...]

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

OK; many thanks.  I was wondering whether there was a better, but apparently
that is all I can get.

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

Well, it is something I would like to have in Spad.  I was just wondering how
I can approximate it in today Spad.  I came to this from different angles.
The most recent is my typed ast representation of Spad programs, as a domain.

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

Yes, I agree with your analysis.

| Otherwise, I fear the
| definition wouldn't look so nice like in the Haskell example.

-- Gaby