Re: [Axiom-developer] Unions in Spad

[William Sit]

Stephen Wilson wrote:

> William Sit <address@hidden> writes:
> > 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.
>
> Ok. I believe that the IndexedUnion implementation might need to wait
> until some basic support can be made available in the compiler.

At first, I wrote down "True."  After finishing writing up most of this 
message, I have second
thoughts. See discussions below.

> I believe that 1) is realistic as a near-term extension, at least
> within Spad code.  I do not know a lot about the interpreter
> implementation so am unsure how much work is involved there.

Well, would making it work for the compiler be any easier? The difficulty I 
found regarding (1)
(after trying for two days, crashing Axiom time and again: see

      http://wiki.axiom-developer.org/AxiomColloquium/IndexedUnion

) is the following. The user can only input a list of domains as a string 
input, like
"[Integer, SQMATRIX(5, INT)]".  We need to translate this into a list of 
domains, and I mean
each is a genuine domain, not as an SExpression as in

dom(sample()$Integer)  -- this gives (Integer) where Integer is a Symbol
dom(sample()$SQMATRIX(5,INT) -- this gives (SquareMatrix (5 (Integer)))

Here is an example of a genuine domain:
p:=POLY FRAC INT
a:p := (2*x+1)

p is typed Domain in the interpreter, and I can find no way to make a 
SExpression like
(Polynomial (Fraction (Integer))) into the *domain* p.  Question: how is a 
domain represented
internally in Lisp? It seems something like (|Integer|) but that is just a 
symbol, not the real
McCoy. So for example, how is p above represented? In general, it seems some 
type of parsing is
needed to unwind the pieces building up to say SquareMatrix(5, Integer). What 
are the lisp
functions that does the parsing? (I can only find an unparse function in 
InputForm). Also, what
lisp function translate the abbreviation to the full domain name?

Is Domain really a domain? category? Is it a primitive type like Union? If so, 
what are its
exports?

> Given 1), does 2) not follow by defining SetAsDomain as a domain constructor?

(1) simply asks to construct say [Integer, String] or {Integer, String}, which 
is a list or a
set whose elements are domains (not just domain identifiers, see above). That 
means the result
has to belong to (or be an element of) a containing domain (but the result 
itself is not a
domain) such as List Domain or Set Domain (these only allow finite sets), and 
more generally,
List SetCategory and Set SetCategory.  (2) makes a domain of SetCategory 
consisting of
elements that are domains, possibly anonymous as in SetAsDomain({Integer, 
String}) which
returns a domain with only two elements, namely, the domains Integer, and 
String. This domain
is needed so that we can code signatures of maps into this two-element set (in 
the example),
such as
       g: I -> SetAsDomain([Integer,String]).
Thus SetAsDomain is a domain constructor, whereas {Integer, String} is just a 
list (element
constructor). Of course, mathematically, we view
       g:I->{Integer,String}
as valid but this is "by abuse of language" (the reason I did not notice the 
mistake at first
-- a key observation, by the way). It would seem fairly easy to turn elements 
of Set S or List
S into a domain for any given S: BasicType. I tried, see above URL, not easy at 
all for me.
Moreover, we are now at one level higher where S is a category, and we can't 
even talk about
List SetCategory or Set SetCategory, yet.  Here, I have "lowered" the status of 
the map g to a
function instead of a domain constructor. Maybe that is where the problems lie.
Ideally, mathematics requires even another higher level, to talk about sets of 
(small)
categories.

> However, 3) and 4) might require a large amount of work.  This is
> something I am more than willing to do.

Thank you. It affects something very basic (and the solution may be ... read 
on).

