Re: Type coercicion (was: Re: [Axiom-developer] Re: Axiom interactive input syntax)

[nic]

On Wed, 2003-12-10 at 21:19, David MENTRE wrote:
> Hello,
> 
> nic <address@hidden> writes:
> 
> > I did some work on automatic type changing in the interpreter for my
> > thesis under James Davenport...
> 
> >From what I have understood from the introduction and conclusion, you
> have an algorithm to transform any "type"[1] in any other mathematically
> compatible "type" (provided the type system follows some mathematical
> guidelines). This makes me ask the following naïve and meta question:
> how would you use such an algorithm? From user behavior (tim-user uses
> variable x with another operator implying a new type context) or with
> explicit user information (calls to coerce)? Within a type inference
> algorithm? 

It "should" be invisible to the user (ie. during an internal call to
coerceInteractive() ).

The standard case being that Q[x] has a natural injection into Z(x)
( UPoly Frac Int -> Frac UPoly Int ).

So if a := ( ( 1/2 ) * x**2 + x - 1/3 ) (Upoly Frac Int) we are free to
add a member of Z, Q, Z(x) to it and will "work" without the user having
to call coerce.

That's not to say that it shouldn't be callable by the user, somehow.

It should also be noted that I think my algorithm is slow. The proof in
the thesis is a reverse-engineered hack. :-) Finally, I don't think
we'll be in a position to have Axiom's language like B-natural
(described in ISSAC '94: "How to Make AXIOM into a Scratchpad" Jenks and
Trager). There will always be cases where users have to coerce (or
worse, cast e.g. Q -> Float). I don't think that my work is a panacea
for all ills but it should help and is mathematically sound in a large
number of day-to-day cases.

nic
-- 
nic <address@hidden>