Главная » Хабрахабр » [Перевод] Зависимые типы — будущее языков программирования

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

Всем привет!

В конце поста помещаем три ссылки от автора, позволяющие познакомиться с зависимой типизацией в 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 и всех других чисел. Можно написать компилятор, который будет делать это за нас.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

→ Idris

→ F#

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


Оставить комментарий

Ваш email нигде не будет показан
Обязательные для заполнения поля помечены *

*

x

Ещё Hi-Tech Интересное!

Вырастить и научить. Как мы подружились с PEGA

В группе компаний ЛАНИТ работают более десяти тысяч человек. Кажется, что в таком коллективе всегда найдётся подходящий специалист. Однако с каждым годом на рынке появляется всё больше новых продуктов, методик, решений. ИТ-профессионалам интересны новинки отрасли, но для того, чтобы изучить ...

В ЕС добиваются права на ремонт крупной бытовой техники

Источник: Schraube locker!? Им удалось собрать более 100 тыс. Европейские активисты движения «права на ремонт» решили начать с холодильников. подписей под соответствующим документом и даже добиться голосования в Брюсселе по поводу изменения законодательства, имеющего отношение к ремонту бытовой техники. Традиционная ...