Everipedia Logo
Everipedia is now IQ.wiki - Join the IQ Brainlist and our Discord for early access to editing on the new platform and to participate in the beta testing.
Agda (programming language)

Agda (programming language)

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis.[2] The original Agda system was developed at Chalmers by Catarina Coquand in 1999.[3] 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 tactics language, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has Emacs and Atom interfaces[4][5] 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),[6] a type theory similar to Martin-Löf type theory.

Agda
ParadigmFunctional
Designed byUlf Norell; Catarina Coquand (1.0)
DeveloperUlf Norell; Catarina Coquand (1.0)
First appeared2007 (2007), 1.0 in 1999 (1999)
Stable release
2.6.0 / April 12, 2019 (2019-04-12)
OSCross-platform
LicenseBSD-like[1]
Filename extensions.agda,.lagda
Websitewiki.portal.chalmers.se/agda [17]
Influenced by
Coq, Epigram, Haskell
Influenced
Idris

Features

Inductive types

The main way of defining data types in Agda is via inductive data types which are similar to algebraic data types in non-dependently typed programming languages.

Here is a definition of Peano numbers in Agda:

Basically, it means that there are two ways to construct a value of type ℕ, representing a natural number. To begin, zero is a natural number, and if n is a natural number, then suc n, standing for the successor of n, is a natural number too.

Here is a definition of the "less than or equal" relation between two natural numbers:

The first constructor, z≤n, corresponds to the axiom that zero is less than or equal to any natural number. The second constructor, s≤s, corresponds to an inference rule, allowing to turn a proof of n ≤ m into a proof of suc n ≤ suc m.[7] So the value s≤s {zero} {suc zero} (z≤n {suc zero}) 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

In core type theory, induction and recursion principles are used to prove theorems about inductive types. In Agda, dependently typed pattern matching is used instead. For example, natural number addition can be defined like this:

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, is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda:

? here is a metavariable. When interacting with the system in emacs mode, it will show the user 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 Coq.

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:

Given a function check-even : (n : ℕ) → Maybe (Even n) that inputs a number and optionally returns a proof of its evenness, a tactic can then be constructed as follows:

The actual proof of each lemma will be automatically constructed at type-checking time. If the tactic fails, type-checking will fail.

Additionally, to write more complex tactics, Agda has support for automation via reflection. The reflection mechanism allows one to quote program fragments into – or unquote them from – the abstract syntax tree. The way reflection is used is similar to the way Template Haskell works.[8]

Another mechanism for proof automation is proof search action in 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.[9]

Termination checking

Agda is a total 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.[10]

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 is in beta, and is under active development.

Unicode

One of the more notable features of Agda is a heavy reliance on Unicode in program source code. The standard emacs mode uses shortcuts for input, such as \Sigma for Σ.

Backends

There are two compiler backends, MAlonzo for Haskell and one for JavaScript.

See also

  • Coq

  • Isabelle (proof assistant)

  • HOL (proof assistant)

References

[1]
Citation Linkcode.haskell.orgAgda license file
Oct 1, 2019, 4:47 AM
[2]
Citation Linkwww.cse.chalmers.seUlf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007. [1]
Oct 1, 2019, 4:47 AM
[3]
Citation Linkocvs.cfv.jp"Agda: An Interactive Proof Editor". Archived from the original on 2011-10-08. Retrieved 2014-10-20.
Oct 1, 2019, 4:47 AM
[4]
Citation Linkmailserver.di.unipi.itCoquand, Catarina; Synek, Dan; Takeyama, Makoto. An Emacs interface for type directed support constructing proofs and programs (PDF). European Joint Conferences on Theory and Practice of Software 2005. Archived from the original (PDF) on 2011-07-22.
Oct 1, 2019, 4:47 AM
[5]
Citation Linkatom.io"agda-mode on Atom". Retrieved 7 April 2017.
Oct 1, 2019, 4:47 AM
[6]
Citation Linkopenlibrary.orgLuo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
Oct 1, 2019, 4:47 AM
[7]
Citation Linkgithub.com"Nat from Agda standard library". Retrieved 2014-07-20.
Oct 1, 2019, 4:47 AM
[8]
Citation Linkhal.inria.frVan 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. [2]
Oct 1, 2019, 4:47 AM
[9]
Citation Linkwww.staff.science.uu.nlKokke, Pepijn, and Wouter Swierstra. "Auto in Agda."
Oct 1, 2019, 4:47 AM
[10]
Citation Linkwww.tcs.informatik.uni-muenchen.deAbel, Andreas. "foetus – Termination checker for simple functional programs." Programming Lab Report 474 (1998). [3]
Oct 1, 2019, 4:47 AM
[11]
Citation Linkwiki.portal.chalmers.seOfficial website
Oct 1, 2019, 4:47 AM
[12]
Citation Linkwww.cse.chalmers.seDependently Typed Programming in Agda
Oct 1, 2019, 4:47 AM
[13]
Citation Linkwww.cse.chalmers.seA Brief Overview of Agda
Oct 1, 2019, 4:47 AM
[14]
Citation Linkwww.youtube.comIntroduction to Agda
Oct 1, 2019, 4:47 AM
[15]
Citation Linkoxij.orgBrutal [Meta]Introduction to Dependent Types in Agda
Oct 1, 2019, 4:47 AM
[16]
Citation Linkpeople.inf.elte.huAgda Tutorial: "explore programming in Agda without theoretical background"
Oct 1, 2019, 4:47 AM
[17]
Citation Linkwiki.portal.chalmers.sewiki.portal.chalmers.se/agda
Oct 1, 2019, 4:47 AM
[18]
Citation Linkcode.haskell.orgAgda license file
Oct 1, 2019, 4:47 AM
[19]
Citation Linkwww.cse.chalmers.se[1]
Oct 1, 2019, 4:47 AM
[20]
Citation Linkweb.archive.org"Agda: An Interactive Proof Editor"
Oct 1, 2019, 4:47 AM