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

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

• корректная - выведенные и назначенные системой типы соответствуют поведению программы

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

• дружественная для разработчика - типы описываются, реализуются и комбинируются с помощью основных операций над множествами: объединение, пересечение и отрицание (поэтому это система множественно-теоретических типов)

Текущая веха направлена на вывод типов из шаблонов и условий и их использование для проверки типов программ, что позволяет компилятору Elixir обнаруживать ошибки и баги в кодовых базах без необходимости внесения изменений в существующее программное обеспечение. Подписанные пользователем сигнатуры типов запланированы на будущие релизы. Основные принципы, теория и дорожная карта нашей работы изложены в "The Design Principles of the Elixir Type System" by Giuseppe Castagna, Guillaume Duboc, José Valim.

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

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

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

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

• tuple() - он представляет все кортежи. Кортежи также могут быть записаны с использованием синтаксиса фигурных скобок, например {:ok, binary()}. ... в конце кортежа означает, что общий размер кортежа неизвестен. Например, следующий кортеж содержит как минимум два элемента: {:ok, binary(), ...}.

• list(type) - он представляет список type. Более точно, он может быть записан как empty_list() or non_empty_list(type, empty_list()). Неправильные списки, которые не заканчиваются пустым списком, такие как [1, 2 | 3], могут быть записаны как list(integer(), integer()).

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

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

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

Мы комбинируем типы, используя операции над множествами. Например, чтобы сказать, что функция возвращает атомы или целые числа, можно написать: 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()). Затем, основываясь на шаблонах и условиях, мы можем уточнить значение переменной x до dynamic() and integer() и dynamic() and boolean() для каждого случая соответственно. Мы говорим, что 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 с осмысленными предупреждениями.

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

Вывод типов

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

Вывод сигнатур типов сопряжен с рядом компромиссов:

• Скорость - алгоритмы вывода типов часто более ресурсоемки, чем алгоритмы проверки типов.

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

• Инкрементная компиляция - вывод типов усложняет инкрементную компиляцию. Если модуль A зависит от модуля B, который зависит от модуля C, изменение в C может потребовать реконструкции сигнатуры типа в B, что может потребовать перекомпиляции A (и так далее). Эта цепочка зависимостей может потребовать от крупных проектов явно добавлять сигнатуры типов для стабильности и эффективности компиляции.

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

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

• Локальный вывод типов - система типов автоматически выводит типы переменных в месте их определения.

• Вывод типов шаблонов (и условий в будущих релизах) - типы аргументов функции автоматически выводятся на основе шаблонов и условий, которые фиксируют и сужают типы на основе общих конструкций Elixir.

• Модульно-локальный вывод типов возвращаемых значений - постепенные типы возвращаемых значений функций вычисляются с учетом всех функций в самом модуле. Любой вызов функции в другом модуле консервативно предполагается возвращать dynamic().

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

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

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

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

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

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

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

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