Agda is a purely functional programming language with a powerful dependent type system. In Agda, types can depend on values, so programs and proofs can be written in the same language. It is strongly typed: every expression must satisfy its type, and these types are rich enough to encode precise properties (for example, the length of a list can be part of its type). Because of this, Agda doubles as a proof assistant. One can write mathematical proofs as programs whose types express the statement being proved. This fits the Curry–Howard correspondence (sometimes called “propositions as types”), meaning that constructing a program of a given type is equivalent to proving a logical proposition. Agda is based on Martin-Löf’s Intuitionistic Type Theory, a foundational system that combines computation with constructive logic.

Every Agda program is total: the language enforces that functions must terminate for all inputs, and every case is covered by definitions. There are no unchecked exceptions or infinite loops (unless coinductive features are explicitly used). This guarantee of termination and coverage makes Agda suitable for writing correct and dependable software, but it also means that some kinds of general recursion must be formulated carefully or replaced by coinductive constructions. In short, Agda programs can be run like ordinary programs, but they are written with extra rigor to ensure logical consistency.

Agda features an interactive editing environment (often within Emacs) where programmers write code and proofs with the help of the type checker. Special holes (placeholders) can be inserted into code; Agda will infer the needed type for the hole or even give suggestions for filling it. As a result, development is roughly a dialogue where the programmer gradually fills in parts of the proof or program, guided by Agda’s feedback.

Historical Context and Evolution

Agda programming language
Type	programming language
Key terms	dependently typed, Martin-Löf type theory, proofs-as-programs
Related	Coq, Idris, Lean
Domain	functional programming, proof assistant
Modules	modules/records, universe polymorphism, standard library
Features	totality/termination checking, pattern matching, holes/interactive editing
Examples	length-indexed vectors, equality proofs, interactive refinement
Variants	Cubical Agda, coinduction
Wikidata	Q20479

The ideas behind Agda have a long history in constructive logic and functional programming. Agda’s roots trace back to Per Martin-Löf’s work on intuitionistic type theory in the 1970s and 1980s. In the 1980s and 1990s, computer scientists at Chalmers University (Gothenburg, Sweden) built early proof assistants like ALF that used these ideas. Language designs like Cayenne (by Lennart Augustsson) and Epigram explored dependent types for programming in the late 1990s and early 2000s.

The original Agda (sometimes called Agda 1) was implemented in Haskell by Catarina Coquand and others around the early 2000s. It provided a prototype of a language merging program and proof. By 2005–2007, Ulf Norell and colleagues at Chalmers designed a new, cleaner version known as Agda 2. Norell’s 2007 PhD thesis (“Towards a Practical Programming Language Based on Dependent Type Theory”) laid out the design and implementation. Agda 2 shipped with a rich editor mode and many new features, and it became an open-source project with contributors across academia.

Since then Agda has evolved steadily. It has a public development repo and regular releases (e.g. versions 2.6, 2.8, etc.). Notable milestones include adding universe polymorphism (flexible handling of type-in-type problems) and coinduction (support for infinite data) in the late 2010s. Most recently, an experimental Cubical Agda mode was introduced to support concepts from Homotopy Type Theory, such as the univalence axiom and higher inductive types. In parallel, a growing standard library of definitions and proven facts about math and data structures has been developed. Throughout its history, Agda’s development has been driven by functional programmers and logicians, so it often leads in advanced type-theoretic features. It is part of a family of modern systems like Coq, Lean, and Idris, which all share the idea of combining programming with proof.

Core Mechanisms and Features

Dependent Types and Type Theory. At the heart of Agda is its dependent type system. A dependent type is a type that can refer to a value. For example, Agda lets you define a type of vectors `Vec A n`, meaning lists of elements of type `A` of length `n`. Here `n` is a natural number value embedded in the type. Functions in Agda can have types that speak about things like “for all lengths `n`” or “there exists a prime factor of `n`”. Formally, the type of a function might be written `(n : Nat) → Vec A n` (a family of types indexed by `n`). This expressive power means a function’s type can state precise invariants (like “the output list has the same length as input” or “the integer returned is prime”), and the compiler will enforce them as part of type checking.

The underlying logic is intuitionistic (constructive) logic. Proofs in Agda are built without relying on classical principles like the law of excluded middle unless you assume them explicitly. In practice, Agda programmers prove statements by constructing functions. For instance, a proof that every natural number has a prime factor is an Agda function that, given a number `n`, returns a pair `(p , proof)` where `p` is a prime dividing `n` and `proof` is a witness of that fact. Completing the function corresponds to completing the proof.

