Search code examples
functional-programmingcompilationtype-inferencehindley-milner

Hindley-Milner type inference for overloaded functions

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?

Solution

  • 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.