Agda (programming language): Difference between revisions

Revision as of 17:41, 30 November 2020

Revision as of 03:03, 7 February 2021

Line 24:

}}

'''Agda''' is a [[Dependent type|dependently typed]] [[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 |accessdateaccess-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]], 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 (programming language)|Haskell]]-like syntax. The system has [[Emacs]] and [[Atom (text editor)|Atom]] interfaces<ref name="emacs-mode">{{cite conference |first1 = Catarina |last1 = Coquand |first2 = Dan |last2 = Synek |first3 = Makoto |last3 = Takeyama |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> but can also be run in batch mode from the command line.

Line 51:

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 |accessdateaccess-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 brackets may be omitted if they can be inferred.

=== Dependently typed pattern matching ===