Проверка против вывода типов

Две задачи, которые часто путают: «проверить заданный тип» и «найти тип, которого никто не написал».

Проверка типов (type checking) отвечает «верна ли аннотация?»; вывод типов (type inference) отвечает «какой тип у выражения без аннотаций?».

Три родственные задачи

Вокруг типов крутятся три разные задачи, и их полезно чётко различать.

В STLC мы делали именно проверку: лямбды несли явные аннотации \x:Int. e, и чекер их использовал. Это просто, но многословно — программист пишет типы везде. Языки ML, Haskell, OCaml, Rust (локально) идут дальше: они выводят типы, так что аннотации почти не нужны.

Почему вывод труднее проверки

При проверке тип параметра известен — мы просто сверяемся. При выводе тип параметра неизвестен заранее; его надо вычислить из того, как параметр используется в теле. Для функции \x. x + 1 мы должны догадаться, что x : Int, потому что к нему применили + 1. Это требует механизма: ввести неизвестную (типовую переменную), собрать ограничения из использований и решить их. Этот механизм — унификация, которой посвящён весь раздел.

Демонстрация: проверка тривиальна, вывод требует догадки

Покажем контраст. Проверка: дан тип — сверяем. Вывод: типа нет — собираем ограничение из использования + и заключаем Int.

# ПРОВЕРКА: тип параметра дан, просто сверяем употребление
def check_lambda(param_type, uses_plus):
    if uses_plus and param_type != "Int":
        return "ошибка: + требует Int, а параметр " + param_type
    return "ок: " + param_type

print("check (x:Int, x+1):", check_lambda("Int", True))
print("check (x:Bool,x+1):", check_lambda("Bool", True))

# ВЫВОД: типа нет, выводим из использования
def infer_lambda(uses_plus):
    t = "?"                       # неизвестная (типовая переменная)
    if uses_plus:
        t = "Int"                 # ограничение: + ⇒ Int
    return t

print("infer (x. x+1)    :", infer_lambda(True))
print("infer (x. x)      :", infer_lambda(False))

Вывод:

check (x:Int, x+1): ок: Int
check (x:Bool,x+1): ошибка: + требует Int, а параметр Bool
infer (x. x+1)    : Int
infer (x. x)      : ?

Заметьте последнюю строку: для \x. x без использований тип параметра остаётся неизвестным — это «любой тип», что приведёт нас к полиморфизму. Вывод естественно порождает общие типы.

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

Алгоритм вывода Хиндли — Милнера работает в три такта: (1) обойти терм, назначая каждому подвыражению свежую типовую переменную; (2) из каждого правила породить уравнение между типами (например, «тип функции = тип аргумента -> тип результата»); (3) решить систему уравнений унификацией. Решение — подстановка типовых переменных, дающая искомые типы. Проверка же пропускает шаги 1–2: типы уже написаны, остаётся сверить.

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

• Считать вывод и проверку одним и тем же. Проверка локальна и проста; вывод глобально решает систему ограничений.
• Думать, что вывод всегда возможен. Для STLC/ML — да и эффективно; для System F (полный) — неразрешимо (см. раздел 8).
• Ожидать, что вывод даст самый конкретный тип. Наоборот, он даёт самый общий (principal type), а конкретику добавляет использование.

Итоги

• Проверка сверяет данный тип; вывод находит тип сам; реконструкция заполняет дыры.
• Вывод труднее: тип параметра вычисляется из использований через ограничения.
• Алгоритм: свежие переменные → уравнения → унификация.
• Вывод даёт самый общий тип; отсутствие ограничений ведёт к полиморфизму.