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

Эта статья поднимает множество проблем. Пожалуйста, помогите улучшить его или обсудите эти проблемы на странице обсуждения . ( Узнайте, как и когда удалить эти сообщения-шаблоны ) Тема этой статьи может не соответствовать общему руководству Википедии о известности . Пожалуйста, помогите продемонстрировать значимость темы, цитируя надежные вторичные источники , не зависящие от темы и обеспечивающие значительное ее освещение, помимо банального упоминания. Если не удается показать известность, вероятно, статья будет объединена , перенаправлена или удалена . Найти источники:  язык программирования "Эпиграмма"  -  новости  · газеты  · книги  · научный сотрудник  · JSTOR ( август 2019 г. )( Узнайте, как и когда удалить этот шаблон сообщения ) Эта статья включает в себя список литературы , связанной литературы или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Август 2019 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

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

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

Синтаксис [ править ]

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

Примеры [ править ]

Натуральные числа [ править ]

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

 (! (! (n: Nat!данные !---------! куда !----------! ; ! -----------! ! Nat: *)! Zero: Nat)! Suc n: 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 nNatInd P mz ms ноль => mzNatInd 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:

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

Зависимые типы [ править ]

Эпиграмма - это, по сути, типизированное лямбда-исчисление с расширениями типов обобщенных алгебраических данных , за исключением двух расширений. Во-первых, типы - это первоклассные сущности типа ; типы - это произвольные выражения типа , а эквивалентность типов определяется в терминах нормальных форм типов. Во-вторых, у него есть зависимый тип функции; вместо того , где связывается в к значению , что аргумент функции (типа ) в конечном счете принимает.${\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. DOI : 10.1017 / S0956796803004829 .
• Макбрайд, Конор (2004). Прототип эпиграммы, кивок и два подмигивания (Отчет).
• Макбрайд, Конор (2004). Учебник по эпиграмме (Отчет).
• Альтенкирх, Торстен; Макбрайд, Конор; МакКинна, Джеймс (2005). Почему важны зависимые типы (Отчет).
• Чепмен, Джеймс; Альтенкирх, Торстен; Макбрайд, Конор (2006). Перезагрузка эпиграммы: автономное средство проверки типов для ETT (отчет).
• Чепмен, Джеймс; Даганд, Пьер-Эварист; Макбрайд, Конор; Моррис, Питер (2010). Нежное искусство левитации (Доклад).

Внешние ссылки [ править ]

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

Ссылки [ править ]