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

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

  • Проверка типов
  • Использование в трансляции

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

Типы имеют структуру. Будем описывать её выражениями типов.

Выражение типа:

  • либо примитивный тип
  • либо образован путём применения конструктора типа к выражениям типа

Примитивные (фундаментальные) типы – имена типов, определённые стандартом языка.

Не могут быть представлены в терминах других типов.

Например, в C: int, bool, float, void и т.п.

Конструкторы типов – “функции” над выражениями типов.

Например int[3] – массив int длины 3 – это конструктор array, применённый к аргументам 3 и int

Конструктор -> – функции

  • в левой части – тип аргумента
  • в правой - тип результата

Например, тип int floor(float x) – float -> int

Для многих аргументов – пары/кортежи.

Например, void(int, float) записывается как int × float -> void

× – конструктор пары.

Эквивалентно: (int, float) -> void.

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

int × float -> void:

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

Когда два выражения типов эквивалентны?

Два подхода:

  • Структурная эквивалентность
  • Именная эквивалентность

Обычно – оба подхода в разных контекстах.

Например, пользовательские типы (в ООП – классы) – именная эквивалентность.

  • не эквивалентны:

    struct StructOne {
  double fieldOne;
  int fieldTwo;
};

struct StructTwo {
  double fieldOne;
  int fieldTwo;
};

  • эквивалентны:

    struct StructOne {
  double fieldOne;
  int fieldTwo;
};

typedef StructOne
        StructTwo;

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

Такой вариант – в TypeScript (структурная эквивалентность в представлении JavaScript)

На практике, в основном – именная эквивалентность. Структурная – синонимы типов.

Причина – именная эквивалентность проще.

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

Для проверки типов:

  • каждому выражению языка – выражение типа
  • проверить, что типы удовлетворяют системе типов

Система типов – набор логических правил.

Проверка типов – способ обнаружения ошибок в программах.

Выполняется:

  • статически (во время компиляции)
  • динамически (в процессе выполнения)

Согласованная или надёжная система типов – все проверки возможны статически.

Строгая система типов – гарантия отсутствия ошибок типов.

Два вида правил проверки:

  • синтез типов
  • выведение типов

Синтез типов – тип выражения определяется в терминах его подвыражений.

Например,

  int x = 3;
  float y = M_PI;
  return x*y;

Тип x*y – выводится из типов x и y (по правилам C++ – float).

Выведение типов – определяет типы использованию, т.е. выводит типы выражений из контекста.

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

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

Операции над выражениями различных типов – необходимо преобразование.

Например, сложение float и int – нет машинной операции. Необходимо преобразовать int в float (или float в int)

Такие преобразования называются приведением типов.

Приведение типов:

  • явное – требуется указание в исходном коде
  • неявное – автоматическое

Также:

  • расширяющие преобразования – (почти) не теряют информацию
  • сужающие преобразования – могут терять информацию

Пусть есть типы int16 и int32, знаковые целые соответственно в 16 и 32 битах.

Тогда:

  • int16 в int32 – расширяющее
  • int32 в int16 – сужающее

Обычно неявные приведения – расширяющие.

Какие расширяющие, какие сужающие – зависит от языка.

Например, в С++ (стрелки – расширяющие):

В ООП – преобразования производных классов к базовым – расширяющие.

С точки зрения теории множеств, преобразования, к типу, имеющему больше возможных значений – расширяющие, наоборот – сужающие.

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

Перегруженная функция – различное определение в зависимости от контекста.

Также – аd-hoc полиморфизм.

Реализуется объявлением нескольких функций с одинаковым названием, но с разными реализациями.

Выбор конкретной реализации

  • на основе типов аргументов (результата)
  • т.е. на основе типа функци
  • называется разрешением перегрузки

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

Термин “полиморфность” – фрагмент кода может быть выполнен для различных типов.

Функция length на Haskell (например):

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

Работает для любых списков.

Чтобы записать тип 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 : 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.

Алгоритм:

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(ζ)

В виде графа:

Класс – после двоеточия.

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

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