Pattern Matching and Definitions. Programming in Agda resembles Haskell in many ways. Data types (including inductive families) are defined by constructors. For example, natural numbers might be defined as `data Nat : Set where zero : Nat ; suc : Nat → Nat`. Functions on such data are typically defined by pattern matching: you write clauses that say what the function does on `zero` versus on `suc n`. Pattern matching can bind values from the structure and even match on dependent indices. Under the hood, Agda checks that all patterns are covered (no missing cases) and that definitions are well-founded.

Because Agda is total, recursion must always meet a termination condition. Usually this means the function makes a call on a strictly smaller argument (structural recursion). Agda’s termination checker inspects recursive calls to ensure they decrease on some argument. For example, a function that recurses on `suc n` can call itself on `n` and satisfy the checker. If recursion is more complex (e.g. mutual or nested), the programmer sometimes needs to convince Agda by rewriting the definitions or by providing a measure function to justify termination. If no termination can be shown, Agda rejects the definition. This totality guarantee means that all Agda functions are guaranteed to terminate with a result, preventing certain classes of runtime errors and infinite loops.

Holes and Interactive Editing. A distinctive feature of Agda is its interactive editing support. In an Agda source file, you can write a question mark `?` or a named placeholder `_hole` as a “hole” in your code. When you run the type checker, it will report the type that is needed at that hole, and often suggest ways to fill it (based on known variables and constructors in scope). Programmers typically iterate: they write an outline of a function with holes, load it, see what each hole’s type is, then go on to refine the holes gradually. The Agda Emacs mode also allows jumping to definitions, searching for names, and auto-completion of constructors. This workflow is very goal-directed and similar to interactive theorem proving in Coq or Lean, but integrated directly into the source code.

Modules and Records. For large developments, Agda has a modular namespace system and records (similar to “structs” or “classes”). Modules allow splitting code into files and namespaces; you can `import` or `open import` a module much like Haskell’s module system. Records group related data and proofs, somewhat like algebraic structures. For example, a record `Semigroup` might bundle a type `A`, an operation `_*_ : A → A → A`, and proofs that it is associative, all under one name. Opening a record instance introduces its fields into scope. This makes it convenient to work abstractly. The Agda standard library heavily uses records to define mathematical structures (monoids, groups, rings, etc.) parameterized by sets with operations and laws.

Universe Polymorphism. To avoid logical paradoxes (like “the type of all types”), Agda's type theory includes a hierarchy of universes (often written `Set₀, Set₁, Set₂, …`). A type like `Nat : Set₀` lives in the lowest universe. Types of types might live in `Set₁`, and so on. Universe polymorphism is an advanced feature that lets definitions be generic over universe levels. For instance, one can write a polymorphic list type `List {ℓ} (A : Set ℓ) : Set ℓ` that works if `A` is at any level `ℓ`. This avoids redundancy and makes libraries more uniform. Agda’s universe polymorphism was refined to remove much of the boilerplate of managing levels manually, so that users only rarely need to think about it.

Standard Library. Agda comes with (and has a growing community-maintained) standard library of data types, functions, and proved facts. It includes modules for basic types (`Nat`, `List`, `Maybe`), algebra (`Semiring`, `Matrix`, etc.), decidability (`Relation.Nullary`), and more. For example, it has `Data.Vec` for fixed-length lists, with many utility functions, and `Relation.Binary.PropositionalEquality` for reasoning about equality. These modules are written in Agda itself and use all the usual language features. Users routinely import them to build more complex proofs. The library is available online and updated alongside Agda releases.

Cubical Agda. A recent evolution is Cubical Agda, an extension of the language that incorporates ideas from Cubical Type Theory and Homotopy Type Theory (HoTT). In Cubical Agda, types can represent spaces with geometric structure, and there are built-in notions of paths (equals can be treated as continuous deformation). The key benefit is support for the univalence axiom and higher inductive types as native concepts with computational meaning. In practice, this means one can prove that equivalent types are equal in a strong way, and define quotient types or circle spaces and have Agda compute with them. Cubical Agda also makes coinductive equality notions (bisimilarity) coincide with usual propositional equality by construction. This feature is mostly used in advanced research on type theory and homotopy.

Coinduction and Copatterns. By default, Agda deals with inductive types (finite data built from constructors). For infinite structures (streams, infinite trees, etc.), Agda supports coinductive types. You declare a coinductive (sometimes called “codata” or “corecord”) construction that can produce infinite values that are defined by observation. Related to this are copatterns: just as patterns match on constructing data, copatterns match on destructing data (like saying “`head` of the stream is...” or “the `tail` of this stream has...”). For example, one can define an infinite stream of ones by giving its head and tail records, rather than by recursion on a finite argument. Coinduction in Agda is guarded by a modality (`∞`) or sized types so that productivity (each finite prefix can be computed) is ensured. Where inductive types ensured termination, coinductive types ensure productivity of infinite constructions. This is how Agda handles things like lazy lists or infinite trees in a total setting.

