Типы

То что ты хочешь сделать по уму называется унификацией термов (term unification). Погугли на этот счет или посмотри как это сделано в прологе. Хотя в прологе унификация достаточно обрезанная, но в целом идея должна быть понятна.

>Типы считаются эквивалентными, если один тип можно получить из другого путём переобозначения type variables, и наоборот.

Например пройти выражение слева на право нумеруя переменные. Первая встреченная v1, зетем v2, если переменная пронумерованна, то заменяем на уже присвоенный номер. После этого эквивалентность превращается в равенство.

На языке унификации - типы эквивалентны, если унифицирующая подстановка переименовывает переменные не склеивая их.

>Как проще всего проверить приводимость типов? Тип a считаются приводимым к типу b, если экземпляр типа a является экземпляром типа b. Например, типы (a -> b -> a), (a -> Int), (a -> a), ((a -> b) -> (b -> a)) приводим к типу (a -> b).

Другими словами выражение a приводим к b, если тип, к которому они приводятся унификацией эквивалентен а.

Унификация вещь не сложная. Для двух выражений E1 E2 может получится так, что существуют некоторые подстановки s1 s2, которые приводя их к одинаковому E3. Оказывается, что если существует хотя бы одна пара, по среди их всех есть универсальные u1, u2, E0, такие что E1[u1] = E0 E2[u2] = E0, и для любых s1 s2, таких что E1[s1] = E3 и E2[s2] = E3 существует подстановка s, такая что E0[s] = E3.

Запись E[s] - результат применения подстановки s к E.

Доказывается несложно, индукцией по построению термов. Если оба терма переменные, u1, u2 - заменяет их на одну и туже. Если один терм вида E1 = (F t1 t2 t3 .. ), а другой E2=v переменная, то, если E1 содержит свободное вхождение v, то унификатора не существует, если нет, то u2 заменяет v на E1. И наконец если они оба имею вид (F1 t1 t2 t3...) (F2 t1 t2 t3...), то Если F1 != F2, то унификатора не существует, если F1=F2, то унифицируем все по порядку.

Ну и конечно a->b это сокращенно (-> a b)

Алгоритм Хиндли-Милнера?

> Алгоритм Хиндли-Милнера?

ребята, я хоть и не знаю алгоритм Хиндли-Милнера, но задача топикстартера в его постановке настолько тривиальна, что это даже язык не повернется назвать алгоритмом, да еще и с несколькими именами.

Спасибо, Вы очень понятно объяснили.