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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer