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

Эпиграмма

Парадигма	Функциональный
Разработано	Конор МакБрайд Джеймс МакКинна
Разработчик	Неподдерживаемый
Впервые появился	2004 г ( 2004 )
Стабильная версия	1 / 11 октября 2006 г ( 11.10.2006 )
Дисциплина набора текста	сильный , статичный , зависимый
ТЫ	Кроссплатформенность : Linux , Windows , macOS.
Лицензия	С
Веб-сайт	сеть .архив .org /веб /20120717070845 /http: //www .e-свинья .org /даркс /Pig09 /веб /
Под влиянием
Альф
Под влиянием
Агда , Идрис

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

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

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

Синтаксис

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

Примеры

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

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

(         !       (          !   (  n : Nat  !
data !---------! where !----------! ; !-----------!
     ! Nat : * )       !zero : Nat)   !suc n : Nat)

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

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

${\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 (во всех случаях)».

Рекурсия в натуральных числах

${\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}}$

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

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

... И в ASCII:

NatInd : all P : Nat -> * => P zero ->
         (all n : Nat => P n -> P (suc n)) ->
         all n : Nat => P n
NatInd P mz ms zero => mz
NatInd P mz ms (suc n) => ms n (NatInd P mz ms n)

Дополнение

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

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

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

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

... И в ASCII:

plus x y <= rec x {
  plus x y <= case x {
    plus zero y => y
    plus (suc x) y => suc (plus x y)
  }
}

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

Эпиграмма — это, по сути, типизированное лямбда-исчисление с обобщенными алгебраическими расширениями типов данных, за исключением двух расширений. Во-первых, типы — это сущности первого класса типа $\star$; типы — это произвольные выражения типа $\star$, а эквивалентность типов определяется в терминах нормальных форм типов. Во-вторых, у него есть зависимый тип функции; вместо $P\rightarrow Q$, $\forall x:P\Rightarrow Q$, где $x$ связан в $Q$ значению, которое аргумент функции (типа $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 на GitHub
• Эпиграмма2 на GitHub
• EPSRC по ALF, LEGO и тому подобному; архивная версия от 2006 года