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