Agda (programming language): Difference between revisions

Revision as of 15:21, 17 March 2025

Latest revision as of 21:31, 21 July 2025

(8 intermediate revisions by 5 users not shown)

Line 11:

| 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.78.0

| latest release date = {{Start date and age|20242025|0807|1605}}

| latest preview version =

| latest preview date =

Line 24:

| 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]] [[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)|CoqRocq]], 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)|CoqRocq]], which was originally named Coq after [[Thierry Coquand]].

== Features ==

Line 42:

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.

Line 50:

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.

Line 59:

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)|CoqRocq]], 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 →= ℕ → ℕ?

add x y = ?

</syntaxhighlight>

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

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

(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:

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

Line 116 ⟶ 115:

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