Зависимые типы — будущее языков программирования

Всем привет!

Несмотря на диковинность и некоторую отвлеченность рассматриваемой сегодня темы — надеемся, что она сможет разнообразить вам выходные. В конце поста помещаем три ссылки от автора, позволяющие познакомиться с зависимой типизацией в Idris, F# и JavaScript

Иногда создается впечатление, словно языки программирования почти не изменились с 60-х годов. Когда мне об этом говорят, я часто вспоминаю, сколько крутых инструментов и возможностей теперь есть в нашем распоряжении, и как они упрощают жизнь. Навскидку: это и интегрированные отладчики, и модульные тесты, и статические анализаторы, и крутые IDE, а также типизированные массивы и многое другое. Развитие языков – процесс долгий и поступательный, и здесь нет таких «серебряных пуль», с появлением которых развитие языков бы изменилось раз и навсегда.

Сегодня я хочу рассказать вам об одном из последних этапов в этом поступательном процессе. Технология, о которой пойдет речь, пока активно исследуется, но все указывает на то, что вскоре она укоренится в мейнстримовых языках. А начинается наша история с одной из самых фундаментальных концепций в информатике: с типов.

Мир типов

Типизация – одна из тех вещей, которые настолько неотделимы от нашего мышления, что мы едва ли даже задумываемся о концепции типов как таковой? Почему 1 – это int, но, стоит только поместить это значение в кавычки – и оно превращается в string? Что же такое «тип», в сущности? Как это часто бывает в программировании, ответ зависит от формулировки вопроса.

Типы многообразны. В некоторых системах типов существуют очень четкие границы между типами и значениями. Так, 3, 2 и 1 – это значения типа integer, но integer – это не значение. Этот конструкт «вмурован» в язык и принципиально отличается от значения. Но, на самом деле, такое различие необязательно и может лишь ограничивать нас.

Если освободить типы и превратить их в еще одну категорий значений, то открывается ряд потрясающих возможностей. Значения можно хранить, преобразовывать и передавать функциям. Таким образом, можно было бы сделать функцию, принимающую тип в качестве параметра, создавая обобщенные функции: такие, которые могут работать со множеством типов без перегрузок. Можно иметь массив значений заданного типа, а не заниматься странной арифметикой указателей и приведением типов, как приходится делать в C. Также можно собирать новые типы по ходу выполнения программы и обеспечивать такие возможности, как, например, автоматическая десериализация JSON. Но, даже если трактовать типы как значения, все равно с типами не сделаешь всего того, что можно делать со значениями. Так, оперируя экземплярами user, можно, например, сравнивать их имена, проверять их возраст или идентификатор и т.д.

if user.name == "Marin" && user.age < 65 {
    print("You can't retire yet!")
}

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

if typeof(user) == User {
    print("Well, it's a user. That's all I know")
}

Как было бы круто, если бы у нас была функция, способная получать лишь непустой список пользователей? Либо функция, которая принимала бы адрес электронной почты, лишь если он записан в правильном формате? Для этих целей вам понадобились бы типы «непустой массив» или «адрес электронной почты». В данном случае речь идет о типе, зависящем от значения, т.е. о зависимом типе. В мейнстримовых языках подобное невозможно.

Чтобы типами можно было пользоваться, компилятор должен проверять их. Если вы утверждаете, что переменная содержит integer, то лучше бы в ней не было string, а то компилятор станет ругаться. В принципе, это хорошо, поскольку не дает нам набажить. Проверять типы совсем просто: если функция возвращает integer, а мы пытаемся вернуть в ней "Marin", то это ошибка.

Однако, с зависимыми типами все сложнее. Проблема заключается в том, когда именно компилятор проверяет типы. Как ему убедиться, что в массиве именно три значения, если программа еще даже не выполняется? Как убедиться, что целое число больше 3, если оно еще даже не присвоено? Для этого есть магия… или, иными словами, математика. Если можно математически доказать, что множество чисел всегда больше 3, то компилятор может это проверить.

Математику в студию!

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

1 + 2 + 3 + ... + x = x * (x + 1) / 2

Существует бесконечное множество возможных x, поэтому нам потребовалось бы очень длительное время, чтобы проверить все числа вручную. К счастью, это не обязательно. Нам всего лишь нужно доказать две вещи:

1. Данное утверждение соблюдается для первого числа. (Обычно это 0 или 1)
2. Если данное утверждение соблюдается для числа n, то оно будет соблюдаться и для следующего числа n + 1

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

