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

Функциональный язык программирования

Epigram — это функциональный язык программирования с зависимыми типами и интегрированной средой разработки (IDE), обычно поставляемой вместе с языком. Система типов Epigram достаточно сильна, чтобы выражать спецификации программы . Целью является поддержка плавного перехода от обычного программирования к интегрированным программам и доказательствам, корректность которых может быть проверена и сертифицирована компилятором . Эпиграмма использует соответствие Карри-Ховарда , также называемое принципом предложений как типов , и основано на интуиционистской теории типов .

Прототип Epigram был реализован Конором МакБрайдом на основе совместной работы с Джеймсом МакКинной. Его развитие продолжают группы Epigram в Ноттингеме , Дареме , Сент-Эндрюсе и Ройял Холлоуэй, Лондонский университет в Соединенном Королевстве (Великобритания). Текущая экспериментальная реализация системы Epigram находится в свободном доступе вместе с руководством пользователя, учебным пособием и некоторыми справочными материалами. Система использовалась под Linux , Windows и macOS .

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

Синтаксис

Epigram использует двумерный, естественный синтаксис стиля дедукции с версиями в LaTeX и ASCII . Вот несколько примеров из Учебника по эпиграммам :

Примеры

Натуральные числа

Следующее объявление определяет натуральные числа :

( ! ( ! ( n : Nat ! data !---------! где !----------! ; !-----------! ! Nat : * ) ! ноль : Нэт ) ! успех н : Нэт )                         

В объявлении сказано, что Natэто тип с видом * (т. е. простой тип) и двумя конструкторами: zeroи suc. Конструктор sucпринимает один Natаргумент и возвращает Nat. Это эквивалентно объявлению Haskell " data Nat = Zero | Suc Nat".

В LaTeX код отображается так:

${\displaystyle {\underline {\mathrm {data} }}\;\left({\frac {}{{\mathsf {Nat}}:\star }}\right)\;{\underline {\mathrm {where} }}\;\left({\frac {}{{\mathsf {zero}}:{\mathsf {Nat}}}}\right)\;;\;\left({\frac {n:{\mathsf {Nat}}}{{\mathsf {suc}}\ n:{\mathsf {Nat}}}}\right)}$

Обозначение горизонтальной линии можно прочитать как «предполагая, что (то, что вверху) истинно, мы можем сделать вывод, что (то, что внизу) истинно». Например, «предполагается n, что имеет тип Nat, тогда suc nимеет тип Nat». Если сверху ничего нет, то нижнее утверждение всегда истинно: « zeroимеет тип Nat(во всех случаях)».

Рекурсия по натуральным числам

${\displaystyle {\mathsf {NatInd}}:{\begin{matrix}\forall P:{\mathsf {Nat}}\rightarrow \star \Rightarrow P\ {\mathsf {zero}}\rightarrow \\(\forall n:{\mathsf {Nat}}\Rightarrow P\ n\rightarrow P\ ({\mathsf {suc}}\ n))\rightarrow \\\forall n:{\mathsf {Nat}}\Rightarrow P\ n\end{matrix}}}$

${\displaystyle {\mathsf {NatInd}}\ P\ mz\ ms\ {\mathsf {zero}}\equiv mz}$

${\displaystyle {\mathsf {NatInd}}\ P\ mz\ ms\ ({\mathsf {suc}}\ n)\equiv ms\ n\ (NatInd\ P\ mz\ ms\ n)}$

... И в ASCII:

NatInd : все P : Nat -> * => P ноль -> ( все n : Nat => P n -> P ( suc n )) -> все n : Nat => P n NatInd P mz ms ноль => mz NatInd P mz ms ( suc n ) => ms n ( NatInd P mz ms n )                                                 

Добавление

${\displaystyle {\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {rec} }}\ x\ \{}$

${\displaystyle {\mathsf {plus}}\ x\ y\Leftarrow {\underline {\mathrm {case} }}\ x\ \{}$

${\displaystyle {\mathsf {plus\ zero}}\ y\Rightarrow y}$

${\displaystyle \quad \quad {\mathsf {plus}}\ ({\mathsf {suc}}\ x)\ y\Rightarrow {\mathsf {suc}}({\mathsf {plus}}\ x\ y)\ \}\ \}}$

... И в ASCII:

плюс  x  y <= запись x { plus x y <= case x { плюс ноль y => y plus ( успех x ) y => успех ( плюс x y ) } }                          

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

Эпиграмма — это, по сути, типизированное лямбда-исчисление с обобщенными алгебраическими расширениями типов данных, за исключением двух расширений. Во-первых, типы — это сущности первого класса типа ; типы — это произвольные выражения типа , а эквивалентность типов определяется в терминах нормальных форм типов. Во-вторых, у него есть зависимый тип функции; вместо , , где привязано к значению, которое в конечном итоге принимает аргумент функции (типа ). ${\displaystyle \star }$ ${\displaystyle \star }$ ${\displaystyle P\rightarrow Q}$ ${\displaystyle \forall x:P\Rightarrow Q}$ ${\displaystyle x}$ ${\displaystyle Q}$ ${\displaystyle P}$

Полнозависимые типы, реализованные в Epigram, представляют собой мощную абстракцию. (В отличие от Dependent ML , зависимые значения могут иметь любой допустимый тип.) Пример новых возможностей формальной спецификации, которые предоставляют зависимые типы, можно найти в The Epigram Tutorial .

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

• ALF — помощник по доказательству среди предшественников Epigram.

дальнейшее чтение

• Макбрайд, Конор; Маккинна, Джеймс (2004). «Вид слева». Журнал функционального программирования . 14 : 69–111. дои : 10.1017/S0956796803004829 . S2CID  6232997.
• Макбрайд, Конор (2004). Прототип эпиграммы, кивок и два подмигивания (Отчет).
• Макбрайд, Конор (2004). Учебник по эпиграмме (Отчет).
• Альтенкирх, Торстен; Макбрайд, Конор; Маккинна, Джеймс (2005). Почему зависимые типы имеют значение (Отчет).
• Чепмен, Джеймс; Альтенкирх, Торстен; Макбрайд, Конор (2006). Epigram Reloaded: автономная проверка типов для ETT (отчет).
• Чепмен, Джеймс; Даганд, Пьер-Эварист; Макбрайд, Конор; Моррис, Питер (2010). Нежное искусство левитации (Репортаж).

Рекомендации

1. "Эпиграмма - Официальный сайт" . Проверено 28 ноября 2015 г.

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

• Официальный веб-сайт
• Эпиграмма 1 на GitHub
• Эпиграмма2 на GitHub
• EPSRC по ALF, LEGO и тому подобному; архивная версия от 2006 года