View source for Agda (programming language)

{{Short 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 alt = A stylized chicken in black lines and dots, to the left of the name "Agda" in sans-serif test with the first letter slanted to the right.
| paradigm = [[Functional programming|Functional]]
| designer = Ulf Norell; Catarina Coquand (1.0)
| developer = [[Chalmers University of Technology]]
| released = 1.0 – {{Start date and age|1999}}<br/>2.0 – {{Start date and age|2007}}
| latest release version = 2.7.0
| latest release date = {{Start date and age|2024|08|16}}
| latest preview version = 
| latest preview date = 
| 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]]
| influenced by = [[Coq (software)|Coq]], [[Epigram (programming language)|Epigram]], [[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|wiki.portal.chalmers.se/agda}}
}}
'''Agda''' is a [[Dependent type|dependently typed]] [[Functional 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/ |title=Agda: An Interactive Proof Editor |access-date=2014-10-20 |archive-url=https://web.archive.org/web/20111008115843/http://ocvs.cfv.jp/Agda/ |archive-date=2011-10-08 |url-status=dead}}</ref> The current version, originally named 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]]), but unlike [[Coq (software)|Coq]], has no separate ''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 languages)|syntax]]. The system has [[Emacs]], [[Atom (text editor)|Atom]], and [[VS Code]] interfaces<ref name="emacs-mode">{{cite conference |last1=Coquand |first1=Catarina |last2=Synek |first2=Dan |last3=Takeyama |first3=Makoto |date=2005 |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 a [[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>{{cite web |title=[Agda] origin of "Agda"? (Agda mailing list)|url=https://lists.chalmers.se/pipermail/agda/2016/008867.html |access-date=24 October 2020}}</ref> which is about a [[Chicken#Terminology|hen]] named Agda. This alludes to the name of the theorem prover [[Coq (software)|Coq]], which was named after [[Thierry Coquand]].

== Features ==

=== Inductive types ===
The main way of defining data types in Agda is via inductive data types which are similar to [[algebraic data type]]s in non-dependently typed programming languages.

Here is a definition of [[Peano axioms|Peano numbers]] in Agda:
<syntaxhighlight lang="agda">
 data ℕ : Set where
   zero : ℕ
   suc : ℕ → ℕ
</syntaxhighlight>
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:
<syntaxhighlight lang="agda">
 data _≤_ : ℕ → ℕ → Set where
   z≤n : {n : ℕ} → zero ≤ n
   s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
</syntaxhighlight>
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 |website=[[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 bracket]]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:
<syntaxhighlight lang="agda">
 add zero n = n
 add (suc m) n = suc (add m n)
</syntaxhighlight>
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 [[Coq (software)|Coq]], is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda:
<syntaxhighlight lang="agda">

 add : ℕ → ℕ → ℕ
 add x y = ?
</syntaxhighlight>
<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. 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:
<syntaxhighlight 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>

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:

<syntaxhighlight 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>

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

Further, to write more complex tactics, Agda supports automation via [[reflective programming]] (reflection). The reflection mechanism allows quoting program fragments into, or unquoting 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]] 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 [[total functional programming]] 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>

=== 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 emacs mode uses shortcuts for input, such as <code>\Sigma</code> for Σ.

=== Backends ===
There are two compiler backends, MAlonzo for Haskell and one for [[JavaScript]].

==See also==
* [[List of proof assistants]]

== 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 |title=Brief Overview of Agda – A Functional Language with Dependent 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}}

== External links ==
* {{Official website|wiki.portal.chalmers.se/agda}}
* [https://www.youtube.com/playlist?list=PLB7F836675DCE009C Introduction to Agda], a five-part YouTube playlist by Daniel Peebles
* [http://oxij.org/note/BrutalDepTypes/ Brutal {{bracket|Meta}}Introduction to Dependent Types in Agda]
* [https://people.inf.elte.hu/divip/AgdaTutorial/About.html Agda Tutorial: "explore programming in Agda without theoretical background"]
* [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

{{Haskell programming}}
{{Chalmers University of Technology}}

[[Category:Programming languages]]
[[Category:Dependently typed languages]]
[[Category:Functional languages]]
[[Category:Pattern matching programming languages]]
[[Category:Academic programming languages]]
[[Category:Statically typed programming languages]]
[[Category:Proof assistants]]
[[Category:Free software programmed in Haskell]]
[[Category:Haskell programming language family]]
[[Category:Cross-platform free software]]
[[Category:Free compilers and interpreters]]
[[Category:Chalmers University of Technology]]
[[Category:Programming languages created in 2007]]
[[Category:2007 software]]
<!-- Hidden categories below -->
[[Category:Articles with example Haskell code]]