Re: [Axiom-developer] Unions in Spad

[William Sit]

Stephen Wilson wrote:
> Main question is _why_ they [hybrid union] might be desirable. 
> Spad does not support them. Aldor might in theory, but only in 
> theory.
> [...]

> Do you have an argument for `hybrid' Unions?
Gabriel Dos Reis wrote:
> In general, I'm of the opinion that the language
> should be
> constrained only when we cannot come with proper semantics.
> I'm not sure this case is one such case; that is why I would
> like to understand the arguments. I don't want a language
> designed to express only what I can think of today.
I agree with Gaby.

The construction of Union (in Axiom) as implementing the notion of coproduct or external direct sum in Category Theory, specifically as disjoint union in Set Theory and taking place in the category of sets, should have nothing to do with tags, but with an index set and the sets associated with each index. (By the way, the notions of union, coproduct, and colimit are distinct concepts in category theory, so let's not get too involved with these.) Since in Axiom, sets are domains of SetCategory, accordingly,  Union (renamed) should be specified as:

IndexedUnion(I: SetCategory, g:I ->SetCategory):SetCategory

Example 1:
I:= Integer
g(i:I):SetCategory == if even? i then Integer else String
J:= IndexedUnion(I,g)

A more mathematical example would be to construct the prime field if i is prime, and a product of prime fields over factors of i if i is composite. In the next example, we construct the set of all square matrices with integer entries.

Example 2:
I:=Integer
g(i:I):SetCategory == SquareMatrix(i, Integer)
J:=IndexedUnion(i,g)

Technically, g here is a domain constructor. Whether the implementation should be done as primitive or not depends on language limitation of Spad. As we shall see, at the Spad level, we would need domains and categories to be first class objects and maps would need to allow input-dependent types as its output. So Axiom may not allow that.

As it currently exists, Union (in Axiom) can only form the disjoint union of a *finite* number of sets (each of which is a domain of SetCategory, NOT as elements of Set S for some domain S, which are finite subsets of S). The index set in the tagged version is the set of tags, but this is clearly not enough (there being no useful operations in the set of tags). The index set in the untagged version probably defaults to {1, ..., n} where n is the number of sets (domains) in the union or some n distinct strings generated randomly. (I did not check the code since Union is a primitive and its code lives below the algebra level -- not an excuse, just incompetence on the lower levels on my part).

The convenience of tags (in the case of a small, finite index set) is that the user does not have to make the set of tags into a domain and the tags are supposedly more meaningful to the user. Now, is a hybrid Union type desirable? Example 6 below will illustrate a possible use.
In my opinion, the "mixed" Union where tags are allowed for a small finite subset of the index set would allow the best of both worlds. Unfortunately, tags are strings (by definition) whereas there is no such restriction on an index set (or the rest of it). In most cases, for the index set to remain a domain, the indices must be homogeneous in type and so if there are tags, then the index set should be a subset of the set of all strings. In the finite case, it would be an *element* of Set String (and thus, not a *domain*).  But Union should allow infinite index sets as well and an infinite set of strings is difficult to manipulate in code.

One plausible reason why Union is implemented as a primitive rather than at the algebra level is to avoid having to require a user at the algebra level to make the index set into a *domain*.  To allow hybrid index set, it would be again simpler to implement as a primitive than at the algebra level as Bill Page proposed, because requiring the user to make the hybrid index set into a domain would be a bit harder and less intuitive. We need a domain constructor (which is easy to implement):

TagAsDomain( T: Set String): SetCategory

Note that Set String is used, not List String. This type of construction is already used in Axiom, as in the domain "failed" when we use Union("failed", ...). So it is probably handled specifically by the compiler, or there is a similar function at lower level. The above specification would enforce automatically the constraints Stephen thinks Spad is currently lacking (but documented, see hyperdoc on Union):

> I think the consensus is that `hybrid' Union types
> are not desirable.
> Consequently, I will look into making Spad strictly enforce this. In
> addition, the constraint that an untagged Union not have identically
> typed branches, and that in the tagged case all branch names are
> distinct.
Example 3:
I:= TagsAsDomain({"a", "b", "c"})
-- this would be {"a","b","c"} as a domain
g(i:I):SetCategory ==
  i = "a" => A
  i = "b" => B
  i = "c" => C
