Типизация

ОБЯЗАТЕЛЬНОДЛЯ НОВИЧКОВ

Разработчику Аналитику Архитектору

Типизация

Что читать в первую очередь

База: статическая и динамическая типизация, сильная и слабая, явные и неявные преобразования, типобезопасность.
Продвинуто: boxing, generics, ковариантность, зависимые типы — по мере необходимости.
Скалярные типы (int, string) — в статье Типы данных.

Типизация и система типов

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

Проверку можно выполнять заранее (статическая типизация), в момент использования (динамическая) или совмещать оба подхода (например, Variant в Delphi, пакеты в Alice ML, Data.Dynamic в Haskell). Отдельная ось — строгость преобразований: при сильной типизации несовместимые типы не смешивают без явного действия программиста; при слабой компилятор или runtime допускает неявное приведение.

О сильной и слабой типизации уместно говорить в сравнении языков: формального единого определения нет. Точнее описывают безопасность согласования типов (type safety) и безопасность доступа к памяти, а также момент проверки — в статике или в динамике. Термин "строгая типизация" в русских текстах иногда путают со строгой семантикой вычислений (strict evaluation) — это другая тема.

Архитектурные модели

Типизация — система правил, определяющих, когда и как проверяется соответствие значения его ожидаемому типу.

Представим, что программа - это работяга, сидящий за столом. На этом столе мы располагаем книги, необходимые для работы. Книги раскладываем аккуратно, с учётом их объёма - для огромной многотомной эпопеи "Война и мир" нужно много места, тогда как для номера телефона смысла в отдельной книге нет, не так ли? Вот точно так же необходимо распределять и память в компьютере - нужно понимать, когда данных будет много, как в строке, или всего два значения, как в булевом (True/False). Типизация позволяет регулировать порядок определения размеров "бронируемых" блоков памяти.

Play ITЗагрузка интерактивного демо…

Статическая и динамическая

Статическая типизация — приём, при котором переменная, параметр подпрограммы и возвращаемое значение функции связываются с типом в момент объявления, и этот тип дальше не меняется: принимаются и возвращаются только значения этого типа. Проверка согласования типов выполняется до запуска (компиляция, анализ в IDE). Примеры — Ada, C, C++, C#, D, Java, ML, Pascal, Go, Fortran, Solidity. – Преимущества — раннее выявление ошибок, предсказуемый машинный код и JIT, удобное автодополнение в IDE (лишние варианты отсекаются по типу), выгода растёт с размером проекта.
– Недостатки: многословность без вывода типов; в языках без развитой системы типов (вне семейства ML с principal typing) вывод типов иногда маскирует трудноуловимые ошибки.
Динамическая типизация — тип связывается с значением в момент присваивания, а не при объявлении имени. В разных участках программы одно и то же имя может указывать на значения разных типов. Проверка выполняется во время выполнения; отсутствие типов на этапе компиляции мешает агрессивной оптимизации и статическому анализу в IDE. Примеры — Smalltalk, Python, Ruby, PHP, Perl, JavaScript, Lisp, Objective-C. – Преимущества: гибкость при меняющемся окружении и данных неизвестной схемы, краткий код для прототипов.
– Недостатки: ошибки типов всплывают при исполнении; накладные расходы на проверку при каждой операции (даже при сложении нужно убедиться, что оба операнда подходящего типа и извлечь значения через представление объекта в памяти).

