Обзор языка Idris

Agda is too mainstream! ^[1]

«Предвидение»

(источник ^[2])

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

Итак, Idris — чистый функциональный язык программирования общего назначения с зависимыми типами.

Зачем это?

Для краткого ответа подойдёт известная цитата Дейкстры; хотя подход и изменился с тех пор, цель осталась та же:

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

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

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

Статическая типизация и зависимые типы

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

Типизация может ограничиваеться несколькими примитивными типами — например, строки, числа, числа с плавающей запятой; тогда всё, что мы можем «сказать» о типе некоторого значения (например, аргумента функции, или возвращаемого ею значения) — «строка», «число», «число с плавающей запятой». Но обычно это дополняется чем-то вроде структур: простые C-подобные структуры, классы, (обобщённые) алгебраические типы данных и пр., и заодно синонимами типов (typedef в C, type в Haskell), что уже позволяет «сказать», например, «дата», предварительно определив структуру, класс или тип «дата».

Можно дополнить это фразой «указатель на», что заодно позволяет использовать массивы, но в высокоуровневых языках чаще поддерживается обобщённое программирование ^[4] (шаблоны в C++, generics в Java), что уже позволяет строить для описания типов фразы вида «список дат», «граф дорог», «дерево событий». Другими словами, типы могут быть параметризованы другими типами.

И, наконец, можно параметризовать типы значениями, что даёт возможность сказать «список, состоящий из пяти строк», «сообщение, подписанное Василием»; типы функций тогда могут принимать вид «функция, принимающая сообщение, подписанное некоторым пользователем, и возвращающая данные этого пользователя», вместо более распространённого «функция, принимающая сообщение и возвращающая данные пользователя», что ведёт к намного более точным спецификациям. Более того, это даёт возможность, так сказать, перейти от подлежащих к сказуемым, использовать принцип «высказывания как типы»: «5 больше 3», «неверно, что 5 больше 3», «7 является простым числом», «Василий получил 2 сообщения». Это и есть зависимые типы ^[5], которые реализованы в Idris, как, впрочем, и в нескольких других языках (Agda, Coq, Epigram и т.д.), но от них Idris отличает стремление быть современным прикладным языком.

Также это, в условиях total functional programming, позволяет пользоваться соответствием между компьютерными программами и математическими доказательствами (соответствием Карри – Ховарда ^[6]): типом функции может быть, например, «А меньше Б, Б меньше В, значит А меньше В» или «сообщение отправлено некоторому пользователю, значит данному пользователю доступно данное сообщение»; доказательством тогда становится тело функции, которое просто должно вернуть значение заданного типа, а проверка доказательства — это и есть проверка типов.

Total functional programming

Как было сказано, Idris — чистый функциональный язык ^[7]. Но также поддерживается опциональное требование свойства totality функций, под которым подразумевается два свойства:

1. Определённость всюду: функция должна быть определена для любых входных данных. В чистых языках отсутствие этого свойства — едва ли не единственная возможность для программы «упасть» (другие — IO, в частности убийство процесса системой вследствие каких-то его действий, и возможные баги компилятора).
2. Строгая нормализация: при рекурсивных вызовах функции, хотя бы один из её аргументов должен строго уменьшаться (структурно), либо функция должна быть продуктивна на каждой итерации — т.е. возвращать какую-то часть результата, и обещание просчитать следующую итерацию. В первом случае это гарантирует завершаемость функции, обходя проблему остановки, а во втором — возможность считать конечный префикс любой длины за конечное время.

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

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

Примеры

Непривычный синтаксис, похоже, сильно отвлекает внимание от сути описываемого, и потому описывать синтаксис не буду; примеры кода приводятся для людей, знакомых с языками семейства ML, а для остальных приводятся текстовые описания перед этими примерами.

Деление

Знакомая всем операция, которая есть практически во всех языках программирования (или в их стандартных библиотеках) — деление. Но деление на 0 запрещено, что ведёт к различным спорным решениям:

• Вернуть что-нибудь специальное, вроде Infinity: тогда мы должны определить и правила для работы всех остальных функций/операций с Infinity, что усложняет арифметику в целом, но, например, простое свойство a / b = c → b * c = a будет утеряно, и далее попытка его использования запросто приведёт к результатам, отличным от ожидаемых.
• Породить исключение: это не только приводит к нарушению нормального потока выполнения программы, заодно опять-таки создавая почву для багов при непойманных исключениях, но и значительно затрудняет рассуждение (в частности, формальное) о функциях, если не делает его невозможным.
• Обернуть результат в Maybe ^[8], возвращая Nothing при попытке деления на 0: чем-то лучше предыдущих двух, разве что сама функция не будет стимулировать программиста писать корректные программы, а формулы могут стать менее аккуратными и/или излишне насыщенными теорией категорий, попутно затрудняя рассуждения о функциях, использующих такую реализацию деления.