> However, a few notes:
>
> Once we have a working Axiom atop GCL-2.7.0, this opens up a new world
> for developers (an ANSI lisp).   I am trying to get that working with
> the hopes that I can exploit the new features in an attempt to
> reimplemented the compiler.  This is a huge task, of course, but I think
> it is attainable.
>
> The rewrite can attempt to accommodate the needs and issues raised by
> yourself and others.  On an item by item basis, this might prove to be
> easier in the context of a rewrite than trying to shoehorn more
> features into the existing system, and to do so in a way such that
> little or nothing else breaks.
>
> What Im trying to decide here is how best I can focus my efforts.  I
> am reluctant to invest a huge amount of time in extending a system I
> have every intention of rewriting!  I realize that this is quite
> selfish of me, for putting my own interests and goals first.  I do so
> only because I think the returns are greater in the long run, compared
> to expanding the current implementation over the course of the next
> thirty years.

Well, I no longer expect this to be simple. The original implementers probably 
also were
unwilling to attempt such a generality and hence settled for two versions. 
Maybe Union can be
modified just to enforce the current restrictions and to fix the problem about 
repeated domains
with distinct tags. (Otherwise, users need just be aware of the problems. I 
don't think the
generality is needed soon.)

> > (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)
>
> I know where the second error message is generated (and I think even
> that could be better).  The first I dont know off hand.  But I can put
> this issue into my todo list.

Thanks.

> [...]
> > >> 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.
>
>
> Perhaps the best solution in this case is as Bill Page suggested,
> implementing keyword arguments in Axiom, allowing us to write [a:1] or
> [b:1] thus enabling unambiguous specification of the branch.

The solution is simpler than that. Currently, in Union(a:Integer, b:Integer), 
we already have:
 ?=? : (%,%) -> Boolean                ?case? : (%,a) -> Boolean
 ?case? : (%,b) -> Boolean             coerce : % -> OutputForm
 construct : Integer -> %              construct : Integer -> %
 ?.? : (%,a) -> Integer                ?.? : (%,b) -> Integer

So all it takes is to replace the two "construct" to become:

construct: (Integer, a) -> %
construct: (Integer, b) -> %

Granted, when we have more domains in the Union, this is clumsy (that is the 
reason to
introduce the more general set up IndexedUnion).

WAIT! These signatures in tagged Union are outrageous (abuse of language)! 
Neither identifier a
nor identifier b is a domain! The implementers again finessed the difficult 
problems raised in
(1) to (4). They are more pragmatic than you think.

By the way, in untagged Union, we already require domains to be distinct. For 
example,
Union(Integer, String), we have:

 ?=? : (%,%) -> Boolean                autoCoerce : % -> Integer
 autoCoerce : % -> String              autoCoerce : Integer -> %
 autoCoerce : String -> %              ?case? : (%,Integer) -> Boolean
 ?case? : (%,String) -> Boolean        coerce : % -> Integer
 coerce : % -> OutputForm              coerce : % -> String

I don't know why there are autoCoerce:%->Integer and coerce:%->Integer 
(similarly for String).
Indeed, there is NO autoCoerce! It is not clear to me how an element from 
Integer or String is
coerced into the Union (that is, what function performs the coercion? most 
likely, "pretend"?)

(1) -> dom:=Union(Integer, String)

   (1)  Union(Integer,String)
                                                                 Type: Domain
(2) -> )set mess auto off
(2) -> )set mess bot on
(2) -> a:dom:=5

   (2)  5
                                                     Type: Union(Integer,...)
(3) -> b:dom:="5"

   (3)  "5"
                                                      Type: Union(String,...)
(4) -> a::Integer

   (4)  5
                                                                Type: Integer
(5) -> autoCoerce(a)@Integer

 Function Selection for autoCoerce
      Arguments: INT
      Target type: INT
   -> no appropriate autoCoerce found in Integer
   -> no appropriate autoCoerce found in Integer
   -> no function autoCoerce found for arguments INT
   There are no library operations named autoCoerce
      Use HyperDoc Browse or issue
                             )what op autoCoerce
      to learn if there is any operation containing " autoCoerce " in
      its name.

   Cannot find a definition or applicable library operation named
      autoCoerce with argument type(s)
                                   Integer

      Perhaps you should use "@" to indicate the required return type,
      or "$" to specify which version of the function you need.