Противоположные приёмы дополняют друг друга — часть статически типизированных языков позже получили "окна" динамики (Variant, динамические пакеты, dynamic в C# 4+).

Гибридные подходы:

Type inference (вывод типов): программист не указывает тип явно, но компилятор выводит его статически (let x = 42; // x: i32 в Rust).
Gradual typing (постепенная типизация) — часть кода типизирована явно, часть — динамически (TypeScript, Python с mypy).
Dependent types (зависимые типы) — тип может зависеть от значения (например, "массив длины n") — Idris, Agda, Coq.

Сильная и слабая

Сильная (строгая) и слабая (нестрогая) типизация — характеристика системы типов, отражающая ограничения на приведение типов при присваиваниях и операциях. В языках с более мягкими правилами говорят о слабой типизации.

Исторически Лисков и Зиллес (1974, язык CLU) называли сильно типизированными языки, где при передаче объекта из вызывающей функции в вызываемую тип объекта должен быть совместим с типом, объявленным у параметра: у каждой ячейки данных — свой тип, контракты процессов выражаются через эти типы. Лука Карделли связывает сильную систему типов с полнотиповым программированием — система сильна, если исключает ошибки согласования типов во время выполнения, то есть обеспечивает типобезопасность (нет неконтролируемых срывов из-за неверного приведения).

На практике:

Сильная типизация — несовместимые типы не смешивают без явного шага. int + string — ошибка компиляции (Java, Rust) или исключение (Python). В языках по Хиндли — Милнеру понятия приведения типов нет: "преобразование" — это функция, строящая значение целевого типа из исходного.
Слабая типизация — неявные преобразования и "каламбуры типов" на уровне компилятора. Семейство C и C++: неявные numeric promotions, reinterpret_cast трактует битовое представление одного типа как другой при равной длине — источник крахов при неосторожном использовании. В учебниках по C++ систему типов иногда называют "сильной" в смысле "строже, чем в классическом C" — это сравнительная, а не формальная оценка.

Крайности: Ada — приведение типов в принципе невозможно (уникальная типизация); ассемблер, старый Fortran, Рефал — контроль типов отсутствует.

Здесь критично: слабая типизация не совпадает с динамической. Python — динамически и сильно типизирован: "5" + 2 даёт TypeError. JavaScript — динамически и слабо типизирован. PHP сравнивает значения операторами == и === — второй требует совпадения и значения, и типа (1 == "1" истинно, 1 === "1" ложно) — это особенность языка, а не обязательное свойство любой динамической типизации.

Типобезопасность

Типобезопасность (англ. type safety) — свойство языка, характеризующее надёжность его системы типов. Система типов безопасна (англ. safe, sound), если в программах, успешно прошедших проверку типов (англ. well-typed), исключена возможность ошибок согласования типов во время выполнения.

Ошибка согласования типов (англ. type error) — несогласованность типов в выражении, например деление числа на строку. Пропущенные ошибки в runtime ведут к багам и крахам. Безопасность языка не означает отсутствия всех багов, но такие сбои становятся предсказуемыми в рамках семантики языка.

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

Многие языки системного программирования (Ada, C, C++) содержат небезопасные операции — явные приведения, unsafe-блоки, reinterpret_cast — для обхода системы типов там, где нужен низкоуровневый контроль. В мейнстриме иногда сужают типобезопасность до безопасности доступа к памяти (нельзя читать чужие ячейки через указатель "не того" типа); это частный, но важный случай.

Сильная динамическая типизация (Lisp, Smalltalk) при несовместимости типов обычно бросает исключение, а не портит данные молча. Плюс — меньше консервативности, чем у статических систем (отвергают программы, которые на практике отработали бы корректно); минус — больше пробных прогонов и ниже производительность. Поэтому языки часто комбинируют статический и динамический контроль (TypeScript поверх JavaScript, аннотации и mypy в Python, optional types в C#).

Подход	Идея	Примеры
Надёжная статика	ошибки типов ловят до запуска	Standard ML, Rust (в safe-подмножестве), Haskell (без `unsafe`)
Сильная динамика	ошибки типов — исключения в runtime	Python, Ruby
Слабая динамика	неявные приведения	JavaScript
Явный обход типов	ответственность на программисте	C, C++, `unsafe` в Rust/Haskell

Преобразования типов

Преобразование типов (type conversion) — это процесс получения значения одного типа из значения другого. Его можно классифицировать по нескольким ортогональным признакам:

1. По способу инициации

Явное (explicit, cast) — программист прямо указывает необходимость преобразования:

  double d = 3.14;
  int n = (int) d;  // отбрасывание дробной части

Неявное (implicit, coercion) — преобразование выполняется автоматически компилятором/интерпретатором при операции или присваивании:

  int a = 5;
  double b = a;  // int → double — расширение без потерь

2. По наличию потерь информации

Расширяющее (widening) — преобразование к типу с большим диапазоном или точностью:
int8 → int32, int → double, char → int. Обычно безопасно и разрешено неявно.
Сужающее (narrowing) — преобразование к типу с меньшим диапазоном или точностью:
int32 → int8, double → int, string → int. Потенциально опасно:
- Переполнение: int32 = 300 → uint8 = 44 (300 mod 256),
- Потеря точности: double = 1e20 + 1 → int64 = 100000000000000000000 (единица исчезает из-за недостаточной точности мантиссы),
- Неопределённость: string = "abc" → int — как интерпретировать?

3. По гарантиям корректности

Безопасное (safe) — если исходное значение лежит в подмножестве, представимом целевым типом, преобразование обратимо и сохраняет смысл. Пример: uint8 → int32.
Небезопасное (unsafe) — преобразование возможно всегда, но результат может быть семантически некорректным. Пример: pointer → int в C — нарушает абстракцию памяти и приводит к undefined behavior при неправильном использовании.

Критические случаи и ловушки

a) Числовые преобразования

Целое ↔ вещественное:
При преобразовании double → int стандарт не определяет поведение для значений вне диапазона int (в C/C++ это UB). В Java — ArithmeticException при Math.toIntExact(), или усечение при прямом касте (с потерей).
При int → float значения свыше 2^{24} (для float32) перестают быть представимыми точно:

  float(16777216) == 16777216.0   # True
  float(16777217) == 16777216.0   # True — потеря единицы!

Беззнаковое ↔ знаковое:
В языках без строгого различия (C) сравнение uint32 = 0xFFFFFFFF и int32 = -1 даёт true. В Java — требуется явный каст:

  int i = -1;
  long l = i & 0xFFFFFFFFL; // 4294967295L

b) Строковые преобразования

Парсинг числа из строки:
"123" → 123 — тривиально.
"123.45" → int — ошибка или усечение?
" 123 " — игнорировать пробелы или нет?
"1.23e2" — поддерживать экспоненциальную запись?

Отсутствие стандартизации ведёт к уязвимостям:
- "010" → 8 (восьмеричное в старых версиях JavaScript),
- локаль-зависимые разделители (1,234.56 vs 1.234,56).
Сериализация/десериализация:
JSON-число 12345678901234567890 при чтении в JavaScript (где все числа — double) превращается в 12345678901234567000 — необратимая потеря точности.

c) Указатели и низкоуровневые преобразования

