Системы типов: что доказывает компилятор

Проект ЦИТадель

Завершающая статья цикла посвящена механизму, который уже встречался в предыдущих материалах: владение Rust проверяется системой типов, а Result и Option являются типами-суммами. Основные вопросы здесь таковы: какое свойство проверяет конкретная система типов, на какую часть программы распространяется её гарантия и какие программы она не умеет выразить. Типы дают дешёвую автоматическую проверку важных классов утверждений, но сила результата зависит от языка, настроек и используемых обходных механизмов.

Раздел 1 объясняет границы статической гарантии. Раздел 2 сравнивает время проверки, раздел 3 — вывод типов, раздел 4 — номинативную и структурную совместимость. Раздел 5 вводит произведения, суммы и обобщённые типы, раздел 6 — постепенную типизацию. В разделах 7–8 рассматриваются ограничения и практические упражнения.

1. Что устанавливает проверка типов

Практически тип можно рассматривать как классификацию значений вместе с разрешёнными операциями. Статическая проверка устанавливает, что программа согласуется с правилами этой классификации до запуска. Если система корректна относительно типов (англ. sound), из успешной проверки следует отсутствие определённого класса ошибок во всех исполнениях, охваченных её моделью.

Эта оговорка существенна. Многие промышленные языки допускают небезопасные приведения, рефлексию, внешние функции или специальный тип вроде any. TypeScript прямо не ставит полную корректность относительно типов (soundness) своей целью. Данные из сети и файлов также не становятся корректными только из-за аннотации. Поэтому типовая гарантия действует в пределах конкретной системы и проверенной части программы.

Тест-пример проверяет поведение на конкретном исполнении, а типизатор анализирует все пути в своей абстрактной модели; тест вовсе не является логическим утверждением «существует правильный вход». Сильные статические системы обычно консервативны: ради запрета всех программ с определённой ошибкой они могут отвергнуть безопасный код, который анализ не способен обосновать. Это дополняет, а не заменяет лестницу проверок из статьи «Тестирование сегодня».

2. Ось «когда»: до запуска или во время

Динамический язык не лишён типов: значения имеют типы, а допустимость многих операций проверяется во время исполнения. Ошибка проявляется только на выполненном пути — в тесте, при разработке или в эксплуатации. Статическая проверка переносит часть диагностики до запуска, но может требовать аннотаций и ограничивать приёмы, которые анализатор не понимает. Вывод типов уменьшает число явных аннотаций, а постепенная типизация позволяет проверять программу частями. Поэтому полезнее спрашивать не «статика или динамика вообще», а какие свойства требуется проверять до запуска и на каких границах.

3. Вывод типов и явные аннотации

Вывод типов восстанавливает часть информации из выражений и мест использования. Сложность вывода различается: система Хиндли — Милнера может находить наиболее общий тип без многих аннотаций, тогда как Java, C#, Rust, TypeScript и проверщики Python используют собственные варианты локального и контекстного вывода с ограничениями.

Аннотация публичной границы полезна не только читателю. Она фиксирует обещание модуля и может заставить проверщик отвергнуть реализацию или вызов, которые иначе получили бы более широкий выведенный тип. Поэтому практическое правило следует формулировать мягко: использовать вывод для очевидных локальных выражений, а важные границы записывать явно в тех языках, где это улучшает стабильность контракта.

4. Ось «что»: имя против формы

При номинативной совместимости важны объявленное имя и отношение между декларациями. Момент времени и длительность могут оставаться разными типами, даже если оба представлены числом. При структурной совместимости достаточно требуемого набора полей и методов. Интерфейсы Go удовлетворяются неявно по набору методов, а TypeScript в основном сравнивает структуру.

