Epigram: функциональный язык программирования с зависимыми типами и IDE. Поддержка спецификаций, доказательств и верификации компилятором. Основан на теории типов.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Функциональный язык программирования
Functional programming language
Epigram — это функциональный язык программирования с зависимыми типами, а также интегрированная среда разработки (IDE), которая обычно поставляется вместе с языком. Система типов Epigram достаточно мощна, чтобы выражать спецификации программ. Цель проекта — обеспечить плавный переход от обычного программирования к интегрированным программам и доказательствам, корректность которых может быть проверена и сертифицирована компилятором. Epigram использует соответствие Карри — Ховарда, также известное как принцип «предложения как типы», и основан на интуиционистской теории типов. Прототип Epigram был разработан Конором Макбрайдом на основе совместной работы с Джеймсом Маккинной. Его разработка продолжается группой Epigram в Ноттингеме, Дареме, Сент-Эндрюсе и Royal Holloway Лондонского университета в Соединенном Королевстве (Великобритании). Текущая экспериментальная реализация системы Epigram свободно доступна вместе с руководством пользователя, учебным пособием и вспомогательными материалами. Система использовалась в операционных системах Linux, Windows и macOS. В настоящее время разработка не ведется, а версия 2, которая должна была реализовать наблюдательную теорию типов, так и не была официально выпущена, но существует в репозитории GitHub.
Epigram is a functional programming language with dependent types, and the integrated development environment (IDE) usually packaged with the language. Epigram's type system is strong enough to express program specifications. The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler. Epigram exploits the Curry–Howard correspondence, also termed the propositions as types principle, and is based on intuitionistic type theory. The Epigram prototype was implemented by Conor McBride based on joint work with James McKinna. Its development is continued by the Epigram group in Nottingham, Durham, St Andrews, and Royal Holloway, University of London in the United Kingdom (UK). The current experimental implementation of the Epigram system is freely available together with a user manual, a tutorial and some background material. The system has been used under Linux, Windows, and macOS. It is currently unmaintained, and version 2, which was intended to implement Observational Type Theory, was never officially released but exists in GitHub.
Синтаксис
Эпиграмма использует двумерный синтаксис в стиле естественной дедукции, с реализациями для LaTeX и ASCII. Вот несколько примеров из руководства по Эпиграмме:
Epigram uses a two dimensional, natural deduction style syntax, with versions in LaTeX and ASCII. Here are some examples from The Epigram Tutorial:
Рекурсия на натуральных
И в кодировке ASCII:
And in ASCII:
Добавление
И в кодировке ASCII:
And in ASCII:
Зависимые типы
Эпиграмма – это, по сути, типизированный лямбда-исчисление с обобщёнными алгебраическими расширениями типов данных, за исключением двух дополнений. Во-первых, типы являются объектами первого класса, имеющими тип ; типы – это произвольные выражения типа , а эквивалентность типов определяется через нормальные формы типов. Во-вторых, в нём используется зависимый функциональный тип; вместо , , где связано со значением, которое аргумент функции (типа ) в конечном итоге принимает. Полные зависимые типы, реализованные в Epigram, представляют собой мощную абстракцию. (В отличие от Dependent ML, значение(я), от которых зависит тип, могут быть любого допустимого типа.) Пример новых возможностей формальной спецификации, предоставляемых зависимыми типами, можно найти в руководстве по Epigram.
Epigram is essentially a typed lambda calculus with generalized algebraic data type extensions, except for two extensions. First, types are first class entities, of type ; types are arbitrary expressions of type , and type equivalence is defined in terms of the types' normal forms. Second, it has a dependent function type; instead of , , where is bound in to the value that the function's argument (of type ) eventually takes. Full dependent types, as implemented in Epigram, are a powerful abstraction. (Unlike in Dependent ML, the value(s) depended upon may be of any valid type.) A sample of the new formal specification capabilities dependent types bring may be found in The Epigram Tutorial.