coercion problem
Martin Rubey
does not seem to have.
In Axiom, we currently have the (mostly unused) Categories
CoercibleTo S, RetractableTo S and ConvertibleTo S that provide
coerce: % -> S, coerce: S -> % and retract: % -> S
respectively. One can then ask
(4) -> SquareMatrix(2, INT) has CoercibleTo Matrix INT
(4) true
Type: Boolean
Very unfortunately, currently in almost all cases the query "has CoercibleTo
Something" will return false, because the coerce function is not inherited by
the category.
Now, I would like that for domains of the same category, say
UnivariatePolynomialCategory, that differ only in the representation of their
elements, say sparse or dense, we would have
A has CoercibleTo B and B has CoercibleTo A
Eg., we could have a package
UPOLYCoerce(A: UPOLYC, B: UPOLYC)
that implements coerce: A -> B generically, using only operations from the
category UPOLYC.
But it seems that we cannot teach Aldor/SPAD, that for all domains A and B of
UPOLYC we have
A has CoercibleTo B and B has CoercibleTo A
In Sage/python, this seems possible, although I'm not quite sure about it.
There, people implement a general coerce method in UPOLYC, that checks whether
it's argument is of the right type. I admit, I do not know whether we can then
ask for two given types whether we can do the coercion. Sorry for being very
vague here, I simple do not know the details.
Martin
Ralf Hemmecke
> I'd like to report on a curious problem I have with SPAD/Aldor, which Python
> does not seem to have.
>
> In Axiom, we currently have the (mostly unused) Categories
>
> CoercibleTo S, RetractableTo S and ConvertibleTo S that provide
>
> coerce: % -> S, coerce: S -> % and retract: % -> S
>
> respectively.
Not quite true.
CoercibleTo(S:Type): Category == with
coerce: % -> S
ConvertibleTo(S:Type): Category == with
convert: % -> S
RetractableTo(S: Type): Category == with
coerce: S -> %
retractIfCan: % -> Union(S,"failed")
retract: % -> S
add
retract(s) ==
(u:=retractIfCan s) case "failed" => error "not retractable"
u
> Very unfortunately, currently in almost all cases the query "has CoercibleTo
> Something" will return false, because the coerce function is not inherited by
> the category.
> Now, I would like that for domains of the same category, say
> UnivariatePolynomialCategory, that differ only in the representation of their
> elements, say sparse or dense, we would have
> A has CoercibleTo B and B has CoercibleTo A
OK, let's say I take AbelianMonoid as a category. For A, I take Integer
and for B, I take String (just let's suppose 0: String is the empty
string and +: (String, String) -> String is concatenation.
One can easily find the homomorphism (of monoids) #: String -> Integer
(the length of the string) in one direction and call it coerce. But the
other direction I find a bit difficult to come up with. ;-)
Looks like your specification of the problem is too imprecise.
Ralf
Martin Rubey
> > Now, I would like that for domains of the same category, say
> > UnivariatePolynomialCategory, that differ only in the representation of
> > their elements, say sparse or dense, we would have
>
> > A has CoercibleTo B and B has CoercibleTo A
>
> OK, let's say I take AbelianMonoid as a category. For A, I take Integer and
> for B, I take String (just let's suppose 0: String is the empty string and +:
> (String, String) -> String is concatenation.
One can hardly say that these two domains differ only in the representation of
their elements.
So, I should have been more precise:
There are categories (like for example UPOLYC), where it makes sense to have
for any two domains A and B of that category
A has CoercibleTo B and B has CoercibleTo A.
However, it seems that this cannot be expressed in SPAD or Aldor.
Somehow, it might be nice to have the possibility to say
with CoercibleTo B where B has SomeCategory
Martin
Ralf Hemmecke
> their elements.
Well, what about Dom1, Dom2, and DomS on
http://axiom-wiki.newsynthesis.org/SandboxIsomorphic ?
They are in some sense isomorphic. At least that is my intention.
> So, I should have been more precise:
> There are categories (like for example UPOLYC), where it makes sense to have
> for any two domains A and B of that category.
> A has CoercibleTo B and B has CoercibleTo A.
I don't think you can state that for any two A and B. As in my previous
example, I can certainly give a domain that doesn't work well. How do I
map a domain with 3 variables into one with 2 variables. And back? Do
you assume that mapping back and forth is the identity?
> However, it seems that this cannot be expressed in SPAD or Aldor.
To me it seems that you still have not made the task fully precise.
> Somehow, it might be nice to have the possibility to say
> with CoercibleTo B where B has SomeCategory
See http://axiom-wiki.newsynthesis.org/SandboxIsomorphic .
define IsIsomorphicTo(C: Category, T: C): Category == with {
coerce: % -> T
}
If you want to remove the C from above then that is something that Gaby
and Stephen talked about at the Aldor & Axiom Workshop
(http://axiom-wiki.newsynthesis.org/uploads/WattDosReis-MultisortedAlgebras.pdf)
and which indeed is not yet in Aldor.
But I somehow believe that even if it were possible, it wouldn't help
you in what you are thinking about. Can you be even more explicit. I am
asking for it, because besides the categories one also has to think of
how one actually could implement the respective coercion functions.
Ralf
Martin Rubey
> > One can hardly say that these two domains differ only in the representation of
> > their elements.
>
> Well, what about Dom1, Dom2, and DomS on
> http://axiom-wiki.newsynthesis.org/SandboxIsomorphic ?
Oh dear, it seems difficult to explain what I'm thinking of. All I want is:
> > Somehow, it might be nice to have the possibility to say
>
> > with CoercibleTo B where B has SomeCategory
Of course, this only makes sense for some very special Categories. But then it
makes a lot of sense. For example, for categories, that provide a common
interface to different *representations* of univariate polynomials - sparse or
dense, or matrices, sparse or dense, etc.
> define IsIsomorphicTo(C: Category, T: C): Category == with {
> coerce: % -> T
> }
> But I somehow believe that even if it were possible, it wouldn't help you in
> what you are thinking about. Can you be even more explicit. I am asking for
> it, because besides the categories one also has to think of how one actually
> could implement the respective coercion functions.
I don't see how this would help. As I said, I can have
UPOLYCoerce(A: UPOLYC, B: UPOLYC): with
coerce: A -> B
add
coerce a ==
resta := a
res: B := 0
while not zero? resta repeat
res := res + leadingCoefficient resta * leadingMonomial resta
resta := reductum resta
res
and this will provide a coercion function from any A to any B in UPOLYC, but I
cannot state that for any A and any B in UPOLYC
A has CoercibleTo B
(of course, I want to *state* it, I do *not* want the language to deduce it by
some magic.)
Martin
Ralf Hemmecke
> coerce: A -> B
>
> add
> coerce a ==
> resta := a
> res: B := 0
> while not zero? resta repeat
> res := res + leadingCoefficient resta * leadingMonomial resta
> resta := reductum resta
> res
> and this will provide a coercion function from any A to any B in UPOLYC
In other words, for any A and B you have a package that implements
coerce: A->B. OK.
> but I cannot state that for any A and any B in UPOLYC
> A has CoercibleTo B
Now why do you think this is still important? Onces *you* have
programmed UPOLYCoerce and you know that A: UPOLYC and B: UPOLYC then
everything is clear and you can simply say (for a: A)
b: B := coerce(a)$UPOLYCoerce(A,B)
I see no need to require "A has CoercibleTo B". Perhaps, I still didn't
get your point.
Ralf
Martin Rubey
Well, I may want to code
if A has CoercibleTo SparseUnivariatePolynomial R
then ...
This will "work" only for those A for which I have explicitly stated
CoercibleTo SparseUnivariatePolynomial R.
In a different package, I may want to ask
if A has CoercibleTo UnivariatePolynomial(x, R)
then ...
Of course, this is not really a problem if there are only two or three
implementations of univariate polynomials, say A, B and C. In A I say
with { CoercibleTo B; CoercibleTo C; }
in B I say
with { CoercibleTo A; CoercibleTo C; }
in C I say
with { CoercibleTo A; CoercibleTo B; }
But somehow, this looks suboptimal.
Martin
Ralf Hemmecke
If you have some A that doesn't just come from heaven. Maybe if your
current domain is of type UPOLYC you are satisfied to ask for the other
domain:
if A has UPOLYC then
-- use the coerce from your UPOLYCoerce package
I think, I stop here and wait for very concrete use cases of yours.
Maybe you send me some concrete pieces of your code and we stop spamming
the list until we have a result.
Ralf
Ralf Hemmecke
put your concrete sample code here...
http://axiom-wiki.newsynthesis.org/SandboxIsomorphic
and then let's work on it.
Ralf
Waldek Hebisch
>
> I'd like to report on a curious problem I have with SPAD/Aldor, which Python
> does not seem to have.
>
> In Axiom, we currently have the (mostly unused) Categories
>
> CoercibleTo S, RetractableTo S and ConvertibleTo S that provide
>
> coerce: % -> S, coerce: S -> % and retract: % -> S
>
> respectively. One can then ask
>
> (4) -> SquareMatrix(2, INT) has CoercibleTo Matrix INT
>
> (4) true
> Type: Boolean
>
> Very unfortunately, currently in almost all cases the query "has CoercibleTo
> Something" will return false, because the coerce function is not inherited by
> the category.
>
Hm, AFAICS CoercibleTo(X) is properly inherited. Only X is a fixed
domain. But I belive that intended usage of CoercibleTo was for
cases like CoercibleTo(OutputForm).
> Now, I would like that for domains of the same category, say
> UnivariatePolynomialCategory, that differ only in the representation of their
> elements, say sparse or dense, we would have
>
> A has CoercibleTo B and B has CoercibleTo A
>
> Eg., we could have a package
>
> UPOLYCoerce(A: UPOLYC, B: UPOLYC)
>
> that implements coerce: A -> B generically, using only operations from the
> category UPOLYC.
>
> But it seems that we cannot teach Aldor/SPAD, that for all domains A and B of
> UPOLYC we have
>
> A has CoercibleTo B and B has CoercibleTo A
>
Well, currently:
(6) -> InputForm has CoercibleTo(InputForm)
InputForm has CoercibleTo(InputForm)
(6) false
and I am not sure if we really want A CoercibleTo(A) to be true
(we must be careful to make sure that search for coercions does
not loop).
Considering your main question: currently Spad do not have
"first class" categories. Trurly first class categories,
more precisely computing list signatures at runtime means
trouble with overloading. Namely, in such case dispatching
(overload resolution) should happen at runtime. This is no
problem in languages like Python or Lisp where dispatching
is on types of arguments. But in Spad functions may be
overloaded on return type, such overload is rather nasty
to resolve at runtime -- one would be forced to run separate
copy of program for each possible retrun type and kill
all copies which lead to type error.
If you agree that you can call only "statically" known
signatures, then this is a significant restriction on
how categories can be used. In particular, it limits
what you can do with things like Foo(X) where X is
a category. Another question is using "forall" types
(your semantics of CoercibleToCat is essentially forall
type): I think that such types would be a nice addition,
but first we should work out semantics to make sure
that we do not fall into some trap (like conflict
with overloading).
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Waldek Hebisch
>
> Well, I may want to code
>
> if A has CoercibleTo SparseUnivariatePolynomial R
> then ...
>
> This will "work" only for those A for which I have explicitly stated
> CoercibleTo SparseUnivariatePolynomial R.
>
> In a different package, I may want to ask
>
> if A has CoercibleTo UnivariatePolynomial(x, R)
> then ...
>
> Of course, this is not really a problem if there are only two or three
> implementations of univariate polynomials, say A, B and C. In A I say
>
> with { CoercibleTo B; CoercibleTo C; }
>
> in B I say
>
> with { CoercibleTo A; CoercibleTo C; }
>
> in C I say
>
> with { CoercibleTo A; CoercibleTo B; }
>
> But somehow, this looks suboptimal.
>
Martin, I feel that in general there is a problem. But I think
that your example is not the best one. First, new code is
usually less problematic than old code: you can design new
code in such a way that various workarounds work. Real
problem is with old code: we do not want to go back to old
code and re-write all of it. Second, if you deal with single
category you can just test for this category:
if A has UnivariatePolynomialCategory(R) and _
B has UnivariatePolynomialCategory(R) then
....
Third, for coercion it is natural to have a "pivot domain" P,
so that coerce: A -> B is a composition of coercions from
A to P and coercions from P to B.
Let me also mention a more general workaround: for each category
of interest you define special fake domain which serves a label
for your category. Then instead of using:
CoercibleToCat(A, B)
you would use:
CatA(...): Category == Join(Labeled(LabelA(...), ....
(note: LabelA receies the same parameters as CatA, to make sure
that equality of labels implies equality of categories)
CoercibleToCatLabeld(A, B, LabelA): Category == with _
if A has Labeled(LabelA) and B has Labeled(LabelA) then _
coerce: A -> B
Of course, you still have to make sure that labels are available
when needed, but this is part of general Axiom design: you can
not query about domains from outside, you need to have information
passed explicitly.
--
Waldek Hebisch
heb...@math.uni.wroc.pl
Martin Rubey
Due to other, by far more pressing issues, I'd like to stop work on this thread
for now. I should have put in large letters at the beginning:
This is a theoretical question, no need for action right now.
> I think, I stop here and wait for very concrete use cases of yours.
The concrete use case was to replace the 188 declarations of coerce by a
handful of declarations of CoercibleTo in the SPAD library. I think that this
would make the library more user-friendly, and could be a first step towards
removing i-coerce and i-coerfn.
But I hesitate to write
UnivariatePolynomial(var, R) == with Join(CoercibleTo SUP R,
CoercibleTo Polynomial R,
CoercibleTo DMP([var], R),
CoercibleTo MPOLY([var], R) ...)
This doesn't look right.
Martin
Ralf Hemmecke
> handful of declarations of CoercibleTo in the SPAD library.
Maybe you should also read Doye's thesis. As far as I remember, he also
says something about how the autocoercion should work. (I somehow refer
to what Waldek said about not producing needless loops in the coercion
graph.) There is a whole theory behind coercions. Just adding some here
and there is not right (in my opinion).
> I think that this
> would make the library more user-friendly, and could be a first step towards
> removing i-coerce and i-coerfn.
> But I hesitate to write
>
> UnivariatePolynomial(var, R) == with Join(CoercibleTo SUP R,
> CoercibleTo Polynomial R,
> CoercibleTo DMP([var], R),
> CoercibleTo MPOLY([var], R) ...)
>
> This doesn't look right.
Doesn't seem to look right. But how else would you want to export
coerce: % -> X
for any of the replacements for X from above? They must statically be
given at compile time or (if "extend" where available) could be added
later (but also at compile time).
Ralf
Martin Rubey
> > But I hesitate to write
> > UnivariatePolynomial(var, R) == with Join(CoercibleTo SUP R,
> > CoercibleTo Polynomial R,
> > CoercibleTo DMP([var], R),
> > CoercibleTo MPOLY([var], R) ...)
> > This doesn't look right.
>
> Doesn't seem to look right. But how else would you want to export
>
> coerce: % -> X
>
> for any of the replacements for X from above? They must statically be given at
> compile time or (if "extend" where available) could be added later (but also at
> compile time).
Yes, *exactly* this was my question. And since I think it's a language
problem, I also sent it to aldor-l.
Maybe Christian Aistleitner has an idea...
Martin
Ralf Hemmecke
What about putting
toHere: (X: UPOLYC) -> X -> %
into the category of UPOLYC and then
toHere(X: UPOLYC)(x: X): % == coerce(x)$UPOLYCoerce(X, %)
as default implementation?
It's not exactly like a simple coerce, but you get rid of explicitly
stating all the CoercibleTo X exports.
Ralf
Martin Rubey
> What about putting
>
> toHere: (X: UPOLYC) -> X -> %
>
> into the category of UPOLYC and then
>
> toHere(X: UPOLYC)(x: X): % == coerce(x)$UPOLYCoerce(X, %)
>
> as default implementation?
just to make the analogy with CoercibleTo:
coercibleTo: (X: UPOLYC) -> % -> X
add
coercibleTo(X: UPOLYC)(x: %): X == coerce(x)$UPOLYCoerce(%, X)
> It's not exactly like a simple coerce, but you get rid of explicitly stating
> all the CoercibleTo X exports.
But it's a very nice idea, maybe we can extend it somehow...
A has with coercibleTo(SparseUnivariatePolynomial R):
% -> SparseUnivariatePolynomial R
or even
A has with coercibleTo(SparseUnivariatePolynomial R)
?
However, in truth I think one needs:
> Another question is using "forall" types
> (your semantics of CoercibleToCat is essentially forall
> type): I think that such types would be a nice addition,
> but first we should work out semantics to make sure
> that we do not fall into some trap (like conflict
> with overloading).
Martin