3 views

Skip to first unread message

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.

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

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.

> 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

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

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.

> 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

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

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

> 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

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

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

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

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.

>

>

> 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

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.

>

>

> 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

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

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.

> 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

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

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

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

Search

Clear search

Close search

Google apps

Main menu