How does the Hindley-Milner algorithm work when there are overloaded functions?
In a simple form (without overloads) it looks clean:
y = arr[x1] //it's Generic. x1: int, arr: T[], y:T
z = y+1// z:int, y:int => T:int, arr: int[]. Oh. All types are solved
but I have not found any explanation of how it works with overloaded functions.
For example: I have 4 overloads of '+' function:
+(int, int):int
+(int64, int64):int64
+(double, double):double
+(any,any):string
example:
y = x1+ x2 //x1 and x2 can be int32, int64, real, or objects for string concat
z = x1<<2 //oh! it seems x1 is int!
m = not x2 //omg, x2 is bool. That means that y = 2 + true = '2true' i.e. Ty:string
or complex case:
//functions:
myfun(x,y) = x<<y //(int,int)->int
myfun(x,y) = "some: " + y.toLower() + not x //(bool,string)-> string
//body:
y1 = myfun(x1,x2) //or (int,int)->int or (bool,string)-> string
y2 = myfun(x3,y1) //or (int,int)->int or (bool,string)-> string
y3 = if (x3) 1 else 0 //x3: bool, y3: string
//x3:bool => y2:string, y1:string
//y1:string=> x1:bool, x2:string
The trouble is that I have to keep in mind all these cases:
y1 cases:
int if x1: int and x2:int
string if x1: bool and x2:string
y2 cases:
int if x3: int and y1:int
string if x3: bool and y1:string
and y2 cases reference y1 cases, and it seems like an equation tree, that sounds scary.
Is there any formalization of such algorithms?
You probably want to research type classes. In Haskell, + has a type of:
Num a => a -> a -> a
Essentially, when you come across + during type inference, all you can infer is that your two operands are the same type as each other and the result, and that the type has a Num constraint. Other expressions may allow you to determine a more concrete type, but you may not need a more concrete type.
Your (any, any): string is what really breaks your inference, because it creates almost no restrictions on your types. To enable that scenario, you can create a + that looks like:
(Show a, Show b) => a -> b -> String
However, combining this one with the above Num one and expecting to get a useful result would be extremely difficult. You should really split these into two different operators. HM inference is very handy, but it creates restrictions on your type system. You have to decide if those restrictions are worth the trade off.