Идрис (язык программирования)
 |
| Парадигма | Функциональный |
|---|---|
| Разработано | Эдвин Брэди |
| Впервые появился | 2007 г [1] |
| Стабильная версия | 1.3.4 [2]
/ 22 октября 2021 г |
| Предварительный выпуск | 0.7.0 (Идрис 2) [3]
/ 22 декабря 2023 г |
| Дисциплина набора текста | Предполагаемый , статичный , сильный |
| ТЫ | Кросс-платформенный |
| Лицензия | БСД |
| Расширения имен файлов | .idr, .lidr |
| Веб-сайт | просто идрис |
| Под влиянием | |
| Пригласить , Очистить , [4] Кок , [5] Эпиграмма , F# , Haskell , [5] МЛ , [5] Ржавчина [4] | |
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 в Идрисе может выглядеть так:
module Main
main : IO ()
main = putStrLn "Hello, World!"
Единственные различия между этой программой и ее эквивалентом на Haskell - это одиночное (вместо двойного) двоеточие в сигнатуре типа основной функции и отсутствие слова " where" в объявлении модуля . [9]
Индуктивные и параметрические типы данных
Idris поддерживает индуктивно определяемые типы данных и параметрический полиморфизм . Такие типы могут быть определены как в традиционном синтаксисе, подобном Haskell 98 :
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
Функция append добавляет вектор 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 означает, что тип a принадлежит классу типов Num. Обратите внимание, что эта функция по-прежнему успешно проверяет тип в целом, даже несмотря на отсутствие сопоставления регистра. Nil в одном векторе и число в другом. Поскольку система типов может доказать, что векторы имеют одинаковую длину, мы можем быть уверены во время компиляции, что этот случай не произойдет, и нет необходимости включать этот случай в определение функции.
Функции помощника по проверке доказательств [ править ]
Зависимые типы достаточно мощны, чтобы кодировать большинство свойств программ, а программа Idris может проверять инварианты во время компиляции. Это превращает Идриса в помощника по доказательству.
Существует два стандартных способа взаимодействия с помощниками по доказательству: путем написания серии тактических вызовов (стиль Coq) или интерактивной разработки термина доказательства ( стиль Эпиграмма -Агда). Идрис поддерживает оба режима взаимодействия, хотя набор доступных тактик пока не такой полезный, как у Coq. [ нечеткий ]
Генерация кода [ править ]
Поскольку в Idris есть помощник по доказательству, можно написать программы Idris для передачи доказательств. Если относиться к ним наивно, такие доказательства останутся во время выполнения. Идрис стремится избежать этой ловушки, агрессивно удаляя неиспользуемые термины. [10] [11]
По умолчанию Идрис генерирует собственный код C. через Другой официально поддерживаемый бэкэнд генерирует JavaScript .
Идрис 2 [ править ]
Idris 2 — это новая самостоятельная версия языка, в которой глубоко интегрирована система линейных типов , основанная на количественной теории типов . время он компилируется в Scheme и C. В настоящее [12]
См. также [ править ]
Ссылки [ править ]
- ^ Брэди, Эдвин (12 декабря 2007 г.). «Индекс /~eb/darcs/Idris» . Сент-Эндрюсского университета Школа компьютерных наук . Архивировано из оригинала 20 марта 2008 г.
- ^ «Выпуск 1.3.4» . Гитхаб . Проверено 31 декабря 2022 г.
- ^ «Выпущена версия Idris 2 0.7.0» . Гитхаб . Проверено 20 апреля 2024 г.
- ^ Jump up to: Перейти обратно: а б «Типы уникальности» . Идрис 1.3.1 Документация . Проверено 26 сентября 2019 г.
- ^ Jump up to: Перейти обратно: а б с «Идрис, язык с зависимыми типами» . Проверено 26 октября 2014 г.
- ^ «Размышление разработчика — документация Idris 1.3.2» . Проверено 27 апреля 2020 г.
- ^ «Цели генерации кода — последняя документация Идриса» . docs.idris-lang.org .
- ^ «Часто задаваемые вопросы» . Проверено 19 июля 2015 г.
- ^ «Руководство по синтаксису — документация Idris 1.3.2» . Проверено 27 апреля 2020 г.
- ^ «Анализ стирания по использованию — последняя документация Idris» . idris.readthedocs.org .
- ^ «Результаты сравнительного анализа» . ziman.functor.sk .
- ^ "идрис-ланг/Идрис2" . Гитхаб . Проверено 11 апреля 2021 г.
Внешние ссылки [ править ]
- Официальный сайт , документация, часто задаваемые вопросы, примеры
- Идрис в репозитории Hackage
- Документация по языку Idris (руководство, справочник по языку и т. д.)
на Хаскеле Программирование |
|---|
- Зависимо типизированные языки
- Экспериментальные языки программирования
- Функциональные языки
- Бесплатное программное обеспечение, написанное на Haskell.
- Семейство языков программирования Haskell
- Кроссплатформенное бесплатное программное обеспечение
- Бесплатные компиляторы и интерпретаторы
- Программное обеспечение, использующее лицензию BSD
- Языки программирования, созданные в 2007 году.
- Языки программирования высокого уровня
- программное обеспечение 2007 года
- Языки программирования сопоставления шаблонов