Agda (programming language)

Last updated
Agda
Agda's official logo.svg
Paradigm Functional
Designed by Ulf Norell; Catarina Coquand (1.0)
Developer Ulf Norell; Catarina Coquand (1.0)
First appeared2007;16 years ago (2007) (1.0 in 1999;24 years ago (1999))
Stable release
2.6.3 / January 30, 2023;9 months ago (2023-01-30)
Typing discipline strong, static, dependent, nominal, manifest, inferred
Implementation language Haskell
OS Cross-platform
License BSD-like [1]
Filename extensions .agda, .lagda, .lagda.md, .lagda.rst, .lagda.tex
Website wiki.portal.chalmers.se/agda
Influenced by
Coq, Epigram, Haskell
Influenced
Idris

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.

Contents

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, Atom, and VS Code interfaces [4] [5] [6] 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), [7] a type theory similar to Martin-Löf type theory.

Agda is named after the Swedish song "Hönan Agda", written by Cornelis Vreeswijk, [8] which is about a hen named Agda. This alludes to the name of the theorem prover Coq, which was named after Thierry Coquand, Catarina Coquand's husband.

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:

dataℕ:Setwherezero:ℕ suc:ℕ→ℕ

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:

data_≤_:ℕ→ℕ→Setwherez≤n:{n:ℕ}→zero≤n s≤s:{nm:ℕ}→n≤m→sucn≤sucm

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. [9] 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:

addzeron=n add(sucm)n=suc(addmn)

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:

add:ℕ→ℕ→ℕ addxy=?

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

dataMaybe(A:Set):SetwhereJust:A→MaybeA Nothing:MaybeA  dataisJust{A:Set}:MaybeA→Setwhereauto:∀{x}→isJust(Justx)Tactic:∀{A:Set}(x:MaybeA)→isJustx→A TacticNothing()Tactic(Justx)auto=x

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:

check-even-tactic:{n:ℕ}→isJust(check-evenn)→Evenn check-even-tactic{n}=Tactic(check-evenn)lemma0:Evenzero lemma0=check-even-tacticauto  lemma2:Even(suc(suczero))lemma2=check-even-tacticauto

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. [10]

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. [11]

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. [12]

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

Related Research Articles

ML is a functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the types of most expressions without requiring explicit type annotations, and ensures type safety – there is a formal proof that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. While a general-purpose programming language, ML is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving, and formal verification.

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and type theory in general is the academic study of type systems.

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every term. Usually the terms are various language constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term. Type systems formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types, data structures, or other components.

Intuitionistic type theory is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

<span class="mw-page-title-main">Coq (software)</span> Proof assistant

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics. For this second reason, the CoC and its variants have been the basis for Coq and other proof assistants.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human-machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

Epigram is a functional programming language with dependent types, and the integrated development environment (IDE) usually packaged with the language. Epigram's type system is strong enough to express program specifications. The goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the compiler. Epigram exploits the Curry–Howard correspondence, also termed the propositions as types principle, and is based on intuitionistic type theory.

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, and Idris, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.

In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function.

<span class="mw-page-title-main">Matita</span>

Matita is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man–machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist.

In programming languages and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value; e.g., it is used as the return type of functions which may or may not return a meaningful value when they are applied. It consists of a constructor which either is empty, or which encapsulates the original data type A.

In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

<span class="mw-page-title-main">Thierry Coquand</span> French computer scientist and mathematician

Thierry Coquand is a French computer scientist and mathematician who is currently a professor of computer science at the University of Gothenburg, having previously worked at INRIA. He is known for his work in constructive mathematics, especially the calculus of constructions.

ALF is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.

Conor McBride is a Reader in the department of Computer and Information Sciences at the University of Strathclyde. In 1999, he completed a Doctor of Philosophy (Ph.D.) in Dependently Typed Functional Programs and their Proofs at the University of Edinburgh for his work in type theory. He formerly worked at Durham University and briefly at Royal Holloway, University of London before joining the academic staff at the University of Strathclyde.

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell.

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory.

Lean is a proof assistant and programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. It was made by Microsoft Research.

References

  1. ↑ Agda license file
  2. ↑ Ulf Norell. Towards a practical programming language based on dependent type theory. PhD Thesis. Chalmers University of Technology, 2007.
  3. ↑ "Agda: An Interactive Proof Editor". Archived from the original on 2011-10-08. Retrieved 2014-10-20.
  4. ↑ Coquand, 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.
  5. ↑ "agda-mode on Atom" . Retrieved 7 April 2017.
  6. ↑ "agda-mode - Visual Studio Marketplace". marketplace.visualstudio.com. Retrieved 2023-06-06.
  7. ↑ Luo, Zhaohui. Computation and reasoning: a type theory for computer science. Oxford University Press, Inc., 1994.
  8. ↑ "[Agda] origin of "Agda"? (Agda mailing list)" . Retrieved 24 Oct 2020.
  9. ↑ "Nat from Agda standard library". GitHub . Retrieved 2014-07-20.
  10. ↑ 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.
  11. ↑ Kokke, Pepijn, and Wouter Swierstra. "Auto in Agda."
  12. ↑ Abel, Andreas. "foetus – Termination checker for simple functional programs." Programming Lab Report 474 (1998).

Further reading

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.