Agda

Agda is a dependently typed functional programming language and interactive proof assistant developed at Chalmers University of Technology in Gothenburg, Sweden. Through the Curry-Howard correspondence, Agda treats types as propositions and programs as proofs, allowing programmers to write code that simultaneously serves as a mathematical proof of its own correctness. Agda occupies a unique space between programming languages and theorem provers, making it a cornerstone tool in programming language research and formal verification.

History & Origins

Agda’s roots trace back to the 1980s, when the Programming Logic Group at Chalmers University began building proof assistants based on Per Martin-Löf’s intuitionistic type theory. This lineage produced ALF (A Logical Framework) in the early 1990s, created by Thierry Coquand (type checker) and Lennart Augustsson (window interface), followed by the Alfa graphical interface by Thomas Hallgren.

Agda 1

In the late 1990s, Catarina Coquand created the first version of Agda in Haskell, establishing its Emacs-based interactive development environment. This built on earlier prototypes: a Gofer implementation by Thierry Coquand (1995) and a C implementation by Dan Synek (1996). The name “Agda” comes from a Swedish song “Honan Agda” (The Hen Agda) by Cornelis Vreeswijk, a playful allusion to the proof assistant Coq (now Rocq), which was named after Thierry Coquand - both names refer to poultry.

Agda 2

Starting around 2005, Ulf Norell undertook a fundamental reimplementation as part of his doctoral research at Chalmers. His 2007 PhD thesis, “Towards a practical programming language based on dependent type theory,” introduced Agda 2 - effectively a new language sharing its predecessor’s name and philosophical tradition. Agda 2 brought dependently typed pattern matching as a core primitive, a richer module system, and a more practical approach to programming with dependent types. This is the version in active use today.

Design Philosophy

Agda is built on several distinctive principles that set it apart from mainstream programming languages:

Propositions as Types

Agda fully embraces the Curry-Howard correspondence. A type in Agda is simultaneously a specification (what the program should do) and a proposition (a mathematical statement). Writing a program of that type constitutes a proof that the proposition holds. This means verified software and mathematical proofs are expressed in the same language.

Totality

Agda is a total language by default. Every function must:

• Terminate on all inputs (verified by a termination checker)
• Cover all cases (verified by a coverage checker)

A program of type T will always produce a value of type T - no runtime errors, no infinite loops, no unhandled cases. This guarantee is essential for Agda’s role as a proof assistant, since a non-terminating “proof” would be unsound.

Precision Over Convenience

Agda favors expressive precision. Where most languages let you write a function head that crashes on empty lists, Agda’s type system can encode the requirement that the list be non-empty directly in the type signature, preventing the error at compile time.

Key Features

Dependent Types

Types in Agda can depend on values, enabling extremely precise specifications:

1
2
3
4
5
6
7
8

-- A vector type indexed by its length
data Vec (A : Set) : Nat → Set where
  []  : Vec A zero
  _∷_ : A → Vec A n → Vec A (suc n)

-- Type-safe head: can only be called on non-empty vectors
head : Vec A (suc n) → A
head (x ∷ _) = x

The type Vec A (suc n) guarantees at compile time that the vector has at least one element. No runtime check is needed.

Unicode and Mixfix Operators

Agda supports Unicode identifiers throughout, allowing code to closely mirror mathematical notation. Combined with mixfix operators (where underscores mark argument positions), this enables natural syntax:

1
2
3
4
5
6
7
8

-- Mixfix if-then-else
if_then_else_ : Bool → A → A → A
if true  then x else _ = x
if false then _ else y = y

-- Mathematical notation
_≤_ : Nat → Nat → Set
_+_ : Nat → Nat → Nat

Interactive Development

Agda’s Emacs mode (and VS Code extension) provides a uniquely interactive programming experience. Programmers can leave “holes” (denoted by ?) in their code and use editor commands to:

• Ask the type checker what type is expected
• Automatically refine the goal by case-splitting on variables
• Search for terms that fill a hole (using the Mimer synthesizer since Agda 2.7.0)

