Agda (programming language)

Agda combines a pure functional language with dependent types, so a type may describe properties of the value it classifies. A vector type, for example, can encode its length, making an append function preserve a statically visible length equation. This style follows the Curry–Howard correspondence: propositions are types, proofs are terms, and type checking verifies proofs. Agda has inductive data types, records, modules, pattern matching, higher-order functions, and an expressive universe hierarchy. Unlike a tactic-centered prover, it normally represents a proof directly as a program term, although libraries and editor commands provide substantial automation.³

Definitional equality is central to the experience. The checker can reduce function applications and pattern matches while comparing types, so many routine equalities need no explicit theorem. The trusted core also checks termination and positivity conditions, preserving consistency for the ordinary total fragment.⁴

Agda’s editor interaction turns incomplete programs into typed proof-development environments. A programmer can mark a hole, ask Agda for the expected type, inspect local hypotheses, refine a goal by case splitting, and let the system generate implicit arguments or matching clauses. This workflow is supported through Emacs and other editor integrations, while the command-line checker independently verifies the finished module.¹

Agda source commonly uses readable Unicode notation for dependent function and pair types, though ASCII alternatives are available. Definitions can be compiled into executable code, most notably through a Haskell backend, enabling verified components to run outside the proof checker. Compilation does not make every proof artifact computationally relevant: erased arguments and proof terms can be omitted where the backend permits, separating specification from runtime data.²

Agda is used to formalize mathematics, semantics, compilers, programming-language metatheory, and algorithms whose invariants are naturally expressed in types. A prominent application is verified data-structure programming: indexed types can rule out impossible states, while dependent pattern matching can make preservation of those invariants visible in the implementation. Researchers also use Agda to mechanize proofs about type systems and operational semantics, where intrinsically typed syntax carries judgments in its representation.⁴

The language is closely connected to the broader Martin-Löf type theory tradition and shares practical territory with Coq, Lean, Idris, and other dependently typed systems. Agda’s libraries provide reusable foundations for equality, algebra, finite structures, and formalized mathematics, but its ecosystem remains more research-oriented and less standardized than those of general-purpose industrial languages.

Agda has experimental and advanced modes that extend its role beyond conventional dependent programming. Cubical Agda adds an implementation of cubical type theory, supporting computational treatments of path equality and a form of univalence; this makes some higher-dimensional constructions executable rather than merely axiomatic.⁵

Other distinctive features include copatterns for defining observations of coinductive objects, instance arguments for type-directed search, reflection for metaprogramming, and sized types for expressing termination of selected recursive or coinductive definitions. These facilities are powerful but make the boundary between programming-language design and proof theory unusually visible. Agda also has no single mandatory logic of classical mathematics: users generally work constructively, adding axioms explicitly when a development requires principles such as excluded middle.

The project’s lineage includes Ulf Norell’s work on dependently typed programming and the Agda 2 redesign, which established much of the language’s present interactive character.³

Dependent type

A type whose formation or structure may depend on a term, allowing specifications to mention values such as sizes or indices.

Definitional equality

Equality established by computation and reduction inside the type checker, without requiring a separately supplied proof.

Hole

An unfinished expression in Agda source that exposes an expected type and supports interactive refinement.

Cubical Agda

An Agda mode and extension based on cubical type theory, including computational path equality and univalence-related constructions.