Работа с типами в процессе компиляции может быть разбита на две категории:

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

Выражения типов

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

Примитивные типы (так же называемые фундаментальными) – это конечное множество имён типов, определённых в стандарте языка, которые не могут быть представлены в терминах других типов. Например, в C это такие типы как int, bool, float и т.п. В том числе void, являющийся единичным типом.

Конструкторы типов – это своего рода функции над выражениями типов. Например, конструкцию int[3], выражающую массив 3 значений типа int, можно представить как применение конструктора array к аргументам 3 и int: array(3, int).

Для типа функций часто используется конструктор ->, в левой части – тип аргумента, в правой - тип результата. Для функций многих аргументов обычно используется декартово произведение аргументов, например тип функции void(int, float) может быть записан как int × float -> void, где × – конструктор типа декартова произведения. Эквивалентная запись использует оператор кортежа вместо оператора декартова произведения: (int, float) -> void. Эти записи эквивалентны.

Для представления выражений типов удобно использовать синтаксические деревья или ориентированные ациклические графы.

Эквивалентность типов

Когда два выражения типов эквивалентны? Существует два подхода к ответу на этот, на первый взгляд, простой вопрос.

Мы говорим о структурной эквивалентности типов, если все операции, определённые для значений одного типа без изменений применимы так же и к другому типу. Так, скажем, синонимы типов (typedef в С) объявляют структурно эквивалентные типы.

Мы говорим об именной эквивалентности типов, если в выражениях типов совпадают конструкторы типов, и их аргументы эквиваленты (в смысле именной эквивалентности). Фундаментальные типы эквивалентны если у них совпадают имена.

Большинство языков программирования в различных контекстах используют оба определения эквивалентности. Так, например, эквивалентность пользовательских типов (обычно классов в ООП-языках) часто рассматривается с точки зрения именной эквивалентности. Например, нельзя взаимозаменяемо использовать следующие типы в C++:

struct StructOne {
  double fieldOne;
  int fieldTwo;
};

struct StructTwo {
  double fieldOne;
  int fieldTwo;
};

(если, конечно, не использовать явное приведение типов, типа reinterpret_cast но это уже выход за пределы системы типов)

Но при этом такое определение позволяет их использовать взаимозаменяемо:

struct StructOne {
  double fieldOne;
  int fieldTwo;
};

typedef StructOne StructTwo;

Доведённая до предела идея структурной эквивалентности позволяет использовать любые типы, имеющие на каком-то определённом уровне одинаковое представление, взаимозаменяемо. Такой вариант используется, например в TypeScript (рассматривается структурная эквивалентность в представлении на JavaScript).

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