4

当存在重载函数时，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 案例，它看起来像一个方程式树，听起来很吓人。

这种算法是否有任何形式化？

4

1 回答 1

2

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

Num a => a -> a -> a

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

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

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

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

于 2019-04-22T16:28:22.070 回答