Pointer reinterpretation (в C/C++):

  int x = 0x41424344;
  char* p = (char*)&x;
  printf("%c", *p); // 'D' на little-endian, 'A' на big-endian

— нарушает strict aliasing rule и вызывает UB.

Type punning через union — разрешено в C, но не в C++.

Рекомендация проектирования:

Избегайте неявных сужающих преобразований,

Всегда проверяйте диапазон при парсинге,

Используйте строгие функции (parseInt("123", 10), а не +"123" в JS).

Упаковка и распаковка (boxing/unboxing)

В системах с единым корневым типом (например, Object в Java, System.Object в C#, Any в Swift/Kotlin), все значения — даже скаляры — могут быть представлены как объекты. Однако скаляры (int, bool) хранятся непосредственно в стеке или в полях структур, а объекты — в куче, со служебной информацией (vtable, sync word и пр.).

Упаковка (boxing) — преобразование значения скалярного типа в объектную обёртку:

int x = 42;
Object obj = x;  // компилятор вставляет: Integer.valueOf(x)

Распаковка (unboxing) — обратное преобразование:

Integer boxed = 42;
int y = boxed;   // компилятор вставляет: boxed.intValue()

Архитектурные последствия

Аспект	Упакованный тип	Непосредственное значение
Хранение	Куча (динамическое выделение)	Стек / встроенные поля
Размер	`≥` 16 байт (на 64-битной JVM: заголовок 12 байт + 4 байта int + выравнивание)	4 байта (`int`)
Производительность	Аллокация + сборка мусора	Нулевые накладные расходы
Семантика	Поддержка `null`, полиморфизм (`List<Object>`), рефлексия	Нет `null`, нет наследования

Проблемы

Производительность:
В цикле for (int i = 0; i < 1_000_000; i++) list.add(i) происходит 1 млн аллокаций объектов Integer, даже если JIT частично оптимизирует это через escape analysis.
Null-безопасность:

   Integer a = null;
   int b = a;  // NullPointerException при распаковке

— ошибка времени выполнения, неуловимая статически.

Сравнение через ==:

   Integer a = 127, b = 127;
   System.out.println(a == b); // true (кеширование [-128; 127])
   Integer c = 128, d = 128;
   System.out.println(c == d); // false (новые объекты)

— источник многочисленных багов.

Современный тренд:

Введение value types (Project Valhalla в Java, struct в C#/Swift),

Отказ от автоматического боксинга в новых языках (Rust, Go),

Использование Option<T> вместо null.

Параметрический полиморфизм (generics)

Параметрический полиморфизм — механизм описания алгоритмов и структур данных, независимых от конкретного типа элементов. Он обеспечивает повторное использование кода без потери типовой безопасности.

Сравним подходы:

Подход	Пример	Проблемы
*Без типов (void, Object)**	`void* array[10]`	Нет проверок: можно положить `int`, извлечь как `string` → катастрофа.
Макроподстановка	`#define MAKE_STACK(T) ...` в C	Дублирование кода, отсутствие ABI-совместимости, сложность отладки.
Generics	`List<T>`, `HashMap<K, V>`	Безопасность, эффективность (в Java — стирание типов; в C#/Rust — мономорфизация).

Ключевые концепции

a) Инвариантность, ковариантность, контравариантность

Пусть Cat <: Animal (кошка — подтип животного). Как связаны List<Cat> и List<Animal>?

Инвариантность (List<T> в Java/C#):
List<Cat> и List<Animal> — несравнимы.
Почему? Потому что можно сделать:

  List<Animal> animals = cats;  // если бы разрешалось
  animals.add(new Dog());       // в список кошек добавлена собака!
  Cat c = cats.get(0);          // ClassCastException

Ковариантность (List<? extends Animal> в Java, IEnumerable<out T> в C#):
Разрешает только чтение:

  List<? extends Animal> animals = cats; // OK
  Animal a = animals.get(0);              // OK
  animals.add(new Dog());                 // Запрещено компилятором

Контравариантность (Action<in T>, Comparator<? super T>):
Разрешает только запись:

  Comparator<Animal> comp = (a1, a2) -> a1.weight - a2.weight;
  List<Cat> cats = ...;
  cats.sort(comp); // OK: компаратор для животных годится и для кошек

b) Ограничения типов (bounds)

Верхняя граница — T extends Comparable<T> — гарантирует, что T реализует сравнение,
Нижняя граница — T super File — редко используется, но критична для producer-consumer паттернов (PECS: Producer extends, Consumer super).

c) Реификация

Стирание типов (type erasure) (Java):
В runtime List<String> и List<Integer> — один и тот же класс List. Типы существуют только на этапе компиляции.
— Плюсы: обратная совместимость, компактный bytecode.
— Минусы: невозможность new T(), instanceof List<String>.
Мономорфизация (monomorphization) (C++, Rust, C# для значимых типов):
Компилятор генерирует отдельный код для каждого конкретного типа:

  fn max<T: Ord>(a: T, b: T) -> T { ... }

  max(1i32, 2i32);   // → специализированная версия для i32
  max("a", "b");     // → отдельная версия для &str

— Плюсы: максимальная производительность, поддержка рефлексии.
— Минусы: раздувание кода (code bloat).

Типы и формальная верификация

Типовые системы эволюционировали от простой проверки совместимости к инструменту доказательства корректности программ.

Уровни строгости

Уровень	Возможности	Примеры
Номинальная типизация	Проверка по именам типов (`class A` ≠ `class B`, даже с одинаковыми полями)	Java, C#
Структурная типизация	Проверка по структуре (`{ x: int, y: int }` совместимо с любым типом, имеющим `x` и `y`)	TypeScript, Go (`interface{}`), OCaml
Система типов с эффектами	Отслеживание side effects: `IO`, `throws`, `mutable`	Haskell (`IO a`), Kotlin (`suspend`), Eff language
Зависимые типы	Тип зависит от значения: `Vector n` (вектор длины n), `Fin n` (число `< n`)	Idris, Agda, Coq, Lean

Пример — доказательство отсутствия выхода за границы массива

В обычном языке:

int get(int* arr, int len, int i) {
    return arr[i];  // UB при i < 0 или i ≥ len
}

В языке с зависимыми типами (Idris):

get : (arr : Vect n a) -> (i : Fin n) -> a
get (x :: xs) FZ = x
get (x :: xs) (FS k) = get xs k

Здесь:

Vect n a — вектор длины n типа a,
Fin n — тип натуральных чисел строго меньше n,
Компилятор гарантирует, что i всегда в пределах [0, n),
Функция полна: все случаи покрыты.

То есть, ошибка времени выполнения становится невозможной на уровне типов.

Практическое применение:

Проверка безопасности памяти (Rust ownership System),

Верификация протоколов (TLA+, Tamarin),

Доказательство корректности криптографических примитивов (Project Everest).

Перспективы

1. Линейные и аффинные типы

Гарантируют, что значение используется ровно один раз (линейный) или не более одного раза (аффинный). Применение:

Управление ресурсами (файлы, сокеты),
Предотвращение двойного освобождения памяти,
Квантовые вычисления (где копирование запрещено теоремой no-cloning).

2. Типы как первоклассные сущности

В некоторых языках (например, Julia) типы — значения времени выполнения:

T = Float64
x = T(3.14)  # 3.14::Float64

Это позволяет динамически генерировать специализированный код под конкретные типы (multiple dispatch).

3. Типы и безопасность

Типобезопасность на уровне дизайна API:

Типобезопасный FFI — запрет передачи String в C-функцию, ожидающую char*, без проверки кодировки (Rust CString).
Разделение привилегий — тип SecretKey нельзя передать в функцию без метки trusted.

Источники и смежные материалы

Теоретическая база статьи согласована с русскоязычной Википедией (CC BY-SA): тип данных, статическая типизация, динамическая типизация, сильная и слабая типизация, типобезопасность. Учебное изложение — Б. Пирс, "Типы в языках программирования" (пер. Добросвет, 2012).

Типизация

Типизация

Типизация и система типов

Архитектурные модели

Статическая и динамическая

Сильная и слабая

Типобезопасность

Преобразования типов

1. По способу инициации

2. По наличию потерь информации

3. По гарантиям корректности

Критические случаи и ловушки

a) Числовые преобразования

b) Строковые преобразования

c) Указатели и низкоуровневые преобразования