В языках с зависимыми типами, и в Idris в частности, появляется ещё один вариант: запретить деление на 0. Другими словами, деление на 0 запрещено — и мы просто делаем его невозможным; тип функции тогда описывается как «функция, принимающая два числа, второе из которых не равно 0, и возвращающая число». При желании, можно дополнить эту спецификацию свойством, говорящим о связи возвращаемого значения с аргументами функции, т.е. "… такое, что...", но проще это оставить для отдельных теорем, а пока вернёмся к описанию типа функции деления: к обычным двум аргументам, нам нужно добавить третий — доказательство того, что второй аргумент не равен нулю.

Теперь рассмотрим три случая использования деления (напомню, что речь идёт о времени компиляции):

1. Делитель известен: доказательство тривиально, поскольку эквивалентность натуральных чисел разрешима (другими словами, компилятор сам видит, равен делитель нулю или нет), и потому мы можем, при желании, обернуть такую функцию деления в функцию с обычными двумя аргументами, подставляющую один и тот же простой третий аргумент.
2. Делитель неизвестен, но о нём известно что-то, что позволяет убедиться в том, что он не равен нулю: например, что он больше некоторого неотрицательного числа. Тогда нужно или написать доказательство на месте, или воспользоваться функцией, принимающей то, что у нас есть (доказательство того, что число больше некоторого неотрицательного числа), и возвращающей то, что нам нужно (доказательство того, что это число не равно нулю). Такие функции можно называть как просто функциями, так и леммами или теоремами, но, как уже было упомянуто, в данном контексте это одно и то же.
3. Мы сами не уверены в том, что делитель не будет равен нулю (после внимательного рассмотрения ситуации в попытке доказать неравенство, предыдущий случай может переходить в этот): только в этом случае нам действительно нужно ввести проверку перед делением; если делитель равен нулю, то использовать альтернативное решение, а в противном случае — воспользоваться полученной информацией и выполнить деление.

Такой подход, конечно, необязателен и в Idris, но заставляет программиста убедиться в том, что он выполняет расчёты корректно.

И, наконец, пример кода — каркас для функции деления:

-- (total) функция деления для натуральных чисел
-- "==" - функция проверки разрешимой эквивалентности, возвращающая Bool
-- "=" - эквивалентность высказываний, тип
total div : (n, m: Nat) -> ((m == Z) = False) -> Nat
-- деление на 0 - невозможно; просто показываем это компилятору
-- с тем же успехом, впрочем, можно и вернуть любое число
div n Z f = FalseElim $ trueNotFalse f
-- деление на положительное число
div n (S k) f = {-todo-}?div_rhs

Поскольку это только каркас, здесь использована мета-переменная, div_rhs; людям, знакомым с Agda, уже знакомы «дырки» (holes), более слабой версией которых мета-переменные в Idris являются, а для остальных поясню: Idris позволяет посмотреть её контекст (переменные, которые видны из её позиции) и цель (что должно быть сконструировано/возвращено из данной позиции), что заметно облегчает написание как доказательств, так и программ. Вот так он выглядит в данном случае:

  n : Nat
  k : Nat
  f : S k == 0 = False
--------------------------------------
div_rhs : Nat

Также есть возможность заполнять их полу-автоматически: имея цель вернуть Nat, можно воспользоваться командой (REPL/IDE) «refine», передав ей, например, имя функции plus, и если функция plus в состоянии вернуть значение требуемого типа, то она будет подставлена вместо этой мета-переменной, а для её аргументов будет подставлено две новых меты. Процесс это тот же, который используется и для другой функции — полностью автоматической замены мета-переменных, т.е. поиском доказательства: в некоторых случаях требуемое доказательство может быть найдено автоматически.

Типы (немного подредактированы для читабельности):

λΠ> :t div
div : Nat -> (m : Nat) -> (m == 0 = False) -> Nat

λΠ> :t div 1 2
div 1 2 : (2 == 0 = False) -> Nat

λΠ> :t div 1 2 refl
div 1 2 refl : Nat

λΠ> :t div 1 0 refl
(ошибка, программа с подобным вызовом не пройдёт проверку типов)

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

Списки

Работа со списками (или массивами) — ещё одна частая задача, приводящая примерно к тому же набору спорных решений и последующих ошибок. В частности, рассмотрим функцию, возвращающую энный элемент списка: проблема при её реализации состоит в том, что мы можем запросить элемент с позиции, которой нет в списке. Обычные решения — падать с «access violation» или «segmentation fault», порождать исключение (и, возможно, потом падать с ним), использовать Maybe.

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

Здесь можно заметить, что различные числа, списки, «if-then-else» и т.п. определяются на самом языке. Натуральные числа, реализованные в библиотеке, заменяются на GMP числа при компиляции в C, а такие функции, как сложение и умноженние — на соответствующие функции GMP, что даёт и быстрые расчёты в скомпилированных программах, и возможность рассуждать о них. Теперь взглянем на код:

data Nat = Z | S Nat
data List a = Nil | (::) a (List a)