Proofs-as-Programs. Underlying almost everything is the principle that writing programs is writing proofs. For every theorem we want to prove, we give it a precise type, and then we write a program that inhabits that type. For example, the statement “a list of length n appended with a list of length m has length n+m” becomes a type whose returned value is a proof object. Completing the proof means writing a function (using pattern matching and recursion) that constructs the proof in each case. Agda’s type checker plays the role of the proof checker. This approach means that to prove something, one must be very explicit about how all cases work, which in turn means bugs in proofs usually correspond to type errors that the programmer fixes.

Representative Examples

Agda has been used for a variety of programming and proving tasks, both as toy examples and in real developments. Here are some illustrative cases:

Arithmetic and Number Theory Proofs. A classic example is formalizing Euclid’s theorem that there are infinitely many primes. In Agda one can prove: “for every natural number `n`, there exists a prime `p` greater than `n`.” As a constructive proof, this means writing a function that, given `n`, produces a specific prime and a proof of these properties. The proof uses factorial and divisibility: it shows that factors of `n! + 1` must be larger than `n`. This kind of proof makes extensive use of Agda’s standard library (importing definitions of naturals, primes, factorial, and divisibility) and showcases pattern matching and record proofs. In fact, such a proof was written (with commentary) in Agda to illustrate how a full mathematical argument can be encoded. It highlights how the module system groups definitions, and how the propositional equality type is used to chain equalities in a proof.

Algorithms with Correctness. One can program algorithms in Agda and simultaneously prove their correctness. For example, a sorting function can be given a type that guarantees the output is sorted and is a permutation of the input. A developer would then write the function (say, insertion sort or merge sort) by recursion and also supply proofs of the sorting property and permutation property. The proofs become additional cases checked by Agda. In practice, this is burdensome for large algorithms, but it is done as an exercise in teaching or for critical code. Agda’s termination checks and pattern coverage ensure that, once all proofs are complete, the code is guaranteed to meet its specification.

Data Structures with Invariants. Datasets that carry invariants in their types are natural in Agda. For instance, one can define a binary search tree type indexed by a size so that any two BSTs of the same size are considered equal up to isomorphism. In such cases, inserting or deleting an element becomes a function whose type guarantees the size changes as expected. Similarly, dependent records can carry proofs as fields. For example, a record for a finite group includes not just the group data and laws, but as part of the type it includes the size of the group. This way, any proof about groups also keeps track of finiteness data. The standard library contains many such indexed definitions.

Type-Checker or Language Semantics. Agda itself has been used to partly formalize and prototype theories of programming languages. For example, one can encode the syntax and reduction rules of a small lambda calculus in Agda and prove meta-theorems like type preservation. In fact, research papers have used Agda to develop and check type systems: for instance, showing that a dependently typed language has decidable type-checking or that certain optimizations preserve semantics. Because Agda can execute functions, such formalizations can sometimes even act as running interpreters for toy languages.

Mathematical Mathematics. While not as famous as Coq or Lean for large-scale formalization of mathematics, some Agda users have formalized pieces of pure math. For example, algebraic topology results can be encoded when using Cubical Agda, allowing reasoning about spaces. More modestly, researchers in homotopy type theory have used Agda to experiment with new kinds of types (like higher inductive types) to prove abstract theorems from algebra and topology. Agda’s emphasis on type theory makes it a natural choice for exploring alternative foundations of mathematics.

These examples illustrate that Agda serves both as a programming language and a laboratory for writing machine-checked proofs. By writing code, users explicitly handle all cases, making omissions practically impossible. As a consequence, any function or proof that checks will have a high level of confidence.

Learning and Practice

Learning Agda usually means learning some type theory and functional programming together. There are several resources: the official Agda manual and tutorials (often called A Taste of Agda) explain the syntax and basic constructs. The Agda wiki and standard library documentation give numerous examples of definitions and proofs. Many university courses on type theory or advanced functional programming use Agda for exercises, since it can illustrate the connection between logic and code.

In practice, newcomers often start with simple definitions in an interactive environment. A common first exercise is to define natural numbers and addition, then prove that addition is commutative. As they type, they use holes to let Agda show what remains to be done. When a type error occurs or a case is missing, Agda highlights it in the editor. Over time, the user picks up conventions like using `fixity` declarations (for operators), mixfix function names, and Unicode symbols for mathematical notation (`∀` for `forall`, `ℕ` for naturals, `–>` or `→` for function types).

Since Agda is open source, one can also read its own source code (written in Haskell) or inspect others’ proofs in the standard library to learn idiomatic patterns. The community is active on mailing lists and chat rooms, so questions about style or error messages often get quick answers. In terms of tooling, besides Emacs, other editors like VS Code have Agda support. Building Agda projects requires running the `agda` command on files; the compiler checks everything and can also generate Haskell code or a Java backend if wanted.

