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

[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