Алгоритм W: вывод как в Haskell и OCaml

Соединяем всё: обход терма порождает ограничения, унификация их решает — и типы выводятся сами.

Алгоритм W (Хиндли — Милнера) — процедура вывода типов: рекурсивно по терму строит тип и подстановку, используя унификацию для согласования.

Идея алгоритма

Алгоритм W обходит дерево терма и для каждого узла делает ровно то, что диктует правило вывода — но с неизвестными типами вместо заданных.

• Переменная: взять её тип из контекста.
• Абстракция \x. e: придумать свежую переменную a для типа x, вывести тип тела e как B в расширенном контексте, вернуть a -> B.
• Аппликация f e: вывести тип f как tf, тип e как te, придумать свежую r для результата и унифицировать tf с te -> r; ответ — r.

Унификация в аппликации — ключевой момент: именно она «прижимает» тип параметра к типу аргумента, распространяя информацию по дереву.

Демонстрация: мини-движок вывода

Соберём вывод поверх унификации из прошлого урока. Выведем тип \f. \x. f x — это (a -> b) -> a -> b, классический «оператор применения».

# --- унификация (как в прошлом уроке) ---
def TV(n):      return ("v", n)
def TC(n, *a):  return ("c", n, tuple(a))
def arrow(a, b):return TC("->", a, b)
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("бесконечный тип")
        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("конфликт типов")
    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]])
def show(t):
    if t[0]=="v": return t[1]
    if t[1]=="->":
        l=show(t[2][0])
        if t[2][0][0]=="c" and t[2][0][1]=="->": l="("+l+")"
        return l+" -> "+show(t[2][1])
    return t[1]

# --- алгоритм W ---
_k=[0]
def fresh():
    _k[0]+=1; return TV("t"+str(_k[0]))
def var(n): return ("var", n)
def lam(p,b): return ("lam", p, b)
def app(f,a): return ("app", f, a)

def infer(e, env, s):
    if e[0]=="var":
        return env[e[1]], s
    if e[0]=="lam":
        a = fresh()
        ne = dict(env); ne[e[1]] = a
        bt, s = infer(e[2], ne, s)
        return arrow(a, bt), s
    if e[0]=="app":
        tf, s = infer(e[1], env, s)
        te, s = infer(e[2], env, s)
        r = fresh()
        s = unify(tf, arrow(te, r), s)
        return r, s

# \f. \x. f x
term = lam("f", lam("x", app(var("f"), var("x"))))
t, s = infer(term, {}, {})
print("тип \\f.\\x. f x  :", show(resolve(t, s)))

# \x. x  -- тождество
t2, s2 = infer(lam("x", var("x")), {}, {})
print("тип \\x. x        :", show(resolve(t2, s2)))

Вывод:

тип \f.\x. f x  : (t2 -> t3) -> t2 -> t3
тип \x. x        : t4 -> t4

Вывелось (t2 -> t3) -> t2 -> t3 — то есть (a -> b) -> a -> b с точностью до имён переменных. А тождество получило t4 -> t4, где t4 свободна (любой тип) — это и есть полиморфизм, к которому мы перейдём.

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

Имена переменных t2, t3 — внутренние свежие имена; реальный компилятор перед показом «причёсывает» их в a, b, c. Накопленная подстановка s несётся через весь обход — это «состояние знаний», которое унификация в аппликациях постепенно уточняет. Алгоритм линеен по числу узлов (с поправкой на стоимость унификации) и потому практичен для реальных компиляторов.

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

• Не протаскивать подстановку. Каждый рекурсивный вызов возвращает обновлённую s; потеряете её — потеряете выведенную информацию.
• Брать одну переменную на все употребления полиморфной функции. Без обобщения (let-полиморфизм) let id = \x.x in (id 1, id true) не пройдёт; об обобщении — в следующем уроке.
• Забывать свежесть переменных. Каждая абстракция/результат требует новой переменной, иначе типы ошибочно «слипнутся».

Итоги

• Алгоритм W обходит терм, порождая свежие переменные и уравнения, и решает их унификацией.
• Унификация в аппликации связывает тип параметра с типом аргумента.
• Подстановка протаскивается через весь обход как «состояние знаний».
• Результат — принципиальный тип; свободные переменные означают полиморфизм.