J:=IndexedUnion(I,g)

Clearly this is a bit awkward at the algebra level, compared to

Union(a:A, b:B, c:C)

But a compiler can easily translate the above into the detailed algebra code in Example 3. On the other hand, in this algebraic level version, there is no "untagged" Union (all domains in IndexedUnion are indexed) and the "untagged" version should not require any constraints such as the associated domains be distinct. It is only required that the elements of the index set be distinct, which is automatically enforced because it is a set. Indeed, hybrid union indexed by a heterogeneous set can be handled easily too, using IndexedUnion itself!

Example 4:
I:=IntegerMod(2)
L:=TagsAsDomain({"a","b","c"})
g(i:I):SetCategory ==
  zero? i => L
  IntegerMod(5)
J:= IndexedUnion(I,g)
f(j:J):SetCategory == ...
K:= IndexedUnion(J, f)

Again, it would be much easier to have this implemented enumeratively and perhaps as a primitive and allow the user to simply write, in case the index set is finite and small:

Union(a:A,b:B,c:C,D,E,F,G,H)

However, the more abstract specification of IndexedUnion is far more powerful.

Example 5:

I:=IntegerMod(2)
L:=TagsAsDomain({"a","b","c"})
g(i:I):SetCategory ==
  zero? i => L
  String
J:= IndexedUnion(I,g)
f(j:J):SetCategory == ...
K:= IndexedUnion(J, f)

In the definition of f, we can actually distinguish the "a" in L from the "a" in String because each element of IndexedUnion is "tagged" and we will use the "=" from L or from String (this is related to the scoping issue of current implementation raised by Gaby). Since J in Example 5 is itself an IndexedUnion object, this brings us to the "case" question, or more generally:

What should be exported from IndexedUnion?

Clearly, there needs to be a way to coerce elements from the domains into the union. If we were to adopt Bill Page's idea that the injections (and projections for Product or Record) should be named by tags, then it would be very clumsy to implement them when the Union is over a large finite set and impossible over an infinite set.  This may be one reason why Axiom separates Union into two versions, tagged (when the indexed set is finite and small) and untagged (the general case).  I can only think of two purposes of tags: (1) to distinguish cases when a domain occurs multiple times in the arguments of Union, and (2) for convenience of use.  The first of these can be handled by the index set and the second, too, but convenience depends on the size of the index set, as illustrated in the previous examples.

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)
 

These are just generalization of what currently exist but I get rid of the "case" and replace it with "index" and "value".  Instead of multiple overloading of "case" and "coerce", we now need only one (this afterall, is exactly the advantage of indexing over explicit enumeration). Of course, we need to be able to use input-dependent signatures. This is a requirement when we deal with heterogeneous objects. In Example 5, where J itself is defined using IndexedUnion, the function f may be defined in the following way. The example illustrates how IndexedUnion may be used.

Example 6 (Example 5 continued):

I:=IntegerMod(2)
L:=tagsAsDomain({"a","b","c"})
g(i:I):SetCategory ==
  zero? i => L
  String
J:= IndexedUnion(I,g)
f(j, J) :SetCategory ==
  jU := value(j)
  index(j) =$I 0 =>
     jU =$L "a" => A
     jU =$L "b" => B
     jU =$L "c" => C
  IntegerMod(#jU)
K:=IndexedUnion(J,f)

Of course this example is contrived. However, I can imagine constructions in mathematics over a set J where for a finite number of (exception) elements of J, there are two cases whereas for all the other there is only one. This would necessitate exceptional handling as in Example 6 above.

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

    Rep:= Record( index: I, value:g(i) )

if allowed would be perfect (note that Record is also a primitive, so let the lower level handle pointers). Record, categorically the product construction, should also be done using an index set. A plausible and trivial implementation of the exported functions is:

      x = y == (x.index = y.index) and (x.value = y.value)
      index(x) == x.index
      value(x)== x.value
      coerce(i:I, v:g(i)) == [i, v]$Rep
 
By generalizing TagsAsDomain, replacing String by any domain, we can create arbitrarily complicated index sets an IndexedUnion objects.
 

William