Agda (programming language): Difference between revisions

Revision as of 00:33, 20 July 2025

Latest revision as of 21:31, 21 July 2025

(One intermediate revision by one other user 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 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.

Line 67:

One of the distinctive features of Agda, when compared with other similar systems such as [[Rocq]], 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 Emacs 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 Rocq.

Line 76 ⟶ 75:

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>

Line 91 ⟶ 90:

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