Re: [Axiom-developer] Unions in Spad

[Stephen Wilson]

Hello William,

This is excellent!  Thanks for all the work here!

I am going to keep going over these issues, and do my best to think
about the possible solutions.  I will just mention the things which I
can make a bit of sense of at the moment.

William Sit <address@hidden> writes:
[...]
> ) 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? 

Well, since you asked, I will try and give a partial answer (I cannot
yet give a full one).

There are two ways.  (|Integer|) evaluates to a domain vector.
This is an efficient but hairy representation used by the compiler
runtime:

  (1) -> )lisp (|Integer|)
  
  Value = #<vector 08b4b8a4>

I need to write down the details I know about this structure, and
figure out the details Im still clueless about.

Thats half the story, as far as the compiler is concerned.  We also
have the database:

  (1) -> )lisp (pprint (getdatabase '|Integer| 'constructormodemap))

  (((|Integer|)
    (|Join| (|IntegerNumberSystem|) (|ConvertibleTo| (|String|))
            (|OpenMath|)
            (CATEGORY |domain| (SIGNATURE |random| ($ $))
                (ATTRIBUTE |canonical|) (ATTRIBUTE |canonicalsClosed|)
                (ATTRIBUTE |noetherian|) (ATTRIBUTE |infinite|))))
   (T |Integer|))
  Value = NIL

This is an example of the ambient information the compiler has
available to reason about types.


To make matters more confusing, the interpreter deals with things in
its own set of data structures.  So if you start Axiom afresh:

  (1) -> p := POLY FRAC INT

     (1)  Polynomial Fraction Integer
                                                                 Type: Domain
  (2) ->  )lisp (let ((*print-circle* t)) (pprint |$interpreterFrameRing|))

  ((|initial|
       ((((% (|value|
              . #0=(#1=(|Domain|) WRAPPED
                    . #2=(|Polynomial| (|Fraction| (|Integer|))))))
          (|p| (|value| . #3=(#1# . #2#))))))
       2 T
       #4=(NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL NIL
               NIL NIL NIL NIL NIL ((|p| (|value|))) . #4#)
       20 1 NIL
       ((1 "p := POLY FRAC INT" (% (|value| . #0#))
         (|p| (|value| . #3#))))
       #<vector 08c9fbec>))
  Value = NIL

As I mentioned, I dont know a lot about the interpreter, but:

      (|p| (|value| . #3=(#1# . #2#)))

means, basically:

      (|p| (|value| |Domain| |Polynomial| (|Fraction| (|Integer|))))

So we can see that the information about p is available.  Combined
with the domain vector and the database, the Interpreter has all the
information it needs in the above.

> 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?

We should investigate the following:

   (1) -> )lisp (|ncParseFromString| "SquareMatrix(5, Integer)")

   Value = (|SquareMatrix| 5 |Integer|)

As for abbreviations, one could do:

   (1) -> )lisp (get 'INT 'ABBREVIATIONFOR)

   Value = |Integer|


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

Its not really anything that has a proper name, as far as I know.  Its
not a primitive in the same way Union is, nor is it defined with
exports from what I can see.  Its just a `special case'.

> > 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. 

OK.  Many thanks for the clarification. 

[...]
> 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.)

Yes.  This is definitely workable in the short term.  I will get this
done over the next few weeks along side finishing the gcl-2.7.0 port.

[...]
> > 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) -> %

OK.  I can look into this too.  Axiom has a lot of undocumented
assumptions built in but with any luck this might be doable.

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

Absolutely agreed.

[...]
> 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"?)

There is a one line comment in the code (buildom.boot.pamphlet):

     ['autoCoerce,[t,g],downFun], --this should be removed eventually

So obviously the original implementers didnt want autocoerce around.

I notices the lack of coerce: % -> Integer, and it struck me as
lacking symmetry, but I thought that the `.' operators would handle
that case.  Also, for coercion from integer or string into the Union
one can use construct equivalently I believe.  Perhaps I am
overlooking something?

[...]
> 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)!

I did not notice the shadowing before.  Thanks!  

I completely agree that working at the level of primitive types is the
simplest approach.

[...]
> 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.

I will see if I can get a sense of direction for possible solutions.
Looking at the AxiomColloquium page and experimenting with the code
you have there will give me some `hands on' examples to work with. Of
course I will let you know of any progress.


Take care,
Steve