Оси систем типов

Системы типов различаются по двум независимым измерениям. Их смешение - или подмена размытыми терминами вроде "строгая" - приводит к спорам, где собеседники не согласны друг с другом по поводу того, что ни один из них даже не назвал.

Статическая или динамическая - когда проверяются типы

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

Динамическая типизация проверяет типы во время выполнения. Каждое значение несёт тег типа, который среда исполнения проверяет по мере необходимости - при попытке выполнить операцию, при диспетчеризации метода или при распаковке значения.

Это отличается от бестиповой модели (untyped), где проверки типов не происходят вовсе - ни статически, ни динамически. Ассемблер бестиповой. Динамически типизированный язык полноценно типизирован; проверки в нём просто выполняются позже.

Сильная или слабая - насколько допустимо неявное приведение

Сильная типизация означает, что язык отказывается неявно преобразовывать типы друг в друга. Операции, смешивающие разные типы, либо завершаются ошибкой, либо требуют явного приведения.

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

Это измерение касается неявности преобразований, а не самого наличия типов.

Обе оси ортогональны

Часто ошибочно полагают, будто статическая типизация подразумевает сильную, а динамическая - слабую. В четырёхклеточной матрице примеры есть для каждого квадранта:

• Статическая + слабая: C. Компилятор проверяет типы статически, но позволяет интерпретировать char* как int* и выполнять над ним арифметические операции.
• Статическая + сильная: Haskell, Rust. Проверка во время компиляции без неявных преобразований.
• Динамическая + сильная: Python. Типы проверяются во время выполнения, но "3" + 4 приводит к ошибке, а не к "34" или 7.
• Динамическая + слабая: JavaScript, PHP. Проверки во время выполнения, но "3" + 4 === "34" и "3" * 4 === 12.

Почему термины "строгая" и "нестрогая" всё запутывают

В дискуссиях термины "строгая типизация" (strict) или "нестрогая типизация" (loose) часто ставят вместо одного из четырёх стандартных понятий. Восстановить смысл при такой подмене невозможно: читатель не может понять, означает ли "строгая" статическую, сильную или обе сразу. Льюис Кэмпбелл (Lewis Campbell) считает, что такие термины придумывают люди, которые не освоили двухосевую модель и хотят свести всё к одному ползунку - которого в реальности нет.

Зависимые типы находятся на дальнем конце статической оси: свойства, проверяемые до запуска программы, могут быть произвольными, а zstd-lean-proof-automation показывает, чего на практике стоит доказательство одного из них - простоты числа или уникальной достижимости.

Исходный пост описан в type-systems-vocabulary. sqlite-strict-tables - пример оси сильной/слабой типизации (приведения типов) в базах данных: гибкая типизация SQLite по умолчанию приводит значения к сродству типов (affinity) колонки, а таблицы STRICT это отключают; "strict" здесь обозначает именно ось приведения, а не статическую/динамическую типизацию.