|
Agda
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
Ссылки
|
|||||||||||||||||||||||||||||||||||||
Portal di Ensiklopedia Dunia
