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

[Martin Rubey]

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