length : List a -> Nat
length []      = 0
length (x::xs) = 1 + length xs

index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
index Z     (x::xs) p    = x
index (S n) (x::xs) p    = index n xs ?indexTailProof
index _     []      refl   impossible

indexTailProof = proof {
  intros;
  rewrite sym p;
  trivial;
}

indexTailProof — доказательство с использованием тактик, в стиле Coq, но можно (и мне чем-то больше нравится) писать их и в стиле Agda, т.е. более привычными функциями (говорят, правда, что скоро тактики будут и в Agda).

Второе решение — использовать не просто список, а список фиксированной длины: вектор, как его называют в контексте языков с зависимыми типами. Пример был упомянут выше: это то, что позволяет сказать «список из пяти строк». Также нам может помочь т.н. конечный тип — то есть тип, количество различных значений которого конечно: можем рассматривать его как тот же тип натуральных чисел, но с верхней границей. Удобен этот тип в частности тем, что с ним проще сказать «число, меньшее n», чем с натуральными числами, где это скорее «число, и оно меньше n». Тип функции получения энного элемента вектора тогда читается как «функция, принимающая число, меньшее чем n, и список из n элементов типа a, и возвращающая элемент типа a».

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

Код:

data Fin : (n : Nat) -> Type where
    fZ : Fin (S k)
    fS : Fin k -> Fin (S k)

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

index : Fin n -> Vect n a -> a
index fZ     (x::xs) = x
index (fS k) (x::xs) = index k xs
-- запросить что-либо из пустого вектора невозможно, в данном случае
-- компилятор это "видит" сам
index fZ     [] impossible

Так мы уходим ещё дальше от явных доказательств, но строим, тем не менее, корректные программы.

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

(++) : Vect m a -> Vect n a -> Vect (m + n) a
(++) []      ys = ys
(++) (x::xs) ys = x :: xs ++ ys

Тело то же, что и для обычных списков, но тип поинтереснее: обратите внимание на m + n.

Примеры побольше

Выше приведены примеры отдельных небольших функций, которые Idris помогает сделать корректными, но вот несколько более крупных вещей навскидку:

• Протоколы: есть библиотека Protocols ^[9], позволяющая описывать протоколы с использованием DSL, а затем реализовывать их; несоответствие реализации описанию протокола приведёт к ошибке.
• Физика ^[10] и игры ^[11]: не только поддерживается корректность вычислений, но и полезно доказывать теоремы уже после написания основных программ.
• Законы функторов, аппликативных функторов и монад могут быть включены в код ^[12], в сами тайпклассы.
• Криптография ^[13]: очевидный пример того, корректность чего важна.
• Разбор и составление текстовых/бинарных форматов: может быть формально доказано, что любые составленные строки разбираются в исходные данные, а разобранные данные — составляются в исходные строки. Примерно это я и выбрал в качестве первого проекта на Idris.
• Системы прав доступа, базы данных, драйверы устройств — реализаций на Idris пока не видел, но тоже вещи, которые хочется видеть надёжными.

Пишется на нём и веб-фреймворк ^[14], и библиотека для взаимодействия с DOM ^[15] (кстати, на момент написания статьи компилятор поддерживает компиляцию в C, LLVM, Java и JavaScript), и всяческие парсеры (раз ^[16], два ^[17]), и на системное программирование он нацелен. Переписываются программы с Haskell на Idris достаточно просто.

Не используется Idris пока на производстве — по крайней мере, широко (слышал, что в Potsdam Institute for Climate Impact Research он активно используется, но это, возможно, не совсем то, что обычно понимается под производством). Основная техническая преграда — «необкатанность», которая должна решиться «обкатыванием».

Заключение

Язык это новый, и потому «сырой», но современный, использующий современную теорию и накопленную другими языками практику.

Позволив себе немного помечтать о будущем использовании Idris (и языков, которые появятся после него), можно представить, помимо общего повышения надёжности программ, технические задания, сопровождаемые формальными спецификациями или даже состоящие из них; рост сервисов наподобие Proof Market ^[18]; библиотеки физических, математических, да и любых других теорий, и языков наподобие Lojban; статьи и книги как списки формальных спецификаций доказанных теорем; общение, выстраиваемое из автоматически проверяемых реплик и пар вопрос-ответ в частности.

Ссылки и книги по теме

• Официальный сайт ^[19] с документацией и ссылками;
• github wiki ^[20];
• Скринкасты ^[21] с использованием idris-mode ^[22] (есть, кстати, и idris-vim ^[23]);
• Software Foundations ^[24] — хорошее введение в языки с зависимыми типами, но использующее Coq;
• Type Theory and Functional Programming ^[25] — описание теории, лежащей в основе подобных языков;
• TaPL, книги по Haskell и документация Agda могут дополнить картину.

P.S.

Спасибо тем, на ком этот обзор тестировался, за их комментарии и идеи.

Автор: defanor

Источник ^[26]