Agda (programming language): Difference between revisions

Revision as of 12:30, 18 May 2025

Revision as of 00:33, 20 July 2025

Line 29:

</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)|Rocq]], 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 65:

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

Line 71:

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

=== Proof automation ===