19-10-2023
Класс языка: | |
---|---|
Автор(ы): | |
Релиз: | |
Типизация данных: | |
Испытал влияние: | |
Сайт: |
Agda wiki |
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
Это заготовка статьи о компьютерных языках. Вы можете помочь проекту, исправив и дополнив её. |
Основные языки программирования (сравнение • IDE • история • хронология) | |
---|---|
Используемые в разработке |
Ада • APL • Язык ассемблера • ActionScript • ABAP/4 • AutoIt • AWK • Бейсик • Си • Кобол • C++ • C# • Cω • Clarion • Clojure • ColdFusion • Common Lisp • D • dBase • Delphi • Eiffel • Erlang • Euphoria • F# • Форт • Фортран • Gambas • Go • Groovy • HAL/S • Haskell • Icon • Java • JavaScript • Limbo • Lua • Модула-3 • Object Pascal • Objective-C • OCaml • Oz • Parser • Паскаль • Компонентный Паскаль • Perl • PHP • PowerBASIC • Python • ПЛ/1 • Пролог • Ruby • Scala • Scheme • Smalltalk • SQL • PL/SQL • Tcl • Vala • Visual Basic (.NET) |
Академические | |
IEC 61131-3 |
Instruction List • ST • FBD • Ladder Diagram (LD) • SFC |
Прочие | |
Эзотерические | |
Визуальные |
Agda.