(5) -> )di op autoCoerce
   autoCoerce is not a known function. AXIOM will try to list its
      functions which contain autoCoerce in their names. This is the
      same output you would get by issuing
                         )what operations autoCoerce

   There are no operations containing those patterns

(5) -> c:=autoCoerce("5")$dom

   The function autoCoerce is not implemented in Union(Integer,String)
      .
(5) -> c:=coerce("5")$dom

   The function coerce is not implemented in Union(Integer,String) .


> Note too that this, I believe, is a necessary first step in getting
> defendant types working in Spad.  Currently there is no propagation of
> binding information in the `modemaps' for functions.

I'm surprised. In tagged Union, the tags are somehow memorized by the system 
and hard wired
into the signatures (recall: by abuse of language). They are thus "local".  
Continuing with the
previous Axiom session:

(9) -> dom3:=Union(a:Integer, b:Integer)

   (9)  Union(a: Integer,b: Integer)
                                                                 Type: Domain
(10) -> a3:dom3:=a

   (10)  5
                                       Type: Union(a: Integer,b: Integer,...)
(11) -> a3 case a

   (11)  true
                                                                Type: Boolean
(12) -> a3 case b

   (12)  false
                                                                Type: Boolean
(13) -> a

   (13)  5
                                                     Type: Union(Integer,...)
(14) -> b

   (14)  "5"
                                                      Type: Union(String,...)
(15) -> a3 case Integer

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

protected-symbol-warn called with (NIL)

The tags in Union (and similarly for Record) seem to be local, but may be 
overshadowed if the
tags are used as identifiers (see another example in
http://wiki.axiom-developer.org/AxiomColloquium/IndexedUnion). I think the 
current choice of
implementing Union and Record as primitive types is simpler than keyword 
arguments (which seems
to add another indirect layer). As primitive types, abuse of language is 
allowed (or rather,
there is no language to abuse at pre-algebra time)!

> We could look at
> how is information is retained for functors and perhaps find some
> inspiration for making it work in arbitrary functions (after all, the
> mechanics is effectively already in place for dependent types as
> handled by domain constructors).

Yes, that is probably because such dependencies can be handled without regard 
to language
restrictions. If we want to have this at the algebra level (or rather non 
primitive type
level), it would be quite difficult. The" mechanics" are very different.

In view of the "abuse of language" observation, I think it should be possible 
to implement the
"tools" for (1)-(4) by creating a few (perhaps primitive) types:

(a) a primitive type Domain:SetCategory  which contains as its elements all 
domains (including
of course, those constructed using domain constructors and their arguments). 
This is probably
already available as "Domain" mentioned earlier, but perhaps not "formally" 
exported and the
interpreter does not recognize it. If we do dom(x::Any), the interpreter will 
return the domain
of x, but only as an SExpression. However, "Domain" is not even a valid type!  
So we need to
make this available at the algebra level and to be able to use it as any other 
domain. Not that
while in principle, the set of domains should really be a category, but that 
would make it
harder to interface (List Domain or Set Domain would not parse if Domain is a 
category). For
data representation of a domain in Domain, we probably can get away with just 
retaining the
necessary identifiers needed to construct and thus SExpression should be good 
enough (much like
in Any). Equality would be equality of SExpression. The key point is to 
restrict these
SExpressions to those defining valid domains only.

The difficulty with this representation, as mentioned earlier, is how to 
convert SExpression
for domain into the real domain. (b) Given (a), we can safely construct Set 
Domain and List
Domain for finite lists and sets of domains, This satisfies (1).

(c) A domain for SetAsDomain.  I tested some algebra level code in two domains 
MyDomain and
ListAsDomain, on the AxiomColloquium page. I need help to fix some crashes in 
SetAsDomain and
List MyDomain.

(d) A domain for the set of maps g: I ->SetCategory.  Not sure about this yet. 
I tested a
lowered g:I->List MyDomain instead (it's a function rather than the domain 
constructor).

Will try some more when I have more time. Meanwhile, any help is welcome.




William