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

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

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

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

• 1 Синтаксис
  • 1.1 Примеры
    • 1.1.1 Натуральные числа
    • 1.1.2 Рекурсия по натуральным числам
    • 1.1.3 Сложение
• 2 Зависимые типы
• 3 См. Также
• 4 Дополнительная литература
• 5 Внешние ссылки
• 6 Ссылки

Эпиграмма использует двумерный синтаксис в стиле естественного вывода с версиями в LaTeX и ASCII. Вот несколько примеров из The Epigram Tutorial:

Примеры

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

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

(! (! (N : Nat! Data! ---------! Где! ----------!;! -----------!! Nat: *)! Zero: Nat)! Suc n: Nat)

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

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

$d\; a\; t\; a\; \_\; (N\; a\; t:\; \star )\; w\; h\; e\; r\; e\; \_\; (z\; e\; r\; o:\; N\; a\; t);\; (n:\; N\; atsucn:\; N\; at)\; \{\backslash \; displaystyle\; \{\backslash \; underline\; \{\backslash \; mathrm\; \{data\}\}\}\; \backslash ;\; \backslash \; left\; (\{\backslash \; frac\; \{\}\; \{\{\backslash \; mathsf\; \{Nat\}\}:\; \backslash \; star\}\}\; \backslash \; right)\; \backslash \; ;\; \{\backslash \; underline\; \{\backslash \; mathrm\; \{where\}\}\}\; \backslash ;\; \backslash \; left\; (\{\backslash \; frac\; \{\}\; \{\{\backslash \; mathsf\; \{zero\}\}:\; \{\backslash \; mathsf\; \{Nat\}\}\}\}\; \backslash \; right)\; \backslash \; ;;\; \backslash ;\; \backslash \; left\; (\{\backslash \; frac\; \{n:\; \{\backslash \; mathsf\; \{Nat\}\}\}\; \{\{\backslash \; mathsf\; \{success\}\}\; \backslash \; n:\; \{\backslash \; mathsf\; \{Nat\}\}\}\}\; \backslash \; right)\}$

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

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

$N\; на\; I\; nd:\; \forall \; P:\; N\; at\; \to \; \star \; \Rightarrow \; P\; zero\; \to \; (\forall \; n:\; N\; at\; \Rightarrow \; P\; n\; \to \; P\; (sucn))\; \to \; \forall \; n:\; N\; at\; \Rightarrow \; P\; n\; \{\backslash \; displaystyle\; \{\backslash \; mathsf\; \{NatInd\}\}:\; \{\backslash \; begin\; \{matrix\}\; \backslash \; forall\; P:\; \{\backslash \; mathsf\; \{Nat\}\}\; \backslash \; rightarrow\; \backslash \; star\; \backslash \; Rightarrow\; P\; \backslash \; \{\backslash \; mathsf\; \{zero\}\}\; \backslash \; rightarrow\; \backslash \backslash \; (\; \backslash \; forall\; n:\; \{\backslash \; mathsf\; \{Nat\}\}\; \backslash \; Rightarrow\; P\; \backslash \; n\; \backslash \; rightarrow\; P\; \backslash \; (\{\backslash \; mathsf\; \{su\}\}\; \backslash \; n))\; \backslash \; rightarrow\; \backslash \backslash \backslash \; forall\; n:\; \{\backslash \; mathsf\; \{Nat\}\}\; \backslash \; Rightarrow\; P\; \backslash \; n\; \backslash \; end\; \{matrix\}\}\}$

$N\; в\; точке\; I\; nd\; P\; mzmszero\; \equiv \; mz\; \{\backslash \; displaystyle\; \{\backslash \; mathsf\; \{NatInd\}\}\; \backslash \; P\; \backslash \; mz\; \backslash \; ms\; \backslash \; \{\backslash \; mathsf\; \{zero\}\}\; \backslash \; Equiv\; mz\}$

$N\; при\; I\; nd\; P\; mzms\; (sucn)\; \equiv \; msn\; (N\; at\; I\; nd\; P\; mzmsn)\; \{\backslash \; displaystyle\; \{\backslash \; mathsf\; \{NatInd\}\}\; \backslash \; P\; \backslash \; mz\; \backslash \; ms\; \backslash \; (\{\backslash \; mathsf\; \{su\}\}\; \backslash \; n)\; \backslash \; эквив\; ms\; \backslash \; n\; \backslash \; (NatInd\; \backslash \; P\; \backslash \; mz\; \backslash \; ms\; \backslash \; n)\}$

... И в ASCII:

NatInd: все P: Nat ->* =>P ноль ->(все 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)

Сложение

$plusxy\; \Leftarrow \; rec\; \_\; x\; \{\{\backslash \; displaystyle\; \{\backslash \; mathsf\; \{plus\}\}\; \backslash \; x\; \backslash \; y\; \backslash \; Left\; стрелка\; \{\backslash \; underline\; \{\backslash \; mathrm\; \{rec\}\}\}\; \backslash \; x\; \backslash \; \backslash \; \{\}$

$plusxy\; \Leftarrow \; case\; \_\; x\; \{\{\backslash \; displaystyle\; \{\backslash \; mathsf\; \{plus\}\}\; \backslash \; x\; \backslash \; y\; \backslash \; Leftarrow\; \{\backslash \; underline\; \{\backslash \; mathrm\; \{\; case\}\}\}\; \backslash \; x\; \backslash \; \backslash \; \{\}$

$pluszeroy\; \Rightarrow \; y\; \{\backslash \; displaystyle\; \{\backslash \; mathsf\; \{plus\; \backslash \; zero\}\}\; \backslash \; y\; \backslash \; Rightarrow\; y\}$

$plus\; (suxx)\; y\; \Rightarrow \; success\; (plusxy)\}\}\; \{\; \backslash \; Displaystyle\; \backslash \; quad\; \backslash \; quad\; \{\backslash \; mathsf\; \{плюс\}\}\; \backslash \; (\{\backslash \; mathsf\; \{suc\}\}\; \backslash \; x)\; \backslash \; y\; \backslash \; Rightarrow\; \{\backslash \; mathsf\; \{suc\}\}\; (\{\backslash \; mathsf\; \{plus\}\}\; \backslash \; x\; \backslash \; y)\; \backslash \; \backslash \}\; \backslash \; \backslash \}\}$

... И в ASCII:

плюс xy <= rec x { plus x y <= case x { plus zero y =>y plus (success x) y =>success (плюс xy)}}

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

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

• ALF, помощник по проверке среди предшественников Epigram.

• McBride, Conor; МакКинна, Джеймс (2004). «Вид слева». Журнал функционального программирования.
• Макбрайд, Конор (2004). Прототип эпиграммы, кивок и два подмигивания (Отчет).
• МакБрайд, Конор (2004). Учебное пособие по эпиграммам (Отчет).
• Альтенкирх, Торстен; Макбрайд, Конор; МакКинна, Джеймс (2005). Почему зависимые типы имеют значение (отчет).
• Чепмен, Джеймс; Альтенкирх, Торстен; Макбрайд, Конор (2006). «Перезагрузка эпиграммы»: автономное средство проверки типов для ETT (отчет).
• Чепмен, Джеймс; Даганд, Пьер-Эварист; Макбрайд, Конор; Моррис, Питер (2010). Мягкое искусство левитации (Отчет).

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