用于重载函数的Hindley-Milner类型推断

Question

当有重载函数时，Hindley-Milner算法如何工作？

它以简单的形式（没有重载）看起来很干净：

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

但是我没有找到任何关于它如何与重载函数一起工作的解释。

例如：我有4个'+'函数重载：

+(int, int):int
+(int64, int64):int64
+(double, double):double
+(any,any):string

例：

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

或复杂的情况：

//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

麻烦的是我必须记住所有这些情况：

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

和y2个案例参考y1个案例，它看起来像一个方程式树，听起来很吓人。

这种算法有没有形式化？

Answer 1

您可能想要研究类型类。在Haskell中，+有一种类型：

Num a => a -> a -> a

基本上，当您在类型推断期间遇到+时，您可以推断出的是，您的两个操作数是彼此相同的类型和结果，并且该类型具有Num约束。其他表达式可能允许您确定更具体的类型，但您可能不需要更具体的类型。

你的(any, any): string真正打破了你的推理，因为它对你的类型几乎没有任何限制。要启用该方案，您可以创建一个如下所示的+：

(Show a, Show b) => a -> b -> String

然而，将这一个与上面的Num相结合并期望获得有用的结果将是非常困难的。你应该把它们分成两个不同的运算符。 HM推理非常方便，但它会对您的类型系统造成限制。你必须决定这些限制是否值得权衡。