[Top][All Lists]
[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: |
Sun, 15 Jul 2007 17:28:47 -0400 |
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
- Re: [Axiom-developer] Unions in Spad, (continued)
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, Gabriel Dos Reis, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, William Sit, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/12
- Re: [Axiom-developer] Unions in Spad, William Sit, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Bill Page, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, William Sit, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, William Sit, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Ralf Hemmecke, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/13
- Re: [Axiom-developer] Unions in Spad,
William Sit <=
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/15
- Re: [Axiom-developer] Unions in Spad (Correction), William Sit, 2007/07/13
- Re: [Axiom-developer] Unions in Spad (Correction), Stephen Wilson, 2007/07/13
- [Axiom-developer] Re: keyword arguments, was: Unions in Spad (Correction), Martin Rubey, 2007/07/14
- Re: [Axiom-developer] Re: keyword arguments, was: Unions in Spad (Correction), Bill Page, 2007/07/21
- Re: [Axiom-developer] Unions in Spad, Ralf Hemmecke, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Ralf Hemmecke, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Ralf Hemmecke, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/13
- Re: [Axiom-developer] Unions in Spad, Stephen Wilson, 2007/07/13