Re: [Axiom-developer] Unions in Spad

[William Sit]

Stephen Wilson wrote:

> You never cease to amaze me with your keen insights!

Thanks. Unfortunately, in Axiom, I have found that the simpler things look, the
more difficult it is to analyse. (This is one reason I find literate programming
impossible to achieve. If we are still having problems understanding the 
simplest
domain constructions, how can we ever document the cutting edge algebra 
domains?)

> I read your post over a few times ...

Sorry, I'll try to write clearer next time around. (Clearly, it is difficult to
write ...).

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

Yes, I understand that. In my lines above, "lacking" refers to lacking "enforce
... constraints" (not "documented"). Poor sentence construct, sorry.

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

Yes, the compiler did not enforce what was specified in the hyperdoc
specification ("In this tagged Union, tags a, ..., b must be distinct.") But
there are lots of other things the compiler would not enforce for various 
reasons
(such as "Commutative" and other attributes). In this case, probably no Axiom
programmer would use the same tag for two distinct fields (I won't even use the
same identifier outside of Union Rep even though I should be able to).  In
mathematics articles, I would be equally careful not to use the same symbol for
different quantities, even if it were just a dummy index. (I modified the
notations in my previous email several times for this reason.)

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

 The problem is the interpreter looks up the signature of prj and finds (only)
one whose target is Integer. This is all as it should be. However, this run time
error may not show up if both fields are Integer.

Try this:  testu2.spad
-------
)abbrev domain BAR Bar

Bar() : Exp == Impl where
   Exp == with
     inj1 : Integer -> %
     inj2 : Integer -> %
     prj : % -> Integer
   Impl == add
     Rep := Union(tag1: Integer, tag2: Integer)
     inj1 (n : Integer) : % == [n]
     inj2 (s : Integer) : % == [2*s]
     prj p == (p::Rep).tag1
-------
After compiling,

(4) -> i1:= inj1 1

 LISP output:
(0 . 1)
                                                                    Type: Bar
(5) -> i2:= inj2 1

 LISP output:
(0 . 2)
                                                                    Type: Bar
(6) -> prj i1

   (6)  1
                                                        Type: PositiveInteger
(7) -> prj i2

   (7)  2
                                                        Type: PositiveInteger

Note the answer is even *correct*! Axiom should have signaled a failure or 
error.
This is most likely due to internal *implementation* of Rep and i2::Rep should
not be allowed to apply to tag1. But EVEN IF it is using tag1, how on earth did
it get the value 2? The problem is that in inj2, there is no indication that the
value should be placed into the tag2 field! (but neither is there an indication
to place it into tag1 field. Axiom simply gives it to the first one! If correct
indexing is done and kept, this would not have happened or allowed. Instead of
the two inj1 and inj2, I would use coerce(0, 1) and coerce(1, 1), (assuming 
index
set is IntegerMod(2)),  and to retrieve the values , I would simply use value(p)
as in my proposal, and there would be no problem. Note that my proposed Rep is
also more efficient than the current Rep (which seems to reserve space for ALL
possible domain values and tags, but did not keep the indexing information) when
all you need is just space for ONE domain value and its index, per Record.

Unfortunately, for the current Union implementation, there seems to be no way to
tell even which domain the underlying value of p belongs, so that one cannot
distinguish the two cases to implement prj correctly (even if the tags and
domains are all distinct). The current "case" requires one to know beforehand 
the
value (without any indication of the index of the domain) to test against, as in
(p case 1) or (p case ""). It is designed to be more like a "switch" than to 
give
you information on the element. So I think it is a design flaw in Union. That is
why my proposed exports in IndexedUnion does not use "case" at all. Rather, it 
is
simpler to tell the index and value of a member in a disjoint union.  (By the
way, the idea of "disjoint union" is precisely to allow the same value to wear
two or more hats.)

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

That would be another discussion altogether. For now, I believe there is no need
for hashing in the implementation of IndexedUnion. If I understanding this
correctly, hashing involves placing items in a fixed prealloted space by
computing the address of storage from the content (or key) of the stored item.
Here we don't have such a situation, unless lists of IndexedUnion objects are
involved (which is where Aggregate comes in).

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

Do you recall we had a fairly long discussion on dependent types?

http://wiki.axiom-developer.org/18AxiomDomainsAndAldorReturnTypes

I believe I figured out a way to code it in current Axiom, but not that
naturally. The idea is to use package or domain constructors, because these
clearly allow dependent types. I need to review that to see if it can be applied
to IndexedUnion. I have a feeling it is not possible because Record cannot be
coerced at the algebra level to take heterogeneous objects. So if you can hack
Record into doing that, we can probably implement the exported functions 
somehow.
Certainly, if Record remains primitive, then all the exported functions I
proposed can be easily implemented. (Functions implemented in primitive domain
such as "case" do not show up in ")di op case" or ")show Union" (but they show 
up
in hyperdoc)).

William