Re: [Axiom-developer] Unions in Spad (Correction)

[William Sit]

I made some erratic comments (attached below) on design flaw in Union that was 
based on
hyperdoc documentation. Since hyperdoc does not allow insertion of parameters 
for Union
(for unknown reasons), I was "misled". Thanks to Stephen's reply to Ralf's 
comments, I now
learn that the )show command does allow that and the set of exported functions 
are slightly
different.

Here is the exports for :
(1) -> )show Union(tag1:Integer, tag2:Integer)
 Union(tag1: Integer,tag2: Integer) is a domain constructor.
------------------------------- Operations --------------------------------

 ?=? : (%,%) -> Boolean                ?case? : (%,tag1) -> Boolean
 ?case? : (%,tag2) -> Boolean          coerce : % -> OutputForm
 construct : Integer -> %              construct : Integer -> %
 ?.? : (%,tag1) -> Integer             ?.? : (%,tag2) -> Integer

(There were only "=", "case" and "coerce" in hyperdoc and their usages for 
"case"  in
Union(a:A, b:B):
   x case y (x: %, y: A) returns an element of Boolean
   x case y (x:%, y:B) returns an element of Boolean
were wrong).

It is not possible to construct elements in the above domain and specify which 
copy of
Integer in the Union one wants the input to below. There are two "construct" 
but they have
the same signature and so the Interpreter will simply select the first. So 
while there is
still some design flaw, it is possible to distinguish the cases.  However, 
there is still
some bug:

(1) -> dom:=Union(tag1:Integer, tag2:Integer)

   (1)  Union(tag1: Integer,tag2: Integer)
                                                                 Type: Domain
(2) -> j1:dom:=[1]

   (2)  1
                                 Type: Union(tag1: Integer,tag2: Integer,

(3) -> j1 case tag1

   (3)  true
                                                                Type: Boolean
(4) -> j1 case 1

   >> Error detected within library code:
   upcase: bad Union form

protected-symbol-warn called with (NIL)

Perhaps a better error message should be given, like:
(5) -> j1.tag2

   >> Error detected within library code:
   (0 . 1) cannot be coerced to mode (Integer)

protected-symbol-warn called with (NIL)

It is not clear what function is called to evaluate the next one, but the 
"coerce" works as
given in hyperdoc.


(6) -> coerce(j1)@Integer

 Function Selection for coerce
      Arguments: Union(tag1: INT,tag2: INT)
      Target type: INT
   -> no appropriate coerce found in Integer
   -> no appropriate coerce found in Integer

 [1]  signature:   INT -> INT
      implemented: slot $(Integer) from INT
 [2]  signature:   INT -> INT
      implemented: slot $(Integer) from INT
 [3]  signature:   INT -> INT
      implemented: slot $(Integer) from INT
 [4]  signature:   INT -> INT
      implemented: slot $(Integer) from INT
 [5]  signature:   INT -> INT
      implemented: slot $$ from INT
 [6]  signature:   INT -> INT
      implemented: slot $$ from INT


   (6)  1
                                                                Type: Integer


William
-------

William Sit wrote:

> 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.)
>
>> The construction is related to the bug in Union when the domains are not 
>> distinct (but
>> the
>> tags are): In Union(a:A, b:B) where A = B, the two coerce functions (one 
>> from A to %
>> and
>> one from B to %) coincides, with no way to distinguish the two.
>

Should be the two "construct" functions.