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

Эпиграмма

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

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 код отображается так:

${\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   :   все   P   :   Nat   ->   *   =>   P   ноль   -> 
          (  все   n   :   Nat   = >   P   n   ->   P   (  suc   n  )   -> 
          все   n   :   Nat   =>   P   n 
  NatInd   P   mz   мс   ноль   =>   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:

плюс   x   y   <=   запись   x   { 
   plus   x   y   <=   case   x   { 
     плюс   ноль   y   =>   y 
      плюс   (  успех   x  )   y   =>   успех   (  плюс   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 года