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

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

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

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

Примитивные типы (так же называемые фундаментальными) – это конечное множество имён типов, определённых в стандарте языка, которые не могут быть представлены в терминах других типов. Например, в 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).

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

Проверка типов

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

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

Правила проверки типов могут иметь две формы: синтеза типов и выведения типов.

Синтез типов – в каком-то смысле более простой вариант. Он требует, чтобы типы, связанные с идентификаторами, были объявлены до использования этих идентификаторов. Тип выражения определяется логической формулой в терминах его подвыражений.

Выведение типов определяет типы выражений по тому, как эти выражения используются, т.е. выводит типы выражений из контекста. Например, если у нас есть функция length, принимающая аргументом список, то, встретив выражение length(x) компилятор делает вывод, что x должен быть списком (компилятор не может сделать вывод о типе элемента списка, но для функции length это и не важно).

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

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

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

Для примера рассмотрим выражение x+y. Оба операнда сложения должны иметь одинаковый тип, поскольку машинные операции сложения определены, как правило, только для значений в одинаковом формате. Тогда если x и y имеют разные типы, скажем, T1 и T2, то T1 должен быть приведён к T2 или T2 к T1. Различают расширяющие преобразования и сужающие преобразования. Расширяющие преобразования, как правило, не теряют информацию. Сужающие могут приводить к потере информации.

Допустим, наш язык поддерживает типы знаковых целых int16 и int32, хранящиеся соответственно в 16 и 32 битах. Тогда преобразование от int16 к int32 будет расширяющим, поскольку все значения типа int16 представимы в типе int32, а преобразование int32 к int16 – сужающим, поскольку обратное неверно.

Как правило, в качестве неявных преобразований используются только расширяющие. Технических ограничений нет, но это разумный подход из “принципа наименьшего удивления”.

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

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

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

Перегрузка функций

Перегруженная функция может иметь различное значение в зависимости от контекста. По сути, это форма полиморфизма, называемая ad-hoc полиморфизм. Как правило, перегрузка реализуется объявлением нескольких функций с одинаковым названием, но с разными реализациями, и выбор конкретной реализации осуществляется на основе типов аргументов (и иногда типа результата). По сути, выбор реализации производится на основе типа функции.

Выбор конкретной реализации в процессе компиляции называется разрешением перегрузки.

Параметрический полиморфизм и выведение типов

Термин “полиморфность” относится к любому фрагменту кода, который может быть выполнен для различных типов. Например, функция length, возвращающая длину списка, на Haskell может быть реализована следующим образом:

length xs = if null xs then 0 else 1+length (tail xs)

Здесь функция null возвращает True для пустого списка, tail отбрасывает первый элемент списка и возвращает остальной список.

Эта функция работает для любых списков, независимо от типа элемента списка. Тогда, чтобы записать тип функции length мы должны использовать так называемую универсальную квантификацию:

length : ∀α. list(α) -> integer

Здесь list – конструктор типа списка, -> – конструктор типа функции, α – переменная типа, которая может принимать значение любого типа, что собственно и обозначается ∀α.

Каждый раз, когда используется полиморфная функция, связанная с ней переменная типа может иметь разное значение (т.е. разный тип). В процессе проверки типов универсальная квантификация убирается и переменная заменяется на конкретный тип.

Поскольку в выражениях могут присутствовать переменные типов, необходимо пересмотреть понятие эквивалентности типов. Если выражение e1 : a -> b применяется к значению e2 : c, то вместо простого понятия эквивалентности a и c мы должны их унифицировать.

Например, при вызове

length([1,2,3])

где [1,2,3] : list(integer), компилятор должен сравнить тип первого аргумента функции ∀α. list(α) с типом значения, передаваемого аргументом list(integer) и найти такую подстановку для α, чтобы эти типы стали эквивалентными. В данном случае подходит подстановка α ⇒ integer, и тип length становится length : list(integer) -> integer.

Алгоритм унификации

Для двух выражений типов s и t, алгоритм унификации определяет, можно ли сделать эти выражения идентичными путём подстановки выражений вместо переменных типов. Если s и t не содержат переменных, то они унифицируются только тогда, когда они идентичны.

Рассмотрим алгоритм унификации типов, работающий на графах. Мы представляем выражения типов графами, где переменные типов представлены листьями, а конструкторы типов – внутренними узлами. Узлы группируются в т.н. классы эквивалентности: если два узла принадлежат одному и тому же классу эквивалентности, то выражения типов, которые они представляют, унифицируются.

Изначально каждый узел принадлежит классу эквивалентности, состоящему только из него самого.

Реализуем классы эквивалентности через указатели на представителя класса эквивалентности. Каждый узел графа имеет свойство set, указывающее на другой узел или имеющее значение 0. Представителем класса эквивалентности является один произвольно выбранный узел в графе выражения типа, и у него set = 0.

Определим функцию find(n), которая возвращает представителя класса эквивалентности, содержащего узел n. Эта функция может быть реализована например следующим образом:

Node find(Node n) {
  Node result = n;
  while (result.set != 0) {
    result = result.set;
  }
  return result;
}

Определим так же функцию union(m,n), объединяющую классы эквивалентности, содержащие узлы m и n. Если один из классов эквивалентности m или n содержит не переменную, а другой – только переменные, то всем узлам назначается именно тот класс эквивалентности, в котором есть не переменная. В противном случае выбор произвольный. Это можно отслеживать, устанавливая в процессе унификации флаг на узлах-представителях.

Тогда алгоритм можно записать:

boolean unify(Node m, Node n) {
  s = find(m);
  t = find(n);
  if (s == t) return true;
  else if (equivalent(s, t)) {
    // s и t эквивалентные фундаментальные типы
    // или эквивалентные конструкторы типа
    if(!s.hasChildren && !t.hasChildren) {
      // s и t -- фундаментальные
      return true;
    }
    union(s, t);
    return unify(s[0], t[0]) && unify(s[1], t[1]);
  } else(s.isVar || t.isVar) {
    // s или t -- переменная
    union(s,t);
    return true;
  } else return false;
}

Например, рассмотрим типы

((α -> β) × list(γ)) -> list(β)
((γ -> δ) × list(γ)) -> list(ζ)

Их можно представить графом

После двоеточия указан класс эквивалентности. В начале работы алгоритма каждый узел в собственном классе эквивалентности.

Мы хотим унифицировать эти типы. Тогда мы должны вызвать unify с узлами →:2 и →:4. На первом шаге выполняется ветка equivalent(s, t). Классы эквивалентности 2 и 4 объединяются (пусть выбирается узел 2), и алгоритм унификации рекурсивно вызывается для пар соответствующих аргументов, аналогично для узлов ×:5 и ×:6 выбирается класс, например, 5, для list:8 и list:10 – класс 8, и алгоритм рекурсивно вызывается для всех дочерних узлов.

Для →:1 и →:3 назначается класс 1, для list:7 и list:9 – класс 7.

При унификации β:12 и ζ:15, срабатывает предпоследняя ветка, обоим назначается класс эквивалентности 12, рекурсия в этой ветви завершается.

При унификации дочерних узлов list:7 и list:9, срабатывает первая ветка s == t.

При унификации дочерних узлов →:1 и →:3, классы эквивалентности α:11 и γ:13, и классы эквивалентности β:12 и δ:14 объединяются.

В результате после завершения алгоритма получаем следующие классы эквивалентности:

Алгоритм унификации здесь завершается успешно.

Выражения типов. Эквивалентность типов. Синтез и выведение. Проверка