Idris (язык программирования)

У этого термина существуют и другие значения, см. Idris.
Idris
Изображение логотипа
Класс языка Функциональный
Появился в 2007[3][4][…]
Автор Эдвин Брейди
Расширение файлов .idr или .lidr
Выпуск Idris 2 version 0.5.1[1] (сентябрь 20, 2021 (2021-09-20))
Система типов строгая, статическая, с поддержкой зависимых типов
Испытал влияние Agda, Coq,[2] Epigram[англ.], Haskell,[2] ML,[2] Rust
Лицензия BSD-3
Сайт idris-lang.org

Idris — чистый тотальный[англ.] функциональный язык программирования общего назначения с Haskell-подобным синтаксисом и поддержкой зависимых типов[5]. Система типов подобна системе типов языка Agda.

Язык поддерживает средства автоматического доказательства, сравнимые с Coq, включая поддержку тактик, однако фокусируется не на них, а позиционируется как язык программирования общего назначения. Цели его создания: «достаточная» производительность, простота управления побочными эффектами и средства реализации встраиваемых предметно-ориентированных языков.

Реализован на Haskell, доступен в виде Hackage-пакета[6]. Исходный код на Idris компилируется в набор промежуточных представлений[7], а из них — в си-код, при исполнении которого используется копирующий сборщик мусора с применением алгоритма Чейни[англ.]. Также официально реализована возможность компиляции в код на JavaScript (в том числе для Node.js). Существуют сторонние реализации кодогенераторов для Java, JVM, CIL, Erlang, PHP и (с ограничением) LLVM.

Язык назван в честь поющего дракона Идриса из британской детской телепередачи 1970 года «Паровозик Айвор»[англ.][8].

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

Вторая версия языка (выпущенная в 2020 году, основанная на «количественной теории типов»[9]) существенно отличается от первой: добавлена полноценная поддержка линейных типов[англ.], код компилируется по умолчанию в Scheme, компилятор языка написан на самом языке.

Функциональное программирование

[править | править код]

Синтаксис языка (как и у Agda) близок к синтаксису языка Haskell[10]. Программа 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 ys

Num означает, что тип a принадлежит к классу типов Num. Функция успешно проходит проверку типов, случай, когда один векторов будет иметь значение Nil, тогда как второй будет числом — произойти не может. Система типов проверяет на этапе компиляции что длина обоих векторов будет совпадать. Это позволяет упростить текст функции, от которой больше не требуется обрабатывать этот особый случай.

Автоматическое доказательство

[править | править код]

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

Idris поддерживает два способа работы с системой автоматического доказательства: путём написания последовательных вызовов тактик (стиль Coq, при этом набор доступных тактик не столь богат, как в Coq, но может быть расширен штатными средствами метапрограммирования) или посредством пошаговой разработки доказательства (стиль Epigram и Agda).

Примечания

[править | править код]
  1. ↑ "Release 0.5.1". Архивировано 1 апреля 2022. Дата обращения: 1 апреля 2022.
  2. ↑ 1 2 3 Idris, a language with dependent types. Дата обращения: 26 октября 2014. Архивировано 11 мая 2021 года.
  3. ↑ https://web.archive.org/web/20080320233322/http://www-fp.cs.st-and.ac.uk/~eb/darcs/Idris/
  4. ↑ https://web.archive.org/web/20080322004024/http://www.cs.st-andrews.ac.uk:80/~eb/
  5. ↑ Mena, 2014, Ch 1. Going Functional § Why Strong Static Typing?, p. 5.
  6. ↑ Mena, 2014, Ch. 13. Strong Types for Describing Offers § Introducing Idris, p. 305.
  7. ↑ Cross-platform Compilers for Functional Languages. Дата обращения: 18 мая 2017. Архивировано 14 мая 2015 года.
  8. ↑ Frequently Asked Questions. Дата обращения: 19 июля 2015. Архивировано 21 июля 2015 года.
  9. ↑ The Syntax and Semantics of Quantitative Type Theory. Дата обращения: 25 мая 2020. Архивировано 9 ноября 2020 года.
  10. ↑ Mena, 2014, Ch. 13. Strong Types for Describing Offers § Dependent Typing, p. 304.

Литература

[править | править код]
  • Alejandro Serrano Mena. Ch. 13. Strong Types for Describing Offers. // Beginning Haskell. A Project-Based Approach. — Apress, 2014. — 402 с. — ISBN 978-1-4302-6250-3.
  • Bruce Tate, Fred Daoud, Jack Moffitt, Ian Dees. Idris // Seven More Languages in Seven Weeks. Languages That Are Shaping the Future. — The Pragmatic Bookshelf, 2014. — С. 243—275. — 319 с. — ISBN 978-1-94122-215-7.
  • Edwin Brady. Type-Driven Development with Idris. — Manning Publications, 2017. — 480 с. — ISBN 9781617293023.

Ссылки

[править | править код]