Let-полиморфизм и обобщение

Почему let id = ... позволяет применять id к разным типам, а аргумент функции — нет.

Обобщение (generalization) — превращение типа со свободными переменными в полиморфную схему forall a. ..., которую можно специализировать под каждое использование.

Проблема

Алгоритм W из прошлого урока выводит id : t4 для \x.x. Но если связать let id = \x. x и использовать его дважды — на числе и на строке, — наивный вывод свяжет t4 с первым же использованием (скажем, Int) и отвергнет второе (String). Одна переменная не может быть и Int, и String. Нужно сделать id по-настоящему полиморфным.

Решение Милнера: обобщать на let

Идея ML: при let-привязке вывести тип правой части, затем обобщить его свободные переменные в схему forall a. a -> a. При каждом использовании схему инстанцируют — подставляют свежие переменные. Тогда первое использование возьмёт a := Int, второе — a := String, и они не конфликтуют, потому что переменные разные.

let id = \x. x          -- вывод: id : t -> t
                        -- обобщение: id : forall a. a -> a
in id 5                  -- инстанс: a := Int   => id : Int -> Int
   id "hi"               -- инстанс: a := String=> id : String -> String

Ключевая тонкость: обобщают только переменные, которые не связаны в окружении (не «торчат» из внешнего контекста). Поэтому параметр лямбды НЕ полиморфен внутри своего тела — он фиксирован, пока функция не применена. Это различие «let-полиморфизм есть, lambda-полиморфизма нет» — суть системы Хиндли — Милнера.

Демонстрация: инстанцирование схемы

Смоделируем схему forall [a]. body и операцию инстанцирования — замену квантифицированных переменных свежими. Увидим, как два использования получают независимые типы.

_k = [0]
def fresh():
    _k[0]+=1; return "t"+str(_k[0])

# схема: (список квантифицированных имён, тип как строка с этими именами)
scheme = (["a"], "a -> a")

def instantiate(sch):
    quantified, body = sch
    mapping = {q: fresh() for q in quantified}
    out = body
    for q, fr in mapping.items():
        out = out.replace(q, fr)
    return out

print("схема id     :", "forall " + " ".join(scheme[0]) + ". " + scheme[1])
print("использ. #1  :", instantiate(scheme), "   (затем a := Int)")
print("использ. #2  :", instantiate(scheme), "   (затем a := String)")
print("две разные переменные => конфликта Int/String нет")

Вывод:

схема id     : forall a. a -> a
использ. #1  : t1 -> t1    (затем a := Int)
использ. #2  : t2 -> t2    (затем a := String)
две разные переменные => конфликта Int/String нет

Каждое использование берёт свежие t1, t2 — поэтому одно может стать Int, другое String. Это и есть механизм, благодаря которому Haskell и OCaml позволяют переиспользовать полиморфные значения свободно.

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

Обобщение формально: generalize(Γ, τ) квантифицирует те свободные переменные τ, которых нет в свободных переменных контекста Γ. Инстанцирование instantiate(σ) заменяет квантифицированные переменные свежими. Ограничение «только на let» сохраняет разрешимость и принципиальность: полный лямбда-полиморфизм — это System F, чей вывод уже неразрешим (раздел 8).

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

Обобщать переменные, торчащие из контекста. Обобщать можно только локально-свободные; иначе вывод станет неверным.
Ждать полиморфизма от параметра лямбды. В ML параметр мономорфен в своём теле; полиморфен только let-связанный идентификатор.
Не инстанцировать при использовании. Без свежих переменных на каждом использовании полиморфизм «схлопнется» в первый встреченный тип.

Итоги

Let-полиморфизм обобщает тип правой части в схему forall a. ....
Каждое использование инстанцирует схему свежими переменными — конфликтов нет.
Обобщают только переменные, не связанные внешним контекстом.
Параметр лямбды мономорфен; полный лямбда-полиморфизм — это уже System F.