Re: [Axiom-developer] Unions in Spad

[Stephen Wilson]

William Sit <address@hidden> writes:

> 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 agree that the challenge is great.  Perhaps if we can get an
IndexedUnion implemented we can work together to get some good
documentation together?  You are far more capable of writing for the
mathematically inclined reader, and I would hope to be able to
contribute some pieces perhaps more natural from a programmers
perspective.  Undoubtedly others can contribute to the process.

Many hands make light work, after all! :)

> > I read your post over a few times ...
> 
> Sorry, I'll try to write clearer next time around. (Clearly, it is difficult 
> to
> write ...).

Oh no, your writing was quite clear.  I am a slow learner, and it can
take me quite some time to digest things.

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

Absolutely, and I understand your careful methods.  On the other hand,
I would like one day for the Spad compiler to be feed utter garbage
and still cope with the input gracefully.

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

The Lisp output you are seeing is actually the underlying
representation which, if I understand correctly, is equivalent to the
representation based on Record.

The representation is a dotted pair, a cons cell, where the first
element is an integer index denoting the valid branch, and the second
yielding the raw data representing the value therein.

So you can see from your example that i1 and i2 give, respectively, 
(0 . 1) and (0 . 2), thus inj1 and inj2 are placing their values in
the tag1 field.

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

Yes, the issues involved here have come up in various other `thought
experiments' of my own in an attempt to figure how Spad could be made
more reflexive/introspective.  One problem is that the raw
representation of the values do not carry type information.  So
instead of (0 . 1) as representation for a Union element we really
need something like (0 (|Integer|) 1).  But this is a simplification.
Ideally (I think), domain elements should carry a header which gives
this information.  However, it may not be necessary to always carry
this extra baggage.  Homogeneous lists/vectors, polynomials, for
example, could store the information once rather than repeat it in all
its terms.

There may even be ways to classify a domain as `rich' enough to
warrant if such a representation of its elements is necessary at all.
 
> > > 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).

Its not so much the representation that I was driving at (sorry for
the ambiguity!).  If one thought of `index' as a function which
returns the last element added to a table, `I' your set of keys, and
`g' a hash function, then you basically get an interface compatible with
the semantics of IndexedUnion.  So I can think of IndexedUnion as a
`dictionary of types', plus the ability to associate a single value
with a given {key, type} pair.  However, this analogy may not turn out
to be terribly useful in practice -- I just couldnt help seeing the
connection.

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

Absolutely I do.  In fact, I have reread that exchange several times
over the past few years, as I have been thinking about the issues
involved regularly since that time (as I said, I am a slow learner :).

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

It would be possible today to do this by calling out to Lisp and
carefully choosing a representation there.  I believe that would be
entirely equivalent to getting a `hacked' record available which suits
your purpose.  Just view Lisp as a supply if infinitely many
`primitive types' to get past the aversion of punting Spads type
system.  This would have practical benefits as we could then
understand better what it would take to implement a more graceful
solution.  I and Im sure others would be more than willing to help
choose a Lisp representation and implement any necessary machinery, as
I understand you are not fluent in the language (many apologies in
advance if that is not accurate!).

Sincerley,
Steve