Challenges and Open Questions

Agda is a very expressive system, but this power comes with trade-offs and ongoing areas of research:

Complexity of Proof Development. Writing proofs in Agda can be lengthy. Unlike some other systems, Agda does not have a built-in tactic language (scripts that automate multiple proof steps). Every proof must be spelled out by constructing terms. This makes proofs clear but sometimes verbose. Extensions like reflection or higher-level libraries try to streamline repetitive patterns, but this remains a labor-intensive aspect compared to tactics in Coq or Lean.

Termination and Totality. The strict totality requirement is both a strength and a limitation. It ensures soundness, but it means certain obvious programs need rethinking. For example, general recursion must be done via well-founded recursion or encoded with streams, which can be awkward. Research into sized types and other extensions is ongoing to give more flexibility while preserving safety. Similarly, coinductive constructions require discipline: one must ensure productivity or otherwise the definition is rejected. These checks can sometimes puzzle newcomers.

Universe Levels. Universe polymorphism reduces the burden of tracking types-of-types, but the concept of universes can still confuse learners. Complex generic libraries often need `{ℓ₁ ℓ₂ : Level}` annotations. Though often implicit, universe levels occasionally surface in error messages, which can be a stumbling block. How to make these safe but invisible remains an area of active design.

Performance and Scalability. Because Agda type-checks dependently, some developments can become slow to check. Large proofs might cause the type checker to run for minutes. The Agda team and community continually optimize the compiler to improve performance. A related issue is maintenance of large libraries: changes in one part (say the definition of equality) can cascade into recompiling many dependent proofs. Improved incremental checking and module systems are topics of interest.

Adoption and Integration. Compared to mainstream programming languages, Agda’s audience is small (mostly research and teaching). Integrating Agda code into standard software projects is nontrivial. Some work has been done to extract Agda definitions to Haskell or JavaScript, but using those in a larger codebase while trusting the correctness is rare. Furthermore, since Agda lacks side effects and I/O except as libraries, it’s not designed as a systems programming language. Whether dependently-typed languages will ever become mainstream (e.g. for safe APIs or protocol implementations) is an open industry question.

Extensionality and New Type Theories. Classically, Agda has an intensional equality (two functions are equal only if provably the same process, not just extensionally equal). Many programmers wish for the ability to automatically reason that functions giving equal outputs on all inputs are equal (function extensionality). Cubical Agda addresses this by adopting a different notion of equality. However, bringing these homotopical features into everyday Agda work raises questions about compatibility and semantics. The balance between constructive rigor and convenient reasoning remains delicate.

Significance and Applications

Agda plays an important role in research combining programming and logic. Its significance includes:

Foundation for Dependently Typed Programming. Agda was one of the pioneering languages demonstrating practical dependent types. It showed how one can write “real” programs (with pattern matching, modules, etc.) in such a setting. Its development influenced and paralleled languages like Idris (which focuses more on general programming), Coq (more on proving), and Lean. Ideas from Agda (like hole-driven development) appear in these other systems too.

Experimentation with Type Theory. Researchers use Agda as a testbed for new type system ideas. For instance, Cubical Agda allowed exploration of homotopy type theory concepts without building a new system from scratch. Similarly, features like universe polymorphism or copatterns were refined through Agda. It is not just a consumer of ideas but also a source of innovations shared with the broader proof assistant community.

Verified Software and Mathematics. By enabling programs to carry proofs, Agda can help build verified software components. Although not widespread in industry, there are projects (especially in academia) that use Agda to prove parts of algorithms correct. Even teaching introductory proofs via Agda can give programmers a taste of formal reasoning. In mathematics, Agda has been used to formalize theories in category theory, algebra, and topology — sometimes as a complement to other systems. Its capability to compute with proofs (via evaluation of programs) can even produce certified counterexamples or concrete witnesses.

Educational Use. Agda is often used in advanced courses on type theory and functional programming. Writing a bit of Agda code teaches students about recursion, data types, and logic in one setting. Some textbooks on type systems or proof assistants use Agda examples. Its combination of syntax (looking like Haskell) with theorem proving makes it a valuable teaching tool.

Interoperability. While Agda itself is self-contained, it can interoperate in small ways. For example, one can write parts of a program in Agda and then use the Agda compiler to generate Haskell code. This means a trusted core (verified in Agda) can supply critical functions to a larger Haskell application. Similarly, small prototyping in Agda can inform the design of safer APIs in other languages.

In summary, Agda sits at the intersection of programming languages, logic, and type theory. Its main significance lies in research and education, demonstrating what happens when code and proof meet tightly. Its ongoing development ensures it remains a cutting-edge environment for dependently typed programming.