Упаковка и распаковка (boxing/unboxing)

Архитектурные последствия

Проблемы

Параметрический полиморфизм (generics)

Ключевые концепции

a) Инвариантность, ковариантность, контравариантность

b) Ограничения типов (bounds)

c) Реификация

Типы и формальная верификация

Уровни строгости

Пример — доказательство отсутствия выхода за границы массива

Перспективы

1. Линейные и аффинные типы

2. Типы как первоклассные сущности

3. Типы и безопасность

Источники и смежные материалы

См. также

Данные и информация

Виды информации

Типы данных в вычислительных системах

Метаданные

Данные и информация — итоги

Данные и информация — чек-лист

Типизация​

Типизация и система типов​

Архитектурные модели​

Статическая и динамическая​

Сильная и слабая​

Типобезопасность​

Преобразования типов​

1. По способу инициации​

2. По наличию потерь информации​

3. По гарантиям корректности​

Критические случаи и ловушки​

a) Числовые преобразования​

b) Строковые преобразования​

c) Указатели и низкоуровневые преобразования​

Упаковка и распаковка (boxing/unboxing)​

Архитектурные последствия​

Проблемы​

Параметрический полиморфизм (generics)​

Ключевые концепции​

a) Инвариантность, ковариантность, контравариантность​

b) Ограничения типов (bounds)​

