Эпиграмма (язык программирования)
-
Обзор Epigram
- Epigram — функциональный язык программирования с зависимыми типами и интегрированной средой разработки.
- Система типов Epigram надежна для спецификации программ.
- Цель — плавный переход от обычного программирования к интегрированным программам с возможностью проверки корректности компилятором.
-
Особенности и развитие
- Epigram использует соответствие Карри-Говарда и основана на интуиционистской теории типов.
- Прототип создан Конором Макбрайдом, разработка продолжается в нескольких университетах Великобритании.
- Текущая экспериментальная версия доступна с руководством пользователя и учебными материалами.
-
Синтаксис и примеры
- Epigram использует двумерный синтаксис с версиями в LaTeX и ASCII.
- Примеры включают натуральные числа, рекурсию по естественным признакам и дополнение.
-
Зависимые типы
- Epigram представляет собой типизированное лямбда-исчисление с расширенными типами данных.
- Типы являются первоклассными сущностями, а зависимые типы функций позволяют связывать значения с аргументами.
-
Дополнительные ресурсы
- Ссылки на официальный веб-сайт, экспериментальные версии на GitHub и предыдущие версии ALF.
Полный текст статьи: