Идрис (язык программирования) - Idris (programming language)

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

Система типов Idris подобна системе типов Agda , а доказательства аналогичны системе типов Coq , включая тактику ( функции / процедуры доказательства теорем ) через рефлексию разработчика. По сравнению с Agda и Coq, Idris отдает приоритет управлению побочными эффектами и поддержке встроенных предметно-ориентированных языков . Idris компилируется в C (полагаясь на настраиваемый копирующий сборщик мусора с использованием алгоритма Чейни ) и JavaScript (как на основе браузера, так и на основе Node.js ). Существуют сторонние генераторы кода для других платформ, включая JVM , CIL и LLVM .

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

Функции

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

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

Синтаксис Idris имеет много общего с синтаксисом Haskell. Программа hello world в Идрисе может выглядеть так:

module Main

main : IO ()
main = putStrLn "Hello, World!"

Единственные различия между этой программой и ее эквивалентом в Haskell - это одинарное (вместо двойного) двоеточие в сигнатуре типа основной функции и отсутствие слова « 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

Функция 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

Numa означает, что тип a принадлежит к классу типов Num . Обратите внимание, что эта функция по-прежнему успешно проверяет тип как итог, даже если Nilв одном векторе нет совпадения регистра, а в другом - числа. Поскольку система типов может доказать, что векторы имеют одинаковую длину, мы можем быть уверены, что во время компиляции такой случай не произойдет, и нет необходимости включать этот случай в определение функции.

Функции Proof Assistant

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

Есть два стандартных способа взаимодействия с помощниками доказательства: путем написания серии тактических вызовов (стиль Coq) или путем интерактивной разработки термина доказательства ( стиль Epigram / Agda). Идрис поддерживает оба режима взаимодействия, хотя набор доступных тактик пока не так полезен, как у Coq.

Генерация кода

Поскольку в Идрисе есть помощник по доказательствам, программы Идриса могут быть написаны так, чтобы передавать доказательства. Если к ним относиться наивно, такие доказательства остаются во время выполнения. Идрис стремится избежать этой ловушки, агрессивно стирая неиспользуемые термины.

По умолчанию, Идрис генерирует машинный код через C . Другой официально поддерживаемый бэкэнд генерирует JavaScript .

Идрис 2

Idris 2 - это новая автономная версия языка, которая глубоко интегрирует систему линейных типов , основанную на количественной теории типов . В настоящее время она составляет в схему и C .

Смотрите также

• Полное функциональное программирование

использованная литература

внешние ссылки

• Домашняя страница Idris , включая документацию, часто задаваемые вопросы и примеры
• Идрис в репозитории Hackage
• Документация по языку Idris (учебник, справочник по языку и т. Д.)