Вывод типа Хиндли-Милнера для перегруженных функций - PullRequest
Новая
       82

Вывод типа Хиндли-Милнера для перегруженных функций

3 голосов
/ 21 апреля 2019

Как работает алгоритм Хиндли-Милнера, когда есть перегруженные функции?

В простой форме (без перегрузок) выглядит чисто: 

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, и это похоже на дерево уравнений, которое звучит страшно.

Есть ли формализация таких алгоритмов?

1 Ответ

2 голосов
/ 22 апреля 2019

Вы, вероятно, хотите исследовать классы типов . В Haskell + имеет тип: 

Num a => a -> a -> a

По сути, когда вы сталкиваетесь с + во время вывода типа, все, что вы можете сделать вывод, это то, что два ваших операнда имеют один и тот же тип и результат, а тип имеет ограничение Num. Другие выражения могут позволить вам определить более конкретный тип, но вам может не нужен более конкретный тип.

Ваш (any, any): string - это то, что действительно нарушает ваш вывод, потому что он почти не создает ограничений для ваших типов. Чтобы включить этот сценарий, вы можете создать +, который выглядит следующим образом: 

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

Тем не менее, объединить это с вышеупомянутым Num и ожидать получить полезный результат было бы чрезвычайно сложно. Вы должны действительно разделить их на два разных оператора. Вывод HM очень удобен, но он создает ограничения для вашей системы типов. Вы должны решить, стоят ли эти ограничения компромисса.

...