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

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

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

Идрис назван в честь поющего дракона из детской телепрограммы Великобритании 1970-х годов. Ivor the Engine.

• 1 Функции
  • 1.1 Функциональное программирование
  • 1.2 Индуктивные и параметрические типы данных
  • 1.3 Зависимые типы
  • 1.4 Функции помощника по проверке подлинности
  • 1.5 Генерация кода
• 2 Idris 2
• 3 См. Также
• 4 Ссылки
• 5 Внешние ссылки

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

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

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

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

Единственные различия между этой программой и ее эквивалентом Haskell - это одинарное (вместо двойного) двоеточие в сигнатуре типа основной функции и пропуск слова " где "в объявлении модуля.

Индуктивные и параметрические типы данных

Идрис поддерживает индуктивно определенные типы данных и параметрический полиморфизм. Такие типы могут быть определены как в традиционном синтаксисе, подобном «Haskell98 »:

Дерево данных a = Узел (Дерево a) (Дерево a) | Leaf

или в более общем синтаксисе, подобном GADT :

Data Tree: Type ->Type, где Node: Tree a ->Tree a ->Tree a Leaf: a ->Tree a

Зависимые типы

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

data Vect: Nat ->Type ->Type, где Nil: Vect 0 a (: :): (x: a) ->(xs: Vect na) ->Vect (n + 1) a

Этот тип может использоваться следующим образом:

total append: Vect na ->Vect ma ->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 na ->Vect na ->Vect na pairAdd Nil Nil = Nil pairAdd (x: : xs) (y :: ys) = x + y :: pairAdd xs ys

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

Функции помощника по доказательству

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

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

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

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

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

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

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

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