Реальные языки часто сочетают элементы обоих подходов, но не одинаковым способом. В TypeScript приватные и защищённые поля вводят номинативные ограничения, а для предметных единиц применяют брендированные типы. В номинативном языке объявленный интерфейс обычно всё равно требует явного отношения реализации и потому не становится полностью структурным. Выбор зависит от того, нужно ли охранять смысл сущности или способность выполнять операции.

5. Словарь утверждений: произведения, суммы, дженерики

Богатство системы типов — в том, какие утверждения на ней можно записать. Три конструкции образуют ядро современного словаря.

Произведение — «и то, и это»: структура, запись, кортеж. Утверждение скромное: все поля присутствуют. Эта давно известная конструкция остаётся основой современных моделей данных.

Сумма — «либо один вариант, либо другой»: Result из статьи об обработке ошибок, Option вместо неявного отсутствия, состояние «загрузка | успех | ошибка». Размеченная сумма позволяет связать с каждым вариантом только подходящие ему данные. Исчерпывающий разбор в языках, которые его проверяют, сообщает о местах, не обработавших новый вариант. Так можно сделать многие бессмысленные сочетания полей непредставимыми, хотя внешние данные всё равно требуют валидации.

Дженерики параметризуют код типом. Параметричность действительно ограничивает реализацию, но выводы зависят от языка и допущений. Полностью полиморфная чистая завершающаяся функция T → T должна вернуть входное значение; если разрешены исключения, бесконечный цикл, небезопасные приведения или наблюдение типа во время исполнения, вариантов больше. Сигнатура Array<T> → T к тому же не может дать значение для пустого массива без частичной операции; корректнее использовать непустую коллекцию или вернуть Option<T>. Ограничения на T явно добавляют доступные операции.

6. Постепенная статическая проверка

TypeScript поверх JavaScript и аннотации с внешними проверщиками в Python позволяют внедрять статическую проверку постепенно. Типизированный и нетипизированный код сосуществуют, а any или аналогичная постепенная форма ослабляет анализ на выбранной границе. Более безопасный unknown в TypeScript, напротив, требует уточнить значение перед использованием.

Механизмы разных языков не тождественны. TypeScript удаляет типы при генерации JavaScript; аннотации Python обычно не обеспечивают проверку во время исполнения; PHP может проверять часть объявленных типов динамически. Поэтому нужно отдельно установить, что делает статический инструмент и что проверяет среда. В любом случае данные из сети, файла или нетипизированного модуля следует валидировать. Подробности TypeScript рассмотрены в статье «Современный JavaScript и TypeScript».

7. Пределы и практическая ценность

Зависимые и уточняющие типы способны выражать длины, диапазоны и предметные инварианты. Чем сильнее утверждение, тем чаще требуются явные доказательства, аннотации или помощь решателя; при этом некоторые системы умеют выводить и такие свойства частично. Универсального «правильного уровня» нет: тип должен окупать сложность снижением риска, улучшением интерфейса или поддержкой изменений.

Статическая информация особенно полезна в трёх областях:

• Рефакторинг. Изменение сигнатуры или добавление варианта суммы выявляет многие зависящие места, если они находятся в проверяемой части программы и не скрыты динамическими обходами. Тесты при этом по-прежнему нужны для поведения, которое тип не выражает.
• Инструменты. Типы улучшают автодополнение, навигацию и автоматические преобразования. Редакторы динамических языков также используют анализ потока и сведения среды исполнения, поэтому качество инструментов не определяется одной только меткой «статический».
• Генерация кода. Явная сигнатура ограничивает допустимый результат генерации, а быстрая проверка типов становится одним из первых этапов контроля. Как показано в статьях «Разработка с ИИ-ассистентами» и «Тестирование сегодня», это лишь один уровень проверки и не заменяет независимый контракт и тесты поведения.

8. Практикум: статические проверки в песочницах

Задания TypeScript и Rust выполняются в официальных песочницах. Для упражнения с Python понадобится выбранный проверщик типов, потому что сама среда исполнения аннотации обычно не проверяет.

Задание 1. Непредставимые состояния (TypeScript). Смоделируйте экран данных флагами isLoading, hasError, data?, затем размеченной суммой «загрузка | успех | ошибка». Перечислите бессмысленные сочетания первой модели. В default оператора switch присвойте оставшееся значение переменной типа never. Добавьте вариант «пусто» и убедитесь, что именно эта явная проверка исчерпывающего разбора выдаёт ошибку.

Задание 2. Вывод и аннотация (TypeScript). Возьмите локальную функцию без аннотаций и изучите выведенные типы. Затем задайте более узкую публичную сигнатуру и проверьте, изменились ли допустимые реализации и вызовы. Повторите пример с выражением, для которого TypeScript выводит any, и включите noImplicitAny. Не переносите результат на Python: проверщик может считать неаннотированные части динамическими.

Задание 3. Имя против формы (TypeScript). Объявите два несвязанных класса одинаковой формы и убедитесь, что структурная система считает их взаимозаменяемыми. Затем защитите один брендированием (фиктивное поле-метка) и покажите, что подмена стала ошибкой компиляции. Сформулируйте по итогам, когда вам нужна форма, а когда — имя.

Задание 4. Параметричность. Задайте непустую коллекцию типом readonly [T, ...T[]] и функцию first<T>, возвращающую её элемент. Перечислите действия, доступные реализации без приведений и проверки типа во время исполнения. Затем разрешите пустой массив и измените результат на T | undefined. Объясните, какое прежнее утверждение оказалось невозможным.

Задание 5. Постепенность на своём проекте (Python). Включите проверщик типов на одном модуле в мягком режиме и классифицируйте первые сообщения: реальный дефект, неточная аннотация, неизвестный тип зависимости или ограничение анализатора. Затем включите одну более строгую настройку и сравните пользу с количеством необходимой работы, не предполагая заранее, что каждое сообщение обнаруживает ошибку исполнения.

Задание 6*. Исчерпывающий рефакторинг (Rust). Создайте перечисление статусов заказа и несколько функций с исчерпывающим match. Добавьте новый вариант и используйте диагностику компилятора как список мест, где разбор перестал быть полным. Затем перечислите места, которые такой список не найдёт: текстовые протоколы, данные в БД, динамические отображения и бизнес-правила без сопоставления вариантов.

Итоги

• Статическая проверка устанавливает свойства в пределах модели конкретной системы типов; обходные механизмы и непроверенные внешние данные ограничивают гарантию.
• Вывод типов уменьшает число аннотаций, а постепенная типизация позволяет проверять программу частями, но оба механизма различаются между языками.
• Номинативность охраняет объявленную сущность, структурность — наличие требуемых членов; многие языки сочетают отдельные элементы обоих подходов.
• Произведения описывают совместные поля, суммы — взаимоисключающие варианты, дженерики — код, параметризованный типами. Параметрические выводы действуют только при явно названных допущениях.
• Более сильный тип полезен, если его проверяемое утверждение окупает сложность. Типы дополняют тесты поведения и валидацию границ.
• Статическая информация помогает рефакторингу, редактору и контролю сгенерированного кода, но не перечисляет автоматически все смысловые последствия изменения.

Литература

1. B. Pierce, "Types and Programming Languages," MIT Press, 2002 — канонический учебник теории; первые главы доступны любому инженеру.
2. P. Wadler, "Theorems for Free!", 1989 — параметричность и «бесплатные теоремы»; читается как детектив.
3. TypeScript Handbook: Type Compatibility и спецификация системы типов Python — структурная совместимость, пределы статических гарантий и постепенная типизация.
4. Связанные материалы сайта: «Современный JavaScript и TypeScript» и «Тестирование сегодня».
5. Оглавление раздела «Языки и парадигмы программирования»; другие статьи цикла: «Как современные языки управляют памятью», «Конкурентность в современных языках» и «Как современные языки обращаются с ошибками».