Идрис (язык программирования)
 |
| Парадигма | Функциональный |
|---|---|
| Разработано | Эдвин Брэди |
| Впервые появился | 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 в Идрисе может выглядеть так:
модуль Main
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
параДобавить Ноль Ноль = Ноль
параДобавить ( x :: xs ) ( y :: ys ) = x + y :: параДобавить 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 г.
- ^ Перейти обратно: а б «Типы уникальности» . Идрис 1.3.1 Документация . Проверено 26 сентября 2019 г.
- ^ Перейти обратно: а б с «Идрис, язык с зависимыми типами» . Проверено 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 года
- Языки программирования сопоставления шаблонов