Agda (programming language): Difference between revisions

Revision as of 13:39, 27 April 2020

Latest revision as of 21:31, 21 July 2025

(48 intermediate revisions by 37 users not shown)

Line 1:

{{shortShort description|Functional programming language}}

{{Distinguish|text = the programming language [[Ada (programming language)|Ada]]}}

{{Use dmy dates|date=September 2024}}

{{Infobox programming language

| name = Agda

| logo = Agda's official logo.svg

| logo_size = 220px

| logo alt = A stylized chicken in black lines and dots, to the left of the name “Agda”"Agda" in sans-serif test with the first letter slanted to the right.

| paradigm = [[Total functional programming|FunctionalTotal functional]]

| year = {{Start date and age|2007}} (1.0 in {{Start date and age|1999}})

| designer = Ulf Norell; Catarina Coquand (1.0)

| developer = Ulf[[Chalmers Norell;University Catarinaof Coquand (1.0)Technology]]

| yearreleased = 1.0 – {{Start date and age|20071999}} (1<br/>2.0 in– {{Start date and age|19992007}})

| latest release version = 2.6.1

| latest release dateversion = {{Start date and age|2020|03|16}}2.8.0

| latest testrelease versiondate = {{Start date and age|2025|07|05}}

| latest testpreview dateversion =

| latest releasepreview versiondate = 2.6.1

| typing = [[Strong and weak typing|strong]], [[Static typing|static]], [[Dependent typing|dependent]], [[Nominal typing|nominal]], [[Manifest typing|manifest]], [[Inferred typing|inferred]]

| implementations =

| dialects =

| influenced = [[Idris (programming language)|Idris]]

| programming language = [[Haskell (programming language)|Haskell]]

| influenced by = [[Coq (software)|Coq]], [[Epigram (programming language)|Epigram]], [[Haskell (programming language)|Haskell]]

| license = [[BSD licenses|BSD-like]]<ref>[http://code.haskell.org/Agda/LICENSE Agda license file]</ref>

| file ext = <code>.agda</code>, <code>.lagda</code>, <code>.lagda.md</code>, <code>.lagda.rst</code>, <code>.lagda.tex</code>

| operating system = [[Cross-platform software|Cross-platform]]

| website = {{URL|https://wiki.portal.chalmers.se/agda}}

}}

'''Agda''' is a [[Dependent type|dependently typed]] [[functionalFunctional programming|functional]] [[programming language]] originally developed by Ulf Norell at [[Chalmers University of Technology]] with implementation described in his PhD thesis.<ref>Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf]

</ref> The original Agda system was developed at Chalmers by Catarina Coquand in 1999.<ref>{{Cite web |url = http://ocvs.cfv.jp/Agda/index.html |title = Agda: An Interactive Proof Editor |accessdate access-date= 2014-10-20 |archive-url = https://web.archive.org/web/20111008115843/http://ocvs.cfv.jp/Agda/index.html |archive-date = 2011-10-08 |url-status = dead }}</ref> The current version, originally known asnamed Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition.

Agda is also a [[proof assistant]] based on the [[''propositions-as-types'' paradigm ([[Curry–Howard correspondence]] paradigm), but unlike [[CoqRocq]], has no separate [[Tactic (computer science)|''tactics]]'' language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as [[data type]]s, [[pattern matching]], [[Record (computer science)|records]], [[let expression]]s and modules, and a [[Haskell]]-like [[Syntax (programming languagelanguages)|Haskellsyntax]]-like syntax. The system has [[Emacs]] and, [[Atom (text editor)|Atom]], and [[VS Code]] interfaces<ref name="emacs-mode">{{cite conference |first1 last1=Coquand |first1=Catarina |last1 last2= CoquandSynek |first2 = Dan |last2 last3= SynekTakeyama |first3 = Makoto |last3 date= Takeyama2005 |title = An Emacs interface for type directed support constructing proofs and programs |conference = European Joint Conferences on Theory and Practice of Software 2005 |url = https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf |archive-url = https://web.archive.org/web/20110722063632/https://mailserver.di.unipi.it/ricerca/proceedings/ETAPS05/uitp/uitp_p05.pdf |url-status = dead |archive-date = 2011-07-22 }}</ref><ref>{{cite web |title = agda-mode on Atom |url = https://atom.io/packages/agda-mode |access-date = 7 April 2017}}</ref><ref>{{Cite web |title=agda-mode - Visual Studio Marketplace |url=https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode |access-date=2023-06-06 |website=marketplace.visualstudio.com |language=en-us}}</ref> but can also be run in [[batch processing]] mode from thea [[command -line interface]].

Agda is based on Zhaohui Luo's [[unified theory of dependent types]] (UTT),<ref>Luo, Zhaohui. ''Computation and reasoning: a type theory for computer science''. Oxford University Press, Inc., 1994.</ref> a type theory similar to [[Intuitionistic type theory|Martin-Löf type theory]].

Agda is named after the [[Swedish language|Swedish]] song "Hönan Agda", written by [[Cornelis Vreeswijk]],<ref>{{citationcite web needed|title=[Agda] origin of "Agda"? (Agda mailing list)|url=https://lists.chalmers.se/pipermail/agda/2016/008867.html |access-date=November24 October 20192020}}</ref> which is about a [[Chicken#Terminology|hen]] named Agda. This alludes to the namingname of the theorem prover [[Rocq]], which was originally named Coq after [[Thierry Coquand]].

== Features ==

Line 38 ⟶ 41:

Here is a definition of [[Peano axioms|Peano numbers]] in Agda:

<sourcesyntaxhighlight lang="agda">

data ℕ : Set where

zero : ℕ

suc : ℕ → ℕ

</syntaxhighlight>

</source>

Basically, it means that there are two ways to construct a value of type ℕ<math>\mathbb{N}</math>, representing a natural number. To begin, <code>zero</code> is a natural number, and if <code>n</code> is a natural number, then <code>suc n</code>, standing for the [[Successor function|successor]] of <code>n</code>, is a natural number too.

Here is a definition of the "less than or equal" relation between two natural numbers:

<sourcesyntaxhighlight lang="agda">

data _≤_ : ℕ → ℕ → Set where

z≤n : {n : ℕ} → zero ≤ n

s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

</syntaxhighlight>

</source>

The first constructor, <code>z≤n</code>, corresponds to the axiom that zero is less than or equal to any natural number. The second constructor, <code>s≤s</code>, corresponds to an inference rule, allowing to turn a proof of <code>n ≤ m</code> into a proof of <code>suc n ≤ suc m</code>.<ref>{{Cite web |url = https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat.agda |title = Nat from Agda standard library |accessdatewebsite=[[GitHub]] |access-date= 2014-07-20 }}</ref> So the value <code lang="agda">s≤s {zero} {suc zero} (z≤n {suc zero})</code> is a proof that one (the successor of zero), is less than or equal to two (the successor of one). The parameters provided in [[curly bracketsbracket]]s may be omitted if they can be inferred.

=== Dependently typed pattern matching ===

In core type theory, induction and recursion principles are used to prove theorems about [[inductive type]]s. In Agda, dependently typed pattern matching is used instead. For example, natural number addition can be defined like this:

<sourcesyntaxhighlight lang="agda">

add zero n = n

add (suc m) n = suc (add m n)

</syntaxhighlight>

</source>

This way of writing recursive functions/inductive proofs is more natural than applying raw induction principles. In Agda, dependently typed pattern matching is a primitive of the language; the core language lacks the induction/recursion principles that pattern matching translates to.

=== Metavariables ===

One of the distinctive features of Agda, when compared with other similar systems such as [[CoqRocq]], is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda:

<sourcesyntaxhighlight lang="agda">

add : ℕ → ℕ → ℕ

add :x ℕy →= ℕ → ℕ?

</syntaxhighlight>

add x y = ?

<code>?</code> here is a metavariable. When interacting with the system in emacsEmacs mode, it will show the user the expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics-based proof assistants such as CoqRocq.

</source>

<code>?</code> here is a metavariable. When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics-based proof assistants such as Coq.

=== Proof automation ===

Programming in pure type theory involves a lot of tedious and repetitive proofs. Although Agda has no separate tactics language, it is possible to program useful tactics within Agda itself. Typically, this works by writing an Agda function that optionally returns a proof of some property of interest. A tactic is then constructed by running this function at type-checking time, for example using the following auxiliary definitions:

<sourcesyntaxhighlight lang="agda">

data Maybe (A : Set) : Set where

Just : A → Maybe A

Nothing : Maybe A

data isJust {A : Set} : Maybe A → Set where

auto : ∀ {x} → isJust (Just x)

Tactic : ∀ {A : Set} (x : Maybe A) → isJust x → A

Tactic Nothing ()

Tactic (Just x) auto = x

</syntaxhighlight>

</source>

(The pattern <code>()</code>, called ''absurd'', matches if the type checker finds that its type is uninhabited, i.e. proves that it stands for a false proposition, typically because all possible constructors have arguments that are unavailable, i.e. they have unsatisfiable premisses. Here no value of type <code>isJust A</code> can be constructed because, in that context, no value of type <code>A</code> exists to which we could apply the constructor <code>Just</code>. The right hand side is omitted from any equation that contains absurd patterns.) Given a function <code>check-even : (n : ℕ<math>\mathbb{N}</math>) → Maybe (Even n)</code> that inputs a number and optionally returns a proof of its evenness, a tactic can then be constructed as follows:

<sourcesyntaxhighlight lang="agda">

check-even-tactic : {n : ℕ} → isJust (check-even n) → Even n

check-even-tactic {n} = Tactic (check-even n)

lemma0 : Even zero

lemma0 = check-even-tactic auto

lemma2 : Even (suc (suc zero))

lemma2 = check-even-tactic auto

</syntaxhighlight>

</source>

The actual proof of each lemma will be automatically constructed at type-checking time. If the tactic fails, type-checking will fail.

AdditionallyFurther, to write more complex tactics, Agda has support forsupports automation via [[Reflection (computerreflective programming)|reflection]] (reflection). The reflection mechanism allows one to quotequoting program fragments into –, or unquoteunquoting them from –, the [[abstract syntax tree]]. The way reflection is used is similar to the way [[Template Haskell]] works.<ref>Van Der Walt, Paul, and Wouter Swierstra. "Engineering proof by reflection in Agda." In ''Implementation and Application of Functional Languages'', pp. 157-173. Springer Berlin Heidelberg, 2013. [http://hal.inria.fr/docs/00/98/76/10/PDF/ReflectionProofs.pdf]

</ref>

Another mechanism for proof automation is proof search action in emacs[[Emacs]] mode. It enumerates possible proof terms (limited to 5 seconds), and if one of the terms fits the specification, it will be put in the meta variable where the action is invoked. This action accepts hints, e.g., which theorems and from which modules can be used, whether the action can use pattern matching, etc.<ref>[http://www.staff.science.uu.nl/~swier004/publications/2015-mpc.pdf Kokke, Pepijn, and Wouter Swierstra. "Auto in Agda."]

</ref>

=== Termination checking ===

Agda is a [[Totaltotal functional programming|total language]] language, i.e., each program in it must terminate and all possible patterns must be matched. Without this feature, the logic behind the language becomes inconsistent, and it becomes possible to prove arbitrary statements. For [[termination checking]], Agda uses the approach of the Foetus termination checker.<ref>Abel, Andreas. "foetus – Termination checker for simple functional programs." ''Programming Lab Report'' 474 (1998). [http://www.tcs.informatik.uni-muenchen.de/~abel/foetus.pdf]</ref>

[http://www.tcs.informatik.uni-muenchen.de/~abel/foetus.pdf]

</ref>

=== Standard library ===

Agda has an extensive de facto [[standard library]], which includes many useful definitions and theorems about basic data structures, such as natural numbers, lists, and vectors. The [[Library (computing)|library]] is in beta, and is under active development.

=== Unicode ===

One of the more notable features of Agda is a heavy reliance on [[Unicode]] in program source code. The standard emacsEmacs mode uses shortcuts for input, such as <code>\Sigma</code> for Σ.

=== Backends ===

Line 122 ⟶ 121:

==See also==

* [[HOLList of (proof assistant)assistants]]

* [[Coq]]

* [[Isabelle (proof assistant)]]

* [[HOL (proof assistant)]]

== References ==

{{reflist}}

==Further reading==

* {{cite web |first1=Ana |last1=Bove |first2=Peter |last2=Dybjer |first3=Ulf |last3=Norell |date=n.d.

* [|url=http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pdf A |title=Brief Overview of Agda], by– Ana Bove,A PeterFunctional Dybjer,Language andwith [[UlfDependent Norell]]Types}}

* [{{cite web |first1=Ulf |last1=Norell |first2=James |last2=Chapman |date=n.d. |url=http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf |title=Dependently Typed Programming in Agda], by [[Ulf Norell]]}}

== External links ==

* {{Official website|wiki.portal.chalmers.se/agda}}

* [https://www.youtube.com/playlist?plist=B7F836675DCE009CPLB7F836675DCE009C Introduction to Agda], a five-part YouTube playlist by Daniel Peebles

* [http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf Dependently Typed Programming in Agda], by [[Ulf Norell]]

* [http://oxij.org/note/BrutalDepTypes/ Brutal &#91;{{bracket|Meta&#93;}}Introduction to Dependent Types in Agda]

* [http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pdf A Brief Overview of Agda], by Ana Bove, Peter Dybjer, and [[Ulf Norell]]

* [httphttps://people.inf.elte.hu/divip/AgdaTutorial/IndexAbout.html Agda Tutorial: "explore programming in Agda without theoretical background"]

* [https://www.youtube.com/playlist?p=B7F836675DCE009C Introduction to Agda], a five-part YouTube playlist by Daniel Peebles

* [https://www.youtube.com/playlist?list=PLtIZ5qxwSNnzpNqfXzJjlHI9yCAzRzKtx HoTTEST Summer School 2022], 66 lectures on Homotopy Type Theory, including many introductory lectures and exercises on Agda

* [http://oxij.org/note/BrutalDepTypes/ Brutal &#91;Meta&#93;Introduction to Dependent Types in Agda]

* [http://people.inf.elte.hu/divip/AgdaTutorial/Index.html Agda Tutorial: "explore programming in Agda without theoretical background"]

{{Haskell programming}}

{{Projects at Chalmers University of Technology}}

[[Category:Programming languages]]

Line 149 ⟶ 151:

[[Category:Haskell programming language family]]

[[Category:Cross-platform free software]]

[[Category:Free compilers and interpretersopen source compilers]]

[[Category:Chalmers University of Technology]]

[[Category:Programming languages created in 2007]]

[[Category:2007 software]]

<!-- Hidden categories below -->

[[Category:Articles with example Haskell code]]