Rstykt

Agda — чистый функциональный язык программирования с зависимыми типами, то есть типами, которые могут быть индексированы значениями другого типа. Теоретической основой Agda служит интуиционистская теория типов Мартин-Лёфа (англ.), которая расширена набором конструкций, полезных для практического программирования.

Agda также является системой автоматического доказательства. Логические высказывания записываются как типы, а доказательствами являются программы соответствующего типа.

Agda поддерживает индуктивные типы данных, сопоставление с образцом (гибко использующее наличие
зависимых типов), систему параметризованных модулей, проверку завершаемости программ (англ.)русск., миксфиксный синтаксис для операторов. Поддержка неявных аргументов приводит к существенному упрощению программирования с зависимыми типами. Для программ на Agda характерно широкое использование Юникода.

В стандартную реализацию Agda входит расширение редактора Emacs, позволяющее осуществлять пошаговое построение программ. Система проверки типов языка дает программисту полезную информацию о ещё не написанных частях программы.

Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована.

Примеры |

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

data Nat : Set where

  zero : Nat

  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat

zero  + m = m

suc n + m = suc (n + m)

Пример зависимого типа: список, в типе которого хранится натуральное число — его длина

data Vec (A : Set) : Nat -> Set where

     : Vec A zero

  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

Безопасная функция вычисления головы списка, не позволяющая выполнять эту операцию над пустым списком (нулевой длины):

head : {A : Set}{n : Nat} -> Vec A (suc n) -> A

head (x :: xs) = x

Примечания |

Ссылки |

• 
  официальный сайт Agda (англ.)
  


• 
  Dependently Typed Programming in Agda (англ.) — подробное введение в язык


• 
  A Brief Overview of Agda (англ.) — краткий обзор языка


• 
  Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis (англ.) — диссертация автора языка

Это заготовка статьи о компьютерных языках. Вы можете помочь проекту, дополнив её.

Для улучшения этой статьи по информационным технологиям желательно: Проставив сноски, внести более точные указания на источники.