coercion problem

3 views
Skip to first unread message

Martin Rubey

unread,
Nov 14, 2008, 3:00:47 AM11/14/08
to fricas-devel, aldor-l, open-axiom-devel
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.

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

unread,
Nov 14, 2008, 3:48:36 AM11/14/08
to Martin Rubey, fricas-devel, aldor-l, open-axiom-devel
On 11/14/2008 09:00 AM, Martin Rubey wrote:
> 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

unread,
Nov 14, 2008, 5:40:51 AM11/14/08
to Ralf Hemmecke, fricas-devel, aldor-l, open-axiom-devel
Ralf Hemmecke <ra...@hemmecke.de> writes:

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

unread,
Nov 14, 2008, 9:04:47 AM11/14/08
to fricas...@googlegroups.com, aldor-l, open-axiom-devel
> 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 ?

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

unread,
Nov 14, 2008, 9:46:51 AM11/14/08
to Ralf Hemmecke, fricas...@googlegroups.com, aldor-l, open-axiom-devel
Ralf Hemmecke <ra...@hemmecke.de> writes:

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

unread,
Nov 14, 2008, 10:01:19 AM11/14/08
to Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel
> 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

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

unread,
Nov 14, 2008, 12:50:58 PM11/14/08
to Ralf Hemmecke, fricas...@googlegroups.com, aldor-l, open-axiom-devel
Ralf Hemmecke <ra...@hemmecke.de> writes:

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

unread,
Nov 14, 2008, 4:26:27 PM11/14/08
to Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel
I am still not getting it.

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

unread,
Nov 14, 2008, 4:34:29 PM11/14/08
to Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel
Martin,

put your concrete sample code here...

http://axiom-wiki.newsynthesis.org/SandboxIsomorphic

and then let's work on it.

Ralf

Waldek Hebisch

unread,
Nov 14, 2008, 5:11:43 PM11/14/08
to fricas...@googlegroups.com
Martin Rubey wrote:
>
> 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

unread,
Nov 14, 2008, 5:56:31 PM11/14/08
to fricas...@googlegroups.com
Martin Rubey wroteL

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

unread,
Nov 15, 2008, 3:21:06 AM11/15/08
to Ralf Hemmecke, Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel
Dear Ralf, Waldek,

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

unread,
Nov 15, 2008, 4:25:36 AM11/15/08
to Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel
> The concrete use case was to replace the 188 declarations of coerce by a
> 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

unread,
Nov 15, 2008, 5:09:51 AM11/15/08
to Ralf Hemmecke, Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel
Ralf Hemmecke <ra...@hemmecke.de> writes:

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

unread,
Nov 15, 2008, 6:15:27 AM11/15/08
to Martin Rubey, fricas...@googlegroups.com, aldor-l, open-axiom-devel

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

unread,
Nov 15, 2008, 6:30:17 AM11/15/08
to Ralf Hemmecke, fricas...@googlegroups.com, aldor-l, open-axiom-devel
Ralf Hemmecke <ra...@hemmecke.de> writes:

> 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

Reply all
Reply to author
Forward
0 new messages