Доказать это не составляет труда:

1 = 1 * (1 + 1) / 2
1 = 1

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

Предположив, что следующее выражение верно:

1 + 2 + 3 + ... + n = n * (n + 1) / 2

Проверим его для n + 1:

(1 + 2 + 3 + ... + n) + (n + 1) = (n + 1) * ((n + 1) + 1) / 2

Таким образом, можно заменить "(1 + 2 + 3 + ... + n)" вышеприведенным равенством:

(n * (n + 1) / 2) + (n + 1) = (n + 1) * ((n + 2) / 2)

и упростить до

(n + 1) * (n/2 + 1) = (n + 1) * (n/2 + 1)

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

Красота данного подхода заключается в том, что любое математическое доказательство можно оформить в виде компьютерной программы – а именно это нам и нужно!

Вернемся к программированию

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

Рассмотрим пример. Здесь у нас есть функция append, принимающая два массива и комбинирующая их. Как правило, сигнатура такой функции будет выглядеть примерно так:

append: (arr1: Array, arr2: Array) -> Array

Однако, просто взглянув на сигнатуру, мы не можем быть уверены в правильности реализации. Сам тот факт, что функция возвращает массив, еще не означает, что она что-то сделала. Один из способов проверить результат – убедиться, что длина результирующего массива равна сумме длин массивов параметров.

newArray = append([1], [2, 3])
assert(length(newArray) == 3)

Но зачем же проверять это во время выполнения, если можно создать ограничение, которое будет проверяться во время компиляции программы:

append: (arr1: Array, arr2: Array) -> newArray: Array
         where length(newArray) == length(arr1) + length(arr2)

Мы объявляем, что append – это функция, принимающая два аргумента Array и возвращающая новый аргумент Array, который мы назвали newArray. Лишь на сей раз мы добавляем оговорку о том, что длина нового массива должна равняться сумме длин всех аргументов функции. Утверждение, имевшееся у нас выше во время выполнения, во время компиляции преобразуется в тип.

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

Чтобы обеспечить работу такого механизма, нужно убедиться, что каждое число относится к отдельному типу. Тип One может содержать всего одно значение: 1. То же самое касается Two, Three и всех других чисел. Естественно, такая работа очень утомительна, но именно для такой работы у нас есть программирование. Можно написать компилятор, который будет делать это за нас.

Сделав это, можно создать отдельные типы для массивов, содержащих 1, 2, 3 и другое количество элементов. ArrayOfOne, ArrayOfTwo, т.д.

Таким образом, можно определить функцию length, которая станет принимать один из вышеприведенных типов массивов и иметь зависимый возвращаемый тип One для ArrayOfOne, Two для ArrayOfTwo и т.д. для каждого числа.

Теперь, когда у нас есть отдельный тип на любую конкретную длину массива, можно убедиться (во время компиляции), что оба массива имеют равную длину. Для этого сравним их типы. А поскольку типы – это такие же значения, как и любые другие, можно назначать операции над ними. Можно определить сложение двух конкретных типов, задав, что сумма ArrayOfOne и ArrayOfTwo равна ArrayOfThree.

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

Допустим, мы хотим создать переменную типа ArrayOfThree:

result: ArrayOfThree = append([1], [2, 3])

Компилятор может определить, что у [1] есть всего одно значение, поэтому можно присвоить тип ArrayOfOne. Он также может присвоить ArrayOfTwo для [2, 3].

Компилятор знает, что тип result должен быть равен сумме типов первого и второго аргумента. Он также знает, что ArrayOfOne+ ArrayOfTwo равно ArrayOfThree, то есть, знает, что все выражение в правой части тождества относится к типу ArrayOfThree. Оно совпадает с выражением в левой части, и компилятор доволен.

Если бы мы написали следующее:

result: ArrayOfTwo = append([1], [2, 3])

то компилятор был бы совершенно недоволен, поскольку ему было бы известно, что тип неверен.

Зависимая типизация – это очень круто

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

При помощи зависимых типов можно выразить практически что угодно. Функция факториала будет принимать только натуральные числа, функция login не будет принимать пустых строк, функция removeLast будет принимать только непустые массивы. Причем, все это проверяется до того, как вы запустите программу.

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

Думаю, зависимая типизация – будущее мейнстримовых языков программирования, и мне уже не терпится его дождаться!

→ Idris

→ F#

→ Добавление зависимых типов в JavaScript

Автор: ph_piter

Источник