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