RE: [Axiom-mail] Spad and inductive types

[Bill Page]

On May 7, 2007 10:41 AM Gaby wrote:
> 
> Martin Rubey writes:
> 
> | Here you go.  But I doubt somehow that Gaby had this in 
> | mind, since this is quite usual stuff in Axiom
> (grep "Rep.*Union")
> 
> Thanks, Martin.
> 
> I did not say I did not know how to write it.  I said "I don't
> have a good way" :-).  Everything I've tried to come up
> (including proposed solutions here) with looked a hack to me.

I think it would have been very useful if you had included what
you came up with in your original email. :-( Anyway, I think
your question is very useful as it stands as an example of
the difference between Spad and Boot.

> Part of the reasons is
> 
>   --     MkAdd ==> Record(lAdd:%,rAdd:%)
>   --     MkMul ==> Record(lMul:%,rMul:%)
> 
> if union are used whose fields are directly records, then
> the fields of the record must themselves have different name.
> In the Boot or Haskell case, only the data constructor name
> need to be different.

That is not an essential feature of how this must be written
in Spad. For example see my recent additional example at:

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

But I think you are right to point out a limitation of the
design of the 'Union' domain constructor in Spad (and in
Aldor).

I think there is no good reason that 'Union' is implemented
in Spad using polymorphism of coerce to create elements. For
example the following provides no method to create objects
with a specific tag, x or y (by default only objects tagged
x are created).

(1) -> )sh Union(x:Integer,y:Integer)

 Union(x: Integer,y: Integer) is a domain constructor.
--------------------------- Operations --------------------

 ?=? : (%,%) -> Boolean           ?case? : (%,x) -> Boolean
 ?case? : (%,y) -> Boolean        coerce : % -> OutputForm
 construct : Integer -> %         construct : Integer -> %
 ?.? : (%,x) -> Integer           ?.? : (%,y) -> Integer

In spite of this it appears that the internal representation of
'Union' does implement a proper disjunction as required by the
expected semantics.

I would prefer that Union have methods something like this:

 construct : (Integer,x) -> %     construct : (Integer,y) -> %

but this would also require some changes in the Axiom interpreter
to work smoothly.

> I fully understand Spad is not Haskell, neither Boot, but I'm
> looking for a solution where only the toplevel data constructors
> needs to be different.

I think my example 'Expr2' at

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

satisfies your requirement, although on initial look it probably
seems more complicated than what you might like. Some of this
complication is merely interface for the Axiom interpreter. The
essential definition of the inductive type is merely given by:

    Rep := Union(MkInt(Integer), MkAdd(%,%), MkMul(%,%))

The definitions of MkAdd and MkMul as named types (domains) is
sufficient to avoid the problem that this form of 'Union' is not
disjunctive.

> I have more to say later.

We're listening. :-)

Regards,
Bill Page.