Re: [Caml-list] Type Inference and Overloading

[skaller <skaller@users.sourceforge.net>]

On Mon, 2006-04-10 at 10:51 +0200, Tom Primožič wrote:
> I would like to pose one really perverse question (perverse because it
> mentions overloading). 
> 
> I have done a lot of thinking over the subject of type inference with
> overloading. I have also read a lot, however, no paper satisfied me. I
> don't like constraints (neither GCaml nor System CT like) as i find
> them too difficult for the user to understand. 

I couldn't understand the constraints of CT either. 

I think (if I understand correctly) that GCaml is simple.
A generic function is called 'as if it were polymorphic'.
Which implementation is used is calculated independently.
Thus there is no impact on the existing type inference
engine for calls to generics, there are new rules for
choosing the implementation based on the construction
of the generic function.

I suggest you look at the rules the new version of C# uses,
it can do both overloading and argument type inference,
with some constraints (I don't understand them either :)

> I have been trying to think of another mechanism for inferring
> overloaded types, but have yet been unsuccessful. 

Generalised Unification. Keep a set of sets of equations.
Each application leads to a set of alternatives.

For each alternative, duplicate the sets of equations,
then add that alternative to each set. Now unify as much
as possible, go on to the next set.

This is VERY expensive. A cut occurs when a function
'goes out of scope'. At the point, the type of the function
must be established (that is, for each argument's type variable,
the same assignment must exist in all the sets). If not,
the program is ambiguous.

BTW: just a pie in the sky :)

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net