Idris — функційна мова програмування загального призначення з Haskell-подібним синтаксисом і підтримкою залежних типів. Система типів подібна до системи типів мови Agda.
Підтримує засоби автоматичного доведення, порівнянні з Coq, як-от підтримка тактик, проте фокусується не на них, а позиціонується як мова програмування загального призначення. Цілі створення: «достатня» продуктивність, простота керування побічними ефектами та засоби реалізації вбудовуваних предметно-орієнтованих мов.
Реалізована на Haskell, доступна у вигляді Hackage-пакета. Сирцевий код на Idris компілюється в набір проміжних подань, а з них — у сі-код, при виконанні якого використовується копіювальний збирач сміття із застосуванням . Також офіційно реалізовано можливість компіляції в код JavaScript (також і для Node.js). Існують сторонні реалізації кодогенераторів для Java, JVM, CIL, Erlang, PHP і (з обмеженням) LLVM.
Мову названо на честь співочого дракона Ідріса з британської дитячої телепередачі 1970 року «».
Мова поєднує особливості основних популярних мов функційного програмування з можливостями, запозиченими із систем автоматичного доведення, фактично розмиваючи межу між цими двома класами мов.
Друга версія мови (випущена 2020 року, заснована на «кількісній теорії типів») суттєво відрізняється від першої: додано повноцінну підтримку , код компілюється за промовчанням у Scheme, компілятор мови написано самою мовою.
Функційне програмування Синтаксис мови (як і в Agda) близький до синтаксису мови Haskell. Програма Hello, world! на Idris виглядає так:module Main
main : IO () main = putStrLn "Hello, World!"Відмінності між цією програмою та її Haskell-еквівалентом: одинарна (замість подвійної) двокрапка в сигнатурі функції main та відсутність слова «where» в оголошенні модуля.
Як і більшість сучасних функційних мов програмування, мова підтримує рекурсивні (визначувані за індукцією) типи даних та параметричний поліморфізм. Такі типи можна визначити як у традиційному синтаксисі Haskell98:data Tree a = Node (Tree a) (Tree a) | Leaf aтак і в загальнішому GADT-синтаксисі:data Tree : Type -> Type where Node : Tree a -> Tree a -> Tree a Leaf : a -> Tree aЗа допомогою залежних типів можна на етапі перевірки типів проводити обчислення за участю значень, якими параметризируются типи. Цей код визначає список зі статично заданою довжиною, традиційно званий вектором:data Vect : Nat -> Type -> Type where Nil : Vect 0 a (::) : (x : a) -> (xs : Vect n a) -> Vect (n + 1) aЦей тип можна використовувати так:total append : Vect n a -> Vect m a -> Vect (n + m) a append Nil ys = ys append (x :: xs) ys = x :: append xs ysФункція дописує вектор із m елементів типу a до вектора з n елементів типу a. Оскільки точний тип вхідних векторів залежить від значень, визначених під час компіляції, результуючий вектор включатиме рівно (n + m) елементів типу a.
Слово «total» викликає , яка, щоб уникнути входження в нескінченний цикл, повідомить про помилку, якщо функція не охоплює всіх можливих випадків, або не може бути (автоматично) доведена.
Інший приклад: попарне додавання двох векторів, параметризованих за їх довжиною:total pairAdd : Num a => Vect n a -> Vect n a -> Vect n a pairAdd Nil Nil = Nil pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ysNum означає, що a належить до класу типів Num. Функція успішно проходить перевірку типів, випадок, коли один вектор матиме значення Nil, тоді як другий буде числом — трапитися не може. Система типів перевіряє на етапі компіляції, що довжини обох векторів збігаються. Це дає змогу спростити текст функції, яка більше не повинна обробляти цей особливий випадок.
Автоматичне доведення Залежні типи досить потужні, щоб описати більшість властивостей програм, завдяки цьому програма на Idris може доводити інваріанти під час компіляції. Це перетворює мову на систему інтерактивного доведення.
Idris підтримує два способи роботи з системою автоматичного доведення: через написання послідовних викликів тактик (стиль Coq, при цьому набір доступних тактик не настільки багатий, як у Coq, але може бути розширений штатними засобами метапрограмування) або за допомогою покрокової розробки доведення (стиль і Agda).
Примітки
Література
Посилання The Idris homepage , including documentation, frequently asked questions and examples Idris at the Hackage repository Documentation for Idris Language (tutorial, language reference, etc.)