This “hole-driven development” transforms programming into a guided dialogue with the type checker.

Inductive Families

Data types can be indexed by values, forming inductive families:

1
2
3
4
5
6
7
8

-- Natural numbers
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

-- Propositional equality
data _≡_ {A : Set} : A → A → Set where
  refl : x ≡ x

Pattern Matching

Agda supports dependently typed pattern matching, where matching on a constructor can refine the types of other variables:

1
2
3
4

-- The type checker knows that if the proof is refl,
-- then x and y must be the same value
sym : x ≡ y → y ≡ x
sym refl = refl

Parameterized Modules

Modules can be parameterized over types and values, enabling generic programming:

1
2
3

module Sort (A : Set) (_≤_ : A → A → Bool) where
  sort : List A → List A
  -- implementation using the provided ordering

Cubical Agda

Since version 2.6.0 (2019), Agda supports Cubical Type Theory via the --cubical flag. This provides:

• Computational univalence: The univalence axiom computes, rather than being postulated
• Higher inductive types: Data types with path constructors, enabling quotient types and other advanced constructions
• Function extensionality: Provable, not just assumed

Cubical Agda is one of the leading implementations of homotopy type theory.

Compilation and Backends

While Agda excels as a proof assistant, it can also produce executable programs through multiple compiler backends:

• GHC Backend: Compiles Agda to Haskell, then to native code via GHC. This is the primary backend for executable programs.
• JavaScript Backend: Compiles to JavaScript (ES6 and CommonJS), enabling web applications.

IO in Agda requires explicit postulation and compiler pragmas to link to the host language’s IO facilities:

1
2
3

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

This reflects Agda’s design priority: it is first a language for reasoning about programs, with execution as a secondary concern.

Evolution

Agda has evolved significantly since its Agda 2 rewrite:

Platform and Tooling

Agda is written in Haskell and runs on any platform supported by GHC:

• Linux, macOS, and Windows
• Available via Hackage (Haskell package registry) and Stackage
• Agda 2.8.0 introduced self-contained binary distributions for easier installation

Editor Support

• Emacs: The primary and most feature-complete interface, with deep integration for interactive development
• VS Code: Via the agda-mode extension
• Neovim: Via the cornelis plugin for interactive Agda development

File Extensions

• .agda - Standard Agda source files (UTF-8 encoded)
• .lagda, .lagda.tex - Literate Agda in LaTeX format
• .lagda.md - Literate Agda in Markdown format
• .lagda.rst - Literate Agda in reStructuredText format

Current Relevance

Agda remains actively developed, with a dedicated core team based primarily at Chalmers University and the University of Gothenburg. Key current maintainers include Ulf Norell (original Agda 2 author), Andreas Abel, Jesper Cockx, Nils Anders Danielsson, and others. The community holds biannual Agda Implementors Meetings (AIMs) that have continued since 2004.

The Agda GitHub repository has approximately 2,800 stars and over 200 contributors, with regular releases. The language continues to push the boundaries of what is possible with dependent types, serving as both a research vehicle and a practical tool for formal verification.

Why It Matters

Agda’s significance extends beyond its direct user base:

1. Pioneering dependent types for programming: Agda demonstrated that dependent types could be practical for programming, not just theorem proving, influencing languages like Idris that brought dependent types closer to mainstream programming.

2. Advancing type theory: Cubical Agda is at the forefront of homotopy type theory, an active area of mathematical research connecting type theory, topology, and higher category theory.

3. Proving programs correct: Agda provides a pathway to software where correctness is mathematically guaranteed, not merely tested. As systems grow more complex and safety-critical, the value of this approach continues to increase.

4. Education: Through textbooks like “Programming Language Foundations in Agda,” it has become an important teaching tool for programming language theory, making abstract concepts concrete and machine-checkable.

5. The Gothenburg tradition: Agda represents decades of research at Chalmers on type theory and proof assistants, a tradition that has shaped how the programming language community thinks about types, proofs, and the connection between them.