Исходный код Постепенные множественно-теоретические типы

Elixir в процессе внедрения множественно-теоретических типов в компилятор. Этот документ описывает текущую стадию нашей реализации.

Текущая веха направлена на выведение типов из шаблонов и защитных условий и их использование для проверки типов программ, позволяя Elixir-компилятору находить ошибки и баги в коде без необходимости изменений в существующем ПО. Основные принципы, теория и дорожная карта нашей работы описаны в "Принципах проектирования системы типов Elixir" (Giuseppe Castagna, Guillaume Duboc, José Valim).

Поддерживаемые типы

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

• binary(), integer(), float(), pid(), port(), reference() - эти типы неделимы. Это означает, что как 1 так и 13 получают один и тот же тип integer().

• atom() - он представляет все атомы и является делимым. Например, атом :foo и :hello_world также являются допустимыми (различными) типами.

• map() и структуры - карты могут быть «закрытыми» или «открытыми». Закрытые карты допускают только указанные ключи, такие как %{key: atom(), value: integer()}. Открытые карты поддерживают любые другие ключи в дополнение к указанным, и их определение начинается с ..., например, %{..., key: atom(), value: integer()}. Структуры представляют собой закрытые карты с ключом __struct__.

• tuple(), list(), и function() - в настоящее время они моделируются как неделимые типы. Следующие версии Elixir также введут здесь более подробные типы.

Операции над множествами

Мы можем комбинировать множественно-теоретические типы, используя операции над множествами (отсюда и название). Например, чтобы указать, что функция возвращает либо атомы, либо целые числа, можно записать: atom() or integer().

Пересечения доступны через оператор and, например, atom() and integer(), который в данном случае становится пустым множеством none(). term() - объединение всех типов, также известный как «верхний» тип.

Пересечения полезны при моделировании функций. Например, представьте следующую функцию:

def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

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

Мы можем сказать, что эта функция имеет тип (integer() -> integer()), потому что она способна принимать целое число и возвращать целое число. В этом случае (integer() -> integer()) — это множество, представляющее все функции, которые могут принимать целое число и возвращать целое число. Даже если эта функция может принимать другие аргументы и возвращать другие значения, она все равно входит в множество (integer() -> integer()).

Эта функция также имеет тип (boolean() -> boolean()), потому что она принимает булевы значения и возвращает булевы значения. Следовательно, мы можем сказать, что общий тип функции — (integer() -> integer()) and (boolean() -> boolean()). Пересечение означает, что функция принадлежит обоим множествам.

На этом этапе некоторые могут спросить, почему не объединение? В качестве реального примера возьмем футболку с зелеными и желтыми полосками. Мы можем сказать, что футболка принадлежит множеству «футболки зеленого цвета». Мы также можем сказать, что футболка принадлежит множеству «футболки желтого цвета». Давайте рассмотрим разницу между объединением и пересечением:

• (t_shirts_with_green() or t_shirts_with_yellow()) — содержит футболки либо зеленого, либо желтого цвета, такие как зеленая, зеленая и красная, зеленая и желтая, желтая, желтая и красная и т. д.

• (t_shirts_with_green() and t_shirts_with_yellow()) — содержит футболки как зеленого, так и желтого (и других) цветов.

Поскольку футболка имеет оба цвета, мы говорим, что она принадлежит пересечению обоих множеств. Точно так же функция, которая работает от (integer() -> integer()) и (boolean() -> boolean()), также является пересечением. На практике не имеет смысла определять объединение двух функций в Elixir, поэтому компилятор всегда укажет правильное направление.

Наконец, мы также можем инвертировать типы, используя not. Например, чтобы выразить все атомы, за исключением атомов :foo и :bar, можно написать: atom() and not (:foo or :bar).

Тип dynamic()

Существующие программы Elixir не имеют деклараций типов, но мы все равно хотим иметь возможность их проверять. Это делается с помощью введения типа dynamic().

Когда Elixir видит следующую функцию:

def negate(x) when is_integer(x), do: -x
def negate(x) when is_boolean(x), do: not x

Elixir проверяет её как если бы функция имела тип (dynamic() -> dynamic()). Мы говорим, что dynamic() — это постепенный тип, что приводит нас к постепенным множественно-теоретическим типам.

Проще всего представить dynamic() в Elixir, как диапазон типов. Если у вас есть тип atom() or integer(), основной код должен работать как с atom() or integer(). Например, если вы вызываете Integer.to_string(var), а var имеет тип atom() or integer(), система типов выдаст предупреждение, потому что Integer.to_string/1 не принимает атомы.

Однако, пересекая тип с dynamic(), мы делаем тип постепенным, а значит, только подмножество типа должно быть валидным. Например, если вы вызываете Integer.to_string(var), а var имеет тип dynamic() and (atom() or integer()), система типов не выдаст предупреждение, потому что Integer.to_string/1 работает хотя бы с одним из типов. Для удобства большинство программ будут писать dynamic(atom() or integer()) вместо пересечения. Они эквивалентны.

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

Как только Elixir введет типизированные сигнатуры функций, типизированные программы Elixir будут вести себя как статически типизированный код, если не используется тип dynamic(). Это приводит нас к последнему замечанию о динамических типах в Elixir: динамические типы всегда находятся на уровне корня. Например, когда вы пишете кортеж типа {:ok, dynamic()}, Elixir перепишет его на dynamic({:ok, term()}). Хотя это имеет недостаток, что вы не можете сделать постепенным часть кортежа/карты/списка, только весь кортеж/карту/список, это имеет преимущество, что динамический всегда явно находится на уровне корня, что делает случайное использование dynamic() в статически типизированной программе сложнее.

Дорожная карта

Текущая веха — реализация вывода типов и проверки типов Elixir-программ без изменений в языке Elixir. На данном этапе мы хотим собрать отзывы о качестве сообщений об ошибках и производительности, и поэтому система типов не имеет API, ориентированного на пользователя.

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

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

Благодарности

Разработка системы типов стала возможной благодаря сотрудничеству CNRS и Remote. Исследования частично поддерживались Supabase и Fresha. Работа по разработке спонсируется Fresha, Starfish* и Dashbit.