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

TypeScript поймал 38% ошибок в крупных JavaScript codebases ещё до запуска - просто добавив статические типы. Вывод типов при этом позволяет писать код без аннотаций на каждой строке. Как компилятор угадывает типы - и почему иногда ошибается в самых неожиданных местах?

• **Rust borrow checker** полностью строится поверх type system: lifetime-параметры - это типовые переменные, а проверка заимствований - специализированный type checking. Без sound type system borrow checker был бы невозможен.
• **TypeScript compiler** при проверке `checker.ts` (50k строк) тратит 2-3 секунды на type checking в cold state. Incremental compilation через language server кеширует типы и сокращает время до ~50ms для типичного файла.
• **GHC** компилирует код с доказательствами корректности типов - phantom types, GADTs, dependent types позволяют кодировать инварианты программы прямо в системе типов, превращая компилятор в theorem prover.

Type Checking

Type checking - проверка того, что операции применяются к операндам совместимых типов. Статический type checker делает это во время компиляции; динамический (Python, JavaScript) - в runtime. Статическая проверка позволяет поймать целый класс ошибок до запуска программы.

Clang реализует type checking в `SemaExpr.cpp` - около 14000 строк кода, обрабатывающих все комбинации выражений. При `a + b` проверяется: оба ли операнда арифметического типа, нужно ли неявное преобразование. Rust делает type checking в `rustc_typeck` - отдельном crate объёмом около 80 тысяч строк. TypeScript checker (`checker.ts`) - 50 тысяч строк и является одним из крупнейших TypeScript-файлов в мире.

Rust использует trait bounds для полиморфного type checking: `fn max<T: Ord>(a: T, b: T) -> T` - компилятор при каждом вызове проверяет, реализует ли конкретный тип `T` трейт `Ord`. Monomorphization затем генерирует отдельный код для каждого конкретного `T` - нулевая стоимость абстракции в runtime при полном контроле типов.

Type Inference

Type inference - автоматический вывод типов без явных аннотаций. Компилятор собирает ограничения из контекста использования и решает систему уравнений над типами. Результат: язык выглядит как динамический, а безопасность - как у статического.

Локальный вывод (local inference) как в Java с `var` или C++ с `auto` смотрит только на правую часть присваивания. Глобальный вывод (Hindley-Milner) может распространять информацию о типах через всю программу. Rust использует нечто среднее: вывод внутри функции - глобальный, между функциями - только через явные сигнатуры.

Scala 3 (Dotty) использует алгоритм вывода типов на основе Local Type Inference - более предсказуемый, чем полный HM, но требующий аннотаций на параметрах функций. Это сознательный trade-off: сложность сообщений об ошибках вывода пропорциональна глобальности алгоритма - чем шире вывод, тем непонятнее ошибки.

Unification

Унификация - алгоритм решения уравнений над типами вида `T1 = T2`. При встрече выражения `x + y` компилятор порождает ограничения `type(x) = int`, `type(y) = int`, `type(x + y) = int` и решает их унификацией. Если решение существует - типы корректны, если нет - ошибка типов.

Rustc хранит ограничения в `InferCtxt` (inference context) и решает их через `eq_types()`. Если тип не может быть выведен - `error[E0282]: type annotations needed`. GHC строит граф ограничений и использует алгоритм Пейтон Джонса-Шейфера для вывода с type classes. Сложность унификации - линейная при использовании Union-Find (алгоритм Тарьяна).

Occurs check - проверка перед присваиванием `alpha := T`: нужно убедиться, что `alpha` не входит в `T`. Без неё `alpha = List alpha` создаёт бесконечный тип. Haskell по умолчанию occurs check пропускает для эффективности, что позволяет бесконечные типы и иногда даёт странные ошибки компиляции.

Hindley-Milner

Hindley-Milner (HM) - система вывода типов с параметрическим полиморфизмом. Главная особенность: функции могут быть полиморфными без явных аннотаций. `id x = x` автоматически получает тип `forall a. a -> a` - работает для любого типа `a`.

OCaml, SML, Haskell, F# используют HM как основу. Rust намеренно отказался от полного HM между функциями - для улучшения сообщений об ошибках и предсказуемости. TypeScript использует bidirectional checking - более гибкий, но менее полный алгоритм. Полный HM иногда даёт совершенно непонятные ошибки: ошибка в строке 200 проявляется в строке 5, потому что ограничения распространяются глобально.

Ключевые идеи

• **Type checking** проверяет совместимость типов операндов и операций. Structural typing (TypeScript) vs nominal typing (Java) - принципиально разные модели совместимости.
• **Type inference** решает систему ограничений над типами. Local inference (C++ `auto`) смотрит на правую часть; глобальный HM распространяет информацию через всю функцию.
• **Унификация** - алгоритм решения уравнений `T1 = T2`. Структурная, рекурсивная, симметричная. Occurs check предотвращает бесконечные типы.
• **Hindley-Milner** обеспечивает полиморфизм без аннотаций через let-полиморфизм. Rust сознательно ограничил HM до функциональных границ для лучших сообщений об ошибках.

Связанные темы

Type checking - центральная фаза семантического анализа, связанная со многими аспектами компилятора:

• Таблица символов — Type checker читает типы из таблицы символов, построенной в фазе name resolution
• Семантические ошибки — Type mismatch - самый частый класс семантических ошибок, обнаруживаемых в этой фазе
• Семантические проходы — После type checking annotated AST передаётся в lowering и desugaring

Вопросы для размышления

• TypeScript иногда выводит `any` вместо конкретного типа - что это говорит об ограничениях алгоритма вывода при работе с динамическими паттернами JavaScript?
• Почему Rust запрещает rank-2 полиморфизм по умолчанию - и что именно пришлось бы добавить в систему типов, чтобы `|id: impl Fn| (id(true), id(42))` заработало?
• Как система типов Haskell с type classes принципиально отличается от Java generics с wildcards - и какие программы можно выразить в одной системе, но не в другой?

Связанные уроки

• plt-02-type-systems
• plt-04-type-inference
• plt-12-subtyping