Agda (programming language): Difference between revisions

Revision as of 04:35, 19 July 2024

Revision as of 00:50, 17 September 2024

Line 1:

{{shortShort description|Functional programming language}}

{{distinguishDistinguish|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 = [[functionalFunctional programming|Functional]]

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

| designer = Ulf Norell; Catarina Coquand (1.0)

| developer = Ulf Norell; Catarina Coquand (1.0)

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

| latest release version = 2.6.3

| latest release dateversion = {{Start date and age|2023|01|30}}2.7.0

| latest testrelease versiondate = {{Start date and age|2024|08|16}}

| latest testpreview dateversion =

| latest releasepreview versiondate = 2.6.3

| 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|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 |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 as 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, but unlike [[Coq (software)|Coq]], 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]], [[Atom (text editor)|Atom]], and [[VS Code]] interfaces<ref name="emacs-mode">{{cite conference |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 mode from the command line.

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

Line 52 ⟶ 53:

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 bracketsbracket]]s may be omitted if they can be inferred.

=== Dependently typed pattern matching ===

Line 72 ⟶ 73:

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

<syntaxhighlight lang="agda">

data Maybe (A : Set) : Set where

Line 101 ⟶ 102:

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

Line 137 ⟶ 135:

* [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]

* [http://people.inf.elte.hu/divip/AgdaTutorial/Index.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 a number ofmany introductory lectures and exercises on Agda

{{Haskell programming}}

Line 157 ⟶ 155:

[[Category:Programming languages created in 2007]]

[[Category:2007 software]]

<!-- Hidden categories below -->

[[Category:Articles with example Haskell code]]