c) Реификация​

Типы и формальная верификация​

Уровни строгости​

Пример — доказательство отсутствия выхода за границы массива​

Перспективы​

1. Линейные и аффинные типы​

2. Типы как первоклассные сущности​

3. Типы и безопасность​

Источники и смежные материалы​

См. также

09Данные и информация

09Виды информации

09Типы данных в вычислительных системах

09Метаданные

09Данные и информация — итоги

09Данные и информация — чек-лист

Типизация

Типизация и система типов

Архитектурные модели

Статическая и динамическая

Сильная и слабая

Типобезопасность

Преобразования типов

1. По способу инициации

2. По наличию потерь информации

3. По гарантиям корректности

Критические случаи и ловушки

a) Числовые преобразования

b) Строковые преобразования

c) Указатели и низкоуровневые преобразования

Упаковка и распаковка (boxing/unboxing)

Архитектурные последствия

Проблемы

Параметрический полиморфизм (generics)

Ключевые концепции

a) Инвариантность, ковариантность, контравариантность

b) Ограничения типов (bounds)

c) Реификация

Типы и формальная верификация

Уровни строгости

Пример — доказательство отсутствия выхода за границы массива

Перспективы

1. Линейные и аффинные типы

2. Типы как первоклассные сущности

3. Типы и безопасность

Источники и смежные материалы

Данные и информация

Виды информации

Типы данных в вычислительных системах

Метаданные

Данные и информация — итоги

Данные и информация — чек-лист