Idris — это чисто функциональный язык программирования с зависимыми типами , необязательными отложенными вычислениями и такими функциями, как проверка совокупности . Idris можно использовать в качестве помощника по доказательству , но он разработан как язык программирования общего назначения, аналогичный Haskell .
Система типов Idris аналогична системе Agda , а доказательства аналогичны системе Coq , включая тактику ( функции/процедуры доказательства теорем ) посредством отражения разработчика. [6] По сравнению с Agda и Coq, Idris отдает приоритет управлению побочными эффектами и поддержке встроенных предметно-ориентированных языков . Idris компилируется в C (полагаясь на специальный копирующий сборщик мусора с использованием алгоритма Чейни ) и JavaScript (как на основе браузера, так и на основе Node.js ). Существуют сторонние генераторы кода для других платформ, включая виртуальную машину Java (JVM), Common Intermediate Language (CIL) и LLVM . [7]
Идрис назван в честь поющего дракона из британской детской телепрограммы 1970-х годов « Паровозик Айвор» . [8]
Idris сочетает в себе ряд функций из относительно распространенных языков функционального программирования с функциями, заимствованными у помощников по доказательству .
Синтаксис Idris имеет много общего с синтаксисом Haskell. Программа hello world в Идрисе может выглядеть так:
модуль Главный main : IO ()
main = putStrLn "Привет, Мир!" Единственные различия между этой программой и ее эквивалентом на Haskell — это одиночное (вместо двойного) двоеточие в сигнатуре типа основной функции и отсутствие слова « where» в объявлении модуля . [9]
Idris поддерживает индуктивно определяемые типы данных и параметрический полиморфизм . Такие типы могут быть определены как в традиционном синтаксисе, подобном Haskell 98 :
Дерево данных a = Узел ( Дерево a ) ( Дерево a ) | Лист а или в более общем синтаксисе, подобном обобщенному алгебраическому типу данных (GADT):
Дерево данных : Тип -> Тип , где Узел : Дерево a -> Дерево a -> Дерево a Лист : a -> Дерево a При использовании зависимых типов значения могут появляться в типах; по сути, любые вычисления на уровне значений могут быть выполнены во время проверки типа . Ниже определяется тип списков, длина которых известна до запуска программы, традиционно называемых векторами :
data Vect : Nat -> Type -> Type где Nil : Vect 0 a (::) : ( x : a ) -> ( xs : Vect n a ) -> Vect ( n + 1 ) a Этот тип можно использовать следующим образом:
всего добавить : Vect n a -> Vect m a -> Vect ( n + m ) a добавить ноль ys = ys добавить ( x :: xs ) ys = x :: добавить xs ys Функция appendдобавляет вектор mэлементов типа aк вектору nэлементов типа a. Поскольку точные типы входных векторов зависят от значения, во время компиляции можно быть уверенным, что результирующий вектор будет содержать ровно ( n+ m) элементы типа a. Слово " total" вызывает средство проверки целостности , которое сообщит об ошибке, если функция не охватывает все возможные случаи или невозможно (автоматически) доказать, что она не входит в бесконечный цикл .
Другой распространенный пример — попарное сложение двух векторов, параметризованных по их длине:
общая параAdd : Num a => Vect n a -> Vect n a -> Vect n a ПараДобавить Nil Nil = Ноль
параДобавить ( x :: xs ) ( y :: ys ) = x + y :: pairAdd xs ys Numa означает, что тип a принадлежит классу типов Num . Обратите внимание, что эта функция по-прежнему успешно проверяет тип в целом, даже несмотря на то, что Nilв одном векторе и числе в другом нет совпадения регистра . Поскольку система типов может доказать, что векторы имеют одинаковую длину, мы можем быть уверены во время компиляции, что этот случай не произойдет, и нет необходимости включать этот случай в определение функции.
Зависимые типы достаточно мощны, чтобы кодировать большинство свойств программ, а программа Idris может проверять инварианты во время компиляции. Это превращает Идриса в помощника по доказательству.
Существует два стандартных способа взаимодействия с помощниками по доказательству: написание серии тактических вызовов (стиль Coq) или интерактивная разработка термина доказательства ( стиль Эпиграмма -Агда). Идрис поддерживает оба режима взаимодействия, хотя набор доступных тактик пока не такой полезный, как у Coq. [ нечеткий ]
Поскольку в Idris есть помощник по доказательству, можно написать программы Idris для передачи доказательств. Если относиться к ним наивно, такие доказательства останутся во время выполнения. Идрис стремится избежать этой ловушки, агрессивно удаляя неиспользуемые термины. [10] [11]
По умолчанию Идрис генерирует собственный код через C. Другой официально поддерживаемый бэкэнд генерирует JavaScript .
Idris 2 — это новая автономная версия языка, в которой глубоко интегрирована система линейных типов , основанная на количественной теории типов. В настоящее время он компилируется в Scheme и C. [12]