coercion problem

[Martin Rubey]

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



_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

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

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Martin Rubey]

Ralf Hemmecke <ralf@...> 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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

> 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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Martin Rubey]

Ralf Hemmecke <ralf@...> 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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

> 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

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Martin Rubey]

Ralf Hemmecke <ralf@...> writes:

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

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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

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

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

Martin,

put your concrete sample code here...

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

and then let's work on it.

Ralf

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Martin Rubey]

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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

> 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

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Martin Rubey]

Ralf Hemmecke <ralf@...> 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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Ralf Hemmecke]

On 11/15/2008 11:09 AM, Martin Rubey wrote:

> Ralf Hemmecke <ralf@...> 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.

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

_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org

[Martin Rubey]

Ralf Hemmecke <ralf@...> 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


_______________________________________________
Aldor-l mailing list
Aldor-l@...
http://aldor.org/mailman/listinfo/aldor-l_aldor.org