Re: [Axiom-developer] Unions in Spad

[William Sit]

Stephen Wilson wrote:

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

Okay. Let's make that a near-term goal. How about starting a sandbox page for 
this
"pamphlet" (I'll even to agree to try this format by inserting the 
documentation if you
start the skeleton). Then anyone can add to it as they see fit. If you agree 
(at least
for now) with what I propose as a possible implementation model, I can adapt 
that email
into the pamplet.

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

I think that would be great (but a very difficult goal to achieve)! Perhaps one 
can set
different optimization levels using )set commands on the fly, especially with 
compiling
Axiom source. I guess that is already available, but I just don't know how.

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

This simple representation limits the generality and naturalness of 
implementation. But
where are the tags? Are they in some symbol table where (0.1) and (1.2) would 
be their
values? I think the tags (at least according to the examples I gave) should be 
used as
the index or part of the index set, and the index set should not be limited to 
the
natural integers (of course, if the index set is ordered, one can put it into a
bijection with 0.. n or 0.. , but that requires something else to store the 
bijection;
if the index set is not ordered, then some hashing function would be needed). In
mathematics, we let the index set to be quite arbitrary, and often a set of 
other
mathematical objects. So for example, the disjoint union of all prime fields 
would
require an index set that is the set of primes.

Subject to a hashing of the index set into an initial segment or the entire set 
of the
natural numbers, I think the data representation using a pair (a . b) is fine 
and
efficient. But this cannot be the same as Record, because in a Record, you need 
to
store all the data fields for each record. In Union, you only need only to 
store one.
The design flaw in Union is the exported functions currently do not allow branch
specification, even though the lisp representation is "indexed" (but without 
type info,
according to you, below). So there is no way to even coerce (the provided 
function in
Union) an element correctly if the domains AND the tags are not distinct. And 
there is
no way to discover the index of an element in the union in that case.

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

Surely, there should be ways to avoid redundant or unnecessary baggage. But 
somewhere,
the type information is kept, perhaps by the interpreter, with each identifier. 
For
compiled code, there should be less baggage. According to your explanation, I 
think the
pair representation is sufficient to implement IndexedUnion as a primitive. 
Note that
at the algebra level, it is not feasible to use Union as Rep because of the 
design
flaw.

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

"Not fluent" is giving me more credit than I deserve! I am certainly all thumbs 
when it
comes to lisp and I marvel at you, Tim, Gaby, Waldek and Camm making exchanges 
(mostly
"gibberish" to me) but understanding one another so easily. (I think if I were 
to spend
time learning this, I certainly would need literate programming on the level 
Tim is
advocating! But my objection is that I should NOT be involved in this "mess" 
because I
am not qualified.)

In the proposed IndexedUnion, what is missing is the Rep:= Record[index:I, 
value:
g(i)]. The key is to implement "coerce" since that creates elements of the 
domain
IndexedUnion, and most likely requires the use of a hash function, especially 
when the
index set is infinite.  It should be possible to implement in lisp all the four
functions ("=", index, value, coerce) and others like outputForm. This way, we 
do not
have to worry about the "signatures" of "value" having dependent types. It 
would be
more involved to do so at the algebra level and the implementation would not be
natural.  As an experiment, rather than modifying Record, perhaps we can create
IndexedUnion as a primitive type directly (from scratch).

Whatever the primitive types are, the important thing is that there be a 
well-designed
user interface (exported functions) on par with all other algebra code. Right 
now,
Tuple and Union are "inaccessible" from the algebra layer without going to lisp 
(Record
seems okay ). That is, in my view, a design flaw. They should be designed as if 
they
were genuine domains (where one can construct elements and extract information 
from
elements and compute with them). How they are implemented and optimized at the 
lower
levels should not be of concern to the algebra layer.

William