重载函数的 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 推断非常方便，但它会对您的类型系统造成限制。您必须决定这些限制是否值得权衡。

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

Hindley-Milner type inference for overloaded functions

functional-programming

compilation

type-inference

hindley-milner