Idris (язык программирования)
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
Функция дописывает вектор из Слово « Другой пример: попарное сложение двух векторов, параметризованных по их длине: 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
Автоматическое доказательствоЗависимые типы достаточно мощны, чтобы описать большинство свойств программ, за счёт этого программа на Idris может доказывать инварианты во время компиляции. Это превращает язык в систему интерактивного доказательства. Idris поддерживает два способа работы с системой автоматического доказательства: путём написания последовательных вызовов тактик (стиль Coq, при этом набор доступных тактик не столь богат, как в Coq, но может быть расширен штатными средствами метапрограммирования) или посредством пошаговой разработки доказательства (стиль Epigram и Agda). Примечания
Литература
Ссылки
|
||||||||||||||||||||||
Portal di Ensiklopedia Dunia
