Типовые переменные и унификация

Сердце вывода типов: как из уравнения «этот тип = тот тип» получить значения неизвестных.

Унификация — поиск подстановки типовых переменных, при которой два типовых выражения становятся синтаксически равными.

Постановка задачи

Во время вывода мы накапливаем уравнения вида «тип A должен равняться типу B», где в типах встречаются неизвестные — типовые переменные a, b, c. Решить уравнение значит найти, чем заменить переменные, чтобы стороны совпали. Например, из a -> b = Int -> c следует a = Int и b = c. Эта подстановка и есть результат.

унифицировать (a -> b)  с  (Int -> c)
  => сопоставить аргументы:  a = Int
  => сопоставить результаты: b = c
решение: { a := Int, b := c }

Правила унификации

Алгоритм рекурсивен и разбирает четыре случая.

• Переменная против чего угодно: a с T — связываем a := T (если a ещё свободна).
• Одинаковые конструкторы: A1 -> B1 с A2 -> B2 — унифицируем A1 с A2, затем B1 с B2.
• Разные конструкторы: Int с Bool или Int со стрелкой — ошибка («не совпадают»).
• Occurs-check: связать a с типом, где a уже встречается (a = a -> b), нельзя — это бесконечный тип. Именно этот случай отвергает самоприменение x x.

Демонстрация: рабочая унификация

Реализуем унификацию с подстановкой и occurs-check. Типы: переменная ("v", имя) или конструктор ("c", имя, аргументы); стрелка — конструктор "->" с двумя аргументами.

def TV(n):      return ("v", n)
def TC(n, *a):  return ("c", n, tuple(a))
def arrow(a, b):return TC("->", a, b)

def show(t):
    if t[0]=="v": return t[1]
    if t[1]=="->":
        l=show(t[2][0])
        if t[2][0][1]=="->" if t[2][0][0]=="c" else False: l="("+l+")"
        return l+" -> "+show(t[2][1])
    if t[2]: return t[1]+" "+" ".join(show(x) for x in t[2])
    return t[1]

def walk(t, s):
    while t[0]=="v" and t[1] in s:
        t = s[t[1]]
    return t

def occurs(v, t, s):
    t = walk(t, s)
    if t[0]=="v": return t[1]==v
    return any(occurs(v, a, s) for a in t[2])

def unify(a, b, s):
    a = walk(a, s); b = walk(b, s)
    if a[0]=="v" and b[0]=="v" and a[1]==b[1]:
        return s
    if a[0]=="v":
        if occurs(a[1], b, s):
            raise TypeError("бесконечный тип: " + a[1] + " в " + show(b))
        ns = dict(s); ns[a[1]] = b; return ns
    if b[0]=="v":
        return unify(b, a, s)
    if a[1]!=b[1] or len(a[2])!=len(b[2]):
        raise TypeError("не совпадают: " + show(a) + " и " + show(b))
    for x, y in zip(a[2], b[2]):
        s = unify(x, y, s)
    return s

def resolve(t, s):
    t = walk(t, s)
    if t[0]=="v": return t
    return TC(t[1], *[resolve(a, s) for a in t[2]])

s = unify(arrow(TV("a"), TV("b")), arrow(TC("Int"), TV("c")), {})
print("a =", show(resolve(TV("a"), s)))
print("b =", show(resolve(TV("b"), s)))
try:
    unify(TV("a"), arrow(TV("a"), TV("b")), {})
except TypeError as e:
    print("occurs:", e)
try:
    unify(TC("Int"), TC("Bool"), {})
except TypeError as e:
    print("clash :", e)

Вывод:

a = Int
b = c
occurs: бесконечный тип: a в a -> b
clash : не совпадают: Int и Bool

Три исхода — успех с подстановкой, ошибка occurs-check, конфликт конструкторов — это ровно три вердикта, которые выдаёт вывод типов в Haskell/OCaml под капотом.

Как работает под капотом

Подстановка s — это «текущие знания» о переменных. Функция walk следует по цепочке связываний, отвечая «чему сейчас равна переменная». Алгоритм Робинсона (1965), который мы реализовали, всегда находит наиболее общий унификатор (most general unifier): любое другое решение получается из него дальнейшей подстановкой. Именно поэтому вывод даёт самый общий (принципиальный) тип.

Частые ошибки

• Забыть occurs-check. Без него унификация a = a -> b зациклится или построит бесконечный тип — классический баг.
• Не применять подстановку транзитивно. Если a := b, а позже b := Int, то a тоже Int; walk обязан проходить цепочку.
• Считать унификацию симметричной по конструкторам. Связывание идёт только «переменная := тип»; два разных конструктора не унифицируются никогда.

Итоги

• Унификация решает уравнения между типами, находя подстановку переменных.
• Случаи: переменная (связать), одинаковые конструкторы (рекурсия), разные (ошибка), occurs (бесконечный тип).
• Occurs-check отвергает самоприменение и бесконечные типы.
• Алгоритм Робинсона даёт наиболее общий унификатор — основу принципиальных типов.