axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Unions in Spad


From: William Sit
Subject: Re: [Axiom-developer] Unions in Spad
Date: Fri, 13 Jul 2007 02:24:36 -0400


William Sit wrote:

> In the proposed IndexedUnion, what is missing is the Rep:= Record[index:I, 
> value:
> g(i)].

     Actually, this can probably be similated by Record(i:I, x:Any) to avoid 
dependent
types.

However, there is another problem: the signature of the index map
     g: I->List SetCategory
has syntax problem. (So, alas, all my examples inherit this problem.) A list 
(more
correctly, a set) of domains in the SetCategory is NOT a domain and hence 
cannot be used as
the target of a map. So we have to turn a list or set into a domain, much like 
turning a
list of tags into a domain (TagsAsDomain).  Here however, we are one level 
higher because
we are trying to make a set of *domains* such as {Integer, String} into a 
domain.

While there is probably a way to do this in Lisp, the question is how should a 
user of
Axiom input this map g? It looks like we need to capture this at the algebra 
level and make
all these maps into a domain, too. So domains and perhaps even categories must 
be first
class objects. Unfortunately, even the domain Any does not capture sets of 
domains as
objects.  This despite the Rep for Any is Record(dm:SExpression, ob:None). The 
Interpreter
refuses to convert domains into objects of Any.

-> (1) k:List Any:= [Integer, String]

    Cannot convert an element of the construct to type Any.


In summary, we need:


(1) make a list or set of domains from SetCategory (or any category) a legal 
construction
(2) SetAsDomain to convert a list or set of domains (or elements, or maps, 
perhaps or
categories) as a domain of SetCategory
(3) Record to accept dependent types, such as [i: I, x:g(i)]
(4) maps such as g: I -> SetAsDomain([Integer, String]) should be first class 
objects and
used as parameters, and definable in the Interpreter.

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.

William







reply via email to

[Prev in Thread] Current Thread [Next in Thread]