Теория языков программирования
Что такое система типов
Хиндли, Милнер и вывод типов
В 1969 году Роджер Хиндли описал алгоритм вывода типов для комбинаторной логики. В 1978 году Робин Милнер независимо разработал ту же систему для языка ML и доказал теорему: 'well-typed programs don't go wrong' - корректно типизированные программы не могут вызвать ошибку типов. Это была первая формальная гарантия soundness. Система Хиндли-Милнера лежит в основе Haskell, OCaml, F#, Elm - и вдохновила TypeScript's inference. За эту и другие работы Милнер получил премию Тьюринга в 1991 году.
Цели урока
- Формулировать тип как множество значений плюс набор операций
- Различать type safety, soundness и completeness
- Объяснять, почему TypeScript unsound и почему это сознательный выбор
- Понимать, почему ни один язык не может быть одновременно sound и complete
TypeScript type system Тьюринг-полна. На ней можно вычислить числа Фибоначчи при компиляции. Это не было задумано - это следствие того, что conditional types + recursive types дают полноту по Тьюрингу. Именно поэтому TypeScript не может гарантировать завершение type checking на всех программах - и Microsoft ограничивает глубину рекурсии принудительно.
- **Ariane 5 (1996)** - integer overflow при касте типа. 370 млн долларов. Современный Rust или Haskell не дали бы скомпилироваться
- **TypeScript** - 10+ млн проектов. Сознательный выбор unsoundness ради совместимости с JavaScript и удобства разработчиков
- **Rust borrow checker** - sound система для memory safety: не компилируется = нет data race в runtime. Mozilla, Google, Microsoft переходят на Rust
- **Haskell в финтехе** (Standard Chartered, Mercury) - sound type system как гарантия корректности финансовых вычислений
- **Agda/Coq** - зависимые типы как formal verification: тип = доказательство теоремы. Верификация криптографических протоколов
Тип = множество + операции
4 июня 1996 года ракета Ariane 5 взорвалась через 37 секунд после старта. Убыток - 370 млн долларов. Причина: **integer overflow** - 64-битное число скорости было преобразовано в 16-битное и не поместилось. Системы типов Ada не предотвратила этот каст. Но не потому что типы бессильны - потому что эта конкретная операция не была запрещена. Современный Rust или Haskell не дали бы скомпилироваться этому коду.
**Тип - это множество допустимых значений и набор операций**, применимых к этим значениям. Не просто слово `int` или `string` в коде - это контракт. Нарушение контракта = ошибка.
| Тип | Множество значений | Операции | Пример |
|---|---|---|---|
| int | ..., -2, -1, 0, 1, 2, ... | +, -, *, /, % | 42 + 8 = 50 |
| bool | true, false | &&, ||, ! | true && false = false |
| string | любые последовательности символов | +, length, slice | "ab" + "cd" = "abcd" |
| float[] | массивы вещественных чисел | push, map, filter, sort | [3.14, 2.71].sort() |
**Ключевая идея:** тип - это не просто метка. Это **контракт**: 'вот что я могу хранить, вот что со мной можно делать'. Нарушение контракта = ошибка. Ariane 5 нарушила контракт типа - и это стоило 370 млн долларов.
Что из перечисленного лучше всего описывает 'тип' в языке программирования?
Type Safety: защита от бессмыслицы
Язык называют **type safe**, если он не позволяет применять операции к значениям неподходящих типов. Степень защиты сильно различается. C позволяет взять указатель на int, привести его к char* и писать в произвольную память - компилятор не скажет ни слова. Rust в аналогичной ситуации откажется компилировать.
| Язык | Type safe? | Null safe? | Проверки | Главная уязвимость |
|---|---|---|---|---|
| C/C++ | Нет | Нет | Минимальные | void*, buffer overflow, UB |
| Python | Да | Нет | Runtime | Ошибки всплывают только при запуске |
| Java | Да | Нет | Compile + Runtime | NullPointerException |
| TypeScript | Да | Частично (strict mode) | Compile | any, type assertions |
| Rust | Да | Да | Compile | unsafe блоки (явный opt-out) |
| Haskell | Да | Да | Compile | Крутая кривая обучения |
**Type safety не равно статической типизации.** Python - type safe (не позволит сложить int + str), но динамически типизирован. C - статически типизирован, но НЕ type safe (void*, произвольные касты).
Чем выше уровень type safety, тем больше ошибок отлавливается **до** того, как код попадёт к пользователю. Разница между проверкой багажа на входе в самолёт и проверкой уже в воздухе.
Статическая типизация = type safety
Статическая типизация означает проверку типов при компиляции, а type safety - невозможность нарушить контракты типов. Это разные свойства.
C - статически типизирован, но не type safe (void*, pointer arithmetic). Python - динамически типизирован, но type safe (TypeError при несовместимых операциях).
Какой язык НЕ является type safe?
Soundness: гарантия без сюрпризов
Код прошёл проверку типов. Компилятор сказал OK. Значит ли это, что в runtime не будет ошибок типов? **Зависит от того, sound ли система типов.** TypeScript говорит OK - и всё равно падает в runtime с `TypeError: Cannot read property 'toUpperCase' of undefined`. Haskell говорит OK - и гарантирует, что этого не случится.
**Sound type system** = если программа прошла проверку типов, то **ошибок типов в runtime гарантированно не будет**. Формулировка Робина Милнера (1978): 'Well-typed programs don't go wrong.'
| Язык | Sound? | Причина unsoundness |
|---|---|---|
| Haskell | Sound | - |
| Rust | Sound* | unsafe блоки - явный opt-out |
| Java | Почти | Generic erasure, null, ковариантные массивы |
| TypeScript | Unsound | any, type assertions, structural typing edge cases |
| C# | Почти | Ковариантные массивы, dynamic |
| Python (mypy) | Unsound | cast(), type: ignore, Any |
**Unsound не значит плохой.** TypeScript сознательно жертвует soundness ради удобства. Позиция команды: 'лучше поймать 95% ошибок удобно, чем 100% мучительно'. Это инженерный tradeoff, а не дефект.
Что означает soundness системы типов?
Completeness: ложные срабатывания
Sound система гарантирует: 'если прошло проверку - ошибок не будет'. А что насчёт обратного? Бывает ли так, что **корректная программа не проходит проверку**? Да. И это не баг - это фундаментальное ограничение математики.
**Complete type system** = все корректные программы проходят проверку типов. Если программа работает правильно, компилятор **обязательно** её примет. На практике **ни одна реальная система типов не является complete**.
**Теорема Райса** (теория вычислений): для любого непростого свойства программ невозможно создать анализатор, который одновременно sound И complete. Это **фундаментальное ограничение**, а не недоработка авторов языков.
Каждый язык делает свой выбор. **Haskell** и **Rust** жертвуют completeness ради гарантий. **TypeScript** жертвует soundness ради совместимости с JavaScript. **Python** максимально complete (нет статической проверки), но soundness обеспечивается только в runtime.
Если язык отклоняет корректный код - значит система типов плохая
Отклонение корректного кода (false positive) - неизбежная цена за soundness. Это осознанный tradeoff.
Ни одна нетривиальная система типов не может быть одновременно sound и complete (теорема Райса). Языки вроде Haskell и Rust выбирают soundness, принимая что иногда придётся 'помогать' компилятору дополнительными аннотациями.
Почему ни один реальный язык не имеет одновременно sound И complete систему типов?
Ключевые идеи
- **Тип** = множество значений + набор допустимых операций. int - числа + арифметика, string - текст + конкатенация
- **Type safety** = язык не позволяет применять операции к несовместимым типам. C - нет, Python/Java/Rust - да
- **Soundness** = если компилятор сказал OK, runtime ошибок типов не будет. Haskell/Rust - sound, TypeScript - нет
- **Completeness** = все корректные программы проходят проверку. Ни один реальный язык не является полностью complete
- **Теорема Райса** делает одновременную soundness и completeness математически невозможной
- TypeScript сознательно жертвует soundness ради удобства - это инженерный tradeoff, не дефект
Связанные темы
Система типов - фундамент, на котором строятся многие другие концепции:
- Статическая vs динамическая типизация — Когда происходит проверка типов - при компиляции или в runtime
- Вывод типов (Type Inference) — Как компилятор определяет типы без явных аннотаций (алгоритм HM)
- Полиморфизм — Как один тип может принимать разные формы - generics, подтипы, ad-hoc
Вопросы для размышления
- Какой tradeoff выбрали бы для нового языка - soundness (как Rust) или удобство (как TypeScript)? Почему?
- Почему TypeScript стал популярнее Haskell, несмотря на то что Haskell имеет более сильную систему типов?
- TypeScript type system Тьюринг-полна - это хорошо или плохо? Что это означает для type checker?
Связанные уроки
- plt-03-static-vs-dynamic — Когда происходит проверка типов: compile time vs runtime
- plt-04-type-inference — Как компилятор выводит типы без явных аннотаций (HM)
- plt-08-generics — Полиморфизм - типы принимают разные формы
- fl-25-rice-theorem — Теорема Райса объясняет, почему soundness и completeness несовместимы
- fl-02-chomsky — Мощность type systems коррелирует с уровнями иерархии Хомского
- plt-09-dependent-types — Зависимые типы - предел мощности: type checker не всегда завершается
- ml-01