[Aldor-l] [open-axiom-devel] [fricas-devel] Re: coercion problem

[Martin Rubey]

Ralf Hemmecke <ralf at 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