Re: [Axiom-developer] Unions in Spad

[Stephen Wilson]

Dear William,

You never cease to amaze me with your keen insights!

I read your post over a few times, and I believe I have a grasp on the
issues.  I am sightly pressed for time, so Id like to just comment on a
few points for now.


William Sit <address@hidden> writes:
[...]
> The above specification would enforce automatically the constraints
> Stephen thinks Spad is currently lacking (but documented, see
> hyperdoc on Union):

Just for clarity, it is not that I dont think Spad lacks a
specification in this regard.  Its the implementation I have concern
with.  For example, in Spad code Union(Integer,Integer) can be used as
a valid type (though the interpreter will recognize it as malformed if
the type is used in a declaration).  The tagged case has problems
too. Consider:

==--- union-test.spad ----

)abbrev domain BAR Bar

Bar() : Exp == Impl where
   Exp == with
     inj : Integer -> %
     inj : String -> %
     prj : % -> Integer
   Impl == add
     Rep := Union(tag1: Integer, tag1: String)
     inj (n : Integer) : % == [n]
     inj (s : String) : % == [s]
     prj p == (p::Rep).tag1

==----------------

                        AXIOM Computer Algebra System 
                          Version: Axiom (May 2007)
               Timestamp: Wednesday July 11, 2007 at 14:11:07 
-----------------------------------------------------------------------------
   Issue )copyright to view copyright notices.
   Issue )summary for a summary of useful system commands.
   Issue )quit to leave AXIOM and return to shell.
-----------------------------------------------------------------------------

(1) -> )co union-test.spad
[...]
   Bar is now explicitly exposed in frame initial 
   Bar will be automatically loaded when needed from 
      /home/steve/development/axiom/spad-playpen/BAR.nrlib/code
(1) -> bi := inj 1
   Loading /home/steve/development/axiom/spad-playpen/BAR.nrlib/code 
      for domain Bar 

 LISP output:
(0 . 1)
                                                                    Type: Bar
(2) -> bs := inj ""

 LISP output:
(1 . )
                                                                    Type: Bar
(3) -> prj bi

   (3)  1
                                                        Type: PositiveInteger
(4) -> prj bs
 
   >> Error detected within library code:
   (1 . ) cannot be coerced to mode (Integer)

> Based on the notion of constructing IndexedUnion using an
> index set, I propose the following exports (there should be
> more if one compares this with IndexedAggregate or other
> Indexed* constructors, but for the purpose of this
> discussion, they are irrelevant):
> 
> IndexedUnion(I: SetCategory, g:I ->SetCategory):SetCategory
> == with
>       "=": (%, %) -> Boolean
>       index: % -> I
>          ++ index(x) returns the index i such that x belongs
> to g(i)
>       value(x:%): g(index(x))
>          ++ index(x) returns x as an element in g(index(x))
>       coerce(i:I, x:g(i)): %
>          ++ coerce(i,x) creates x as an element of % in the
> component g(i)

In fact, I believe that IndexedAggregate is very important here.  The
concept of IndexedUnion and the familiar notion of Dictionary are
exceedingly similar.  If were it not for the context, reading the
signature above would immediately make me think `hash table'.

> What about the data representation of Union? Can we do this
> at the algebra level? We seem to need non-homogeneous data
> representation! In lower level, this is not difficult, say
> using pointers (perhaps another reason why Union is
> implemented as primitive, to hide pointers at the algebra
> level), but at the algebra level, Axiom is not designed for
> heterogeneous objects (that's why people use C++):

Absolutely, the critical issue here is non-homogeneous data.  For Spad
to evolve into a truly flexible language capable of supporting the
constructs you have so very kindly detailed,  I believe that it would
be worth while to consider the `static typing where possible, dynamic
typing where necessary' approach to language design.


Again, many thanks for your detailed article!

Take care,
Steve