Compendium

Agda — Reference

10 min read

Agda — Reference

Source: https://agda.readthedocs.io/en/latest/

Agda

  • Created: 1999 (Agda 1, by Catarina Coquand at Chalmers); Agda 2 complete rewrite by Ulf Norell (2007 PhD), which is what “Agda” means today. Current main developers: Andreas Abel, Jesper Cockx, Nils Anders Danielsson, Ulf Norell. (https://wiki.portal.chalmers.se/agda/pmwiki.php)
  • Latest stable: Agda 2.8.0 (released July 5, 2025); Agda Standard Library 2.3 (Aug 2, 2025). https://github.com/agda/agda/releases
  • Owner / steward: Chalmers University of Technology and University of Gothenburg (Logic and Types group). Open source, MIT-style license.
  • Paradigms: Purely functional, dependently-typed, total. Doubles as a proof assistant — but Agda’s philosophy is “the program is the proof,” with much less reliance on tactics than Coq/Lean.
  • Typing: Intensional Martin-Löf Type Theory (MLTT) with universe polymorphism, optionally cumulativity, optional --without-K (HoTT-compatible) or --cubical (Cubical Type Theory). Inductive families, induction-recursion, sized types.
  • Memory: Implemented in Haskell; uses GHC’s GC. Compiled programs use the chosen backend’s runtime.
  • Compilation: GHC backend (MAlonzo) — compiles to Haskell, then native via GHC. Also JavaScript backend and Erlang backend (community-maintained).
  • Primary domains: Type theory and HoTT research, formalized programming language semantics, proof-as-program teaching, exploratory dependent-types work.
  • Official docs: https://agda.readthedocs.io/en/latest/ • https://wiki.portal.chalmers.se/agda/

At a glance

Agda is the most “expressive” of the dependently-typed family — it has the cleanest theoretical foundation (MLTT), the most flexible reflection / unquoting, and the only one with mature Cubical Type Theory for native HoTT. It is also the least automated: where Coq/Lean lean on tactics, Agda expects you to write the term, with the editor (agda-mode) helping interactively via holes and case-splitting. The language has a famously beautiful syntax with mixfix Unicode operators. Source: https://agda.readthedocs.io/, https://wiki.portal.chalmers.se/agda/pmwiki.php.

Getting started

  • Install: Via cabal (cabal install Agda), stack, or system package manager. Pre-built binaries available on the GitHub release page (Agda 2.8.0+ ships a self-contained single binary). Match the stdlib version to the Agda version (https://github.com/agda/agda-stdlib).

    cabal install Agda
agda --version

  • Editor: Agda is editor-driven. The canonical environment is Emacs + agda2-mode (ships with Agda):

    M-x agda2-mode
C-c C-l   load file
C-c C-,   show goal & context
C-c C-c   case-split on a pattern variable
C-c C-r   refine a hole
C-c C-a   automatic proof search (Agsy)

    VS Code support via agda-mode extension (Sneller); also a --interaction-json mode for editor-agnostic frontends (https://agda.readthedocs.io/en/latest/tools/command-line-options.html).

  • Hello world:

    module Hello where
open import IO
main = run (putStrLn "Hello, Agda!")

  • Smallest proof:

    open import Relation.Binary.PropositionalEquality
refl-example : 1 + 1 ≡ 2
refl-example = refl

  • Project layout: A <name>.agda-lib file declares dependencies and source paths:

    name: myproj
depend: standard-library
include: src

    Dependencies tracked in ~/.agda/libraries.

  • No package manager: Agda has no equivalent of opam/Lake/cabal-for-Agda — you clone libraries and register them manually. The community is iterating; agda-pkg exists but is not standard.

Basics

  • Types & literals: ℕ (Nat, Unicode), Bool, Char, String, Float, Set (the universe of small types), Set ℓ (level-polymorphic universe), ⊤ (unit), ⊥ (empty). Numeric literals use the Number instance class.

  • Variables / scoping: let x = e in body, where-clauses on the right of definitions. private and abstract keywords for visibility.

  • Control flow: Only pattern matching and if then else (defined as a function, not a syntactic form). Strict left-to-right evaluation of patterns.

  • Functions:

    data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
 
_+_ : ℕ → ℕ → ℕ
zero    + m = m
(suc n) + m = suc (n + m)

    Mixfix names use _ as positional placeholders. Anonymous λ x → e or λ where { p1 → e1 ; p2 → e2 }.

  • Strings: UTF-8 String; concatenation _++_. The stdlib provides Data.String.

  • Collections: List A, Vec A n (length-indexed), Maybe A, Σ A B (sigma), _×_ (product). Stdlib modules: Data.List, Data.Vec, Data.Maybe, Data.Product.

Intermediate

  • Type system depth: Full MLTT with universe polymorphism (Set ℓ for ℓ : Level), Set₀ ⊂ Set₁ ⊂ ... (predicative). Inductive families (Vec A n), induction-recursion (define a Set and a function on it simultaneously — Dybjer-Setzer), inductive-inductive types. Pattern matching is the primitive — no tactic-based proof construction by default. (https://agda.readthedocs.io/en/latest/language/index.html)
  • Modules: Modules are first-class — they can be parameterized (module Foo (A : Set) where ...), opened (open Foo), reexported, applied like functors. Records are a special case of modules.
  • Error handling: Pure code uses Maybe/Either/sigma types. The IO type comes from the backend (Haskell IO exposed via the GHC backend’s IO.agda).
  • Concurrency primitives: None at the language level; whatever the backend exposes (e.g., GHC’s forkIO via FFI).
  • I/O: IO monad bound to the backend. Data.IO and IO.Primitive for primitive operations. agda --compile <file> to produce a runnable.
  • Stdlib highlights: agda-stdlib (https://github.com/agda/agda-stdlib) — Data.Nat, Data.List, Data.Vec, Data.Maybe, Data.Product, Data.Sum, Algebra, Relation.Binary, Relation.Binary.PropositionalEquality, Function, Category.*. Significant but smaller than mathlib4.

Advanced

  • Memory / GC: GHC RTS for the standard backend.

  • Concurrency: Backend-dependent.

  • FFI: {-# FOREIGN GHC ... #-} / {-# COMPILE GHC ... #-} pragmas bind Agda declarations to Haskell:

    {-# FOREIGN GHC import qualified Data.Text as T #-}
postulate
  Text : Set
  pack : String → Text
{-# COMPILE GHC Text = type T.Text #-}
{-# COMPILE GHC pack = T.pack #-}

    JS backend uses {-# COMPILE JS ... #-}. (https://agda.readthedocs.io/en/latest/language/foreign-function-interface.html)

  • Reflection: Agda’s reflection API is arguably the most expressive of the dependent-typed family — Term, Pattern, Clause, Definition are first-class data types; unquoteDecl / unquoteDef lets you generate code from a metaprogram running in the TC monad. (https://agda.readthedocs.io/en/latest/language/reflection.html)

  • Performance tools: agda --profile=... (categories: interactive, internal, definitions); --no-positivity-check/--termination-depth to diagnose checker bottlenecks.

  • Tactics & proof automation: Agda philosophically prefers term-mode. The minimal automation is:

    • Agsy (C-c C-a) — built-in proof search, weak compared to auto/omega.
    • tactic arguments — declare an argument as {{ @0 t : Tac _ }} to invoke a TC-monad procedure.
    • Reflection-based tactics — community libs (agda-prelude, agda-tactics) provide auto-like functions in the TC monad.

God mode

  • Instance arguments: Agda’s typeclass equivalent. Declared with {{...}}, resolved by the elaborator from in-scope instance declarations:

    record Eq (A : Set) : Set where
  field _==_ : A → A → Bool
open Eq {{...}} public
instance
  EqNat : Eq ℕ
  EqNat ._==_ n m = ...

    More predictable than Haskell’s typeclasses (no orphan/coherence issues by construction) but slower elaboration.

  • with and rewrite clauses: with adds a value to the LHS so you can pattern match on it; rewrite eq rewrites the goal type using a propositional equality. Idiomatic Agda is unimaginable without them.

    filter : (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

  • Mutual blocks + termination checking: mutual lets several definitions reference each other; the termination checker uses structural recursion plus size analysis. When it fails, options: refactor, use sized types (Size, Size< i, --sized-types), {-# TERMINATING #-} annotation (escape hatch — unsafe).

  • Copatterns + records as coinductive: Records can be defined by copatterns — equations on projections rather than constructors:

    record Stream (A : Set) : Set where
  coinductive
  field head : A
        tail : Stream A
open Stream
zeros : Stream ℕ
zeros .head = 0
zeros .tail = zeros

  • Sized types: Annotate inductive types with a size index; the termination checker uses size monotonicity instead of structural decrease. Powerful but the typing rules for sizes themselves have a known soundness gap ({-# OPTIONS --sized-types #-} is not on by default in 2.6+; use with care).

  • Universe polymorphism + cumulativity: Levels are first-class values of type Level with lzero, lsuc, _⊔_. --cumulativity makes universes cumulative (controversial — off by default).

  • K axiom vs --without-K: Pattern matching in Agda implies the K axiom (uniqueness of identity proofs) by default. {-# OPTIONS --without-K #-} restricts pattern matching to be HoTT-compatible — necessary for Cubical Agda and any HoTT formalization. (https://agda.readthedocs.io/en/latest/language/without-k.html)

  • Cubical Agda: {-# OPTIONS --cubical #-} enables Cubical Type Theory natively — univalence is a theorem, higher inductive types work, function extensionality is provable. The most cleanly HoTT-compatible system in production. https://agda.readthedocs.io/en/latest/language/cubical.html, https://github.com/agda/cubical

  • Reflection / unquoteDecl: Reify a Term from a quoted expression with quoteTerm, manipulate it with TC monad combinators (getDefinition, inferType, checkType), then unquoteDecl name = ... to introduce a new definition synthesized from a Term. Used to derive Eq/Show-style instances and write tactic libraries.

  • Backends:

    • MAlonzo / GHC — primary; compiles to Haskell.
    • JavaScript — for browser deployment.
    • Erlang — community.
    • Agate / agda2hs (https://github.com/agda/agda2hs) — extracts a subset of Agda to readable Haskell, for verified-Haskell development.

  • agda --interaction-json: Stable JSON protocol for editor-agnostic interactive mode — used by the VS Code extension and emerging LSP tools.

Idioms & style

  • Naming: Heavy use of Unicode (ℕ, →, ⊥, ⊤, ≡, ∷, ⊎, Σ, ∀, ∃). lowerCamelCase for terms, UpperCamelCase for types and modules. Mixfix names use _ (if_then_else_, _++_, _<_).
  • Formatter / linter: No standard formatter. The stdlib’s CHANGELOG.md plus a thorough type-checker substitute for one. Style guidance: https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md.
  • Idiomatic patterns: Express invariants in indexed types (Vec A n, Fin n); prove with refl + rewrite + cong; use copatterns for productive coinduction; pick --without-K if there’s any chance of HoTT later.
  • What experts look for: Termination checker passing without {-# TERMINATING #-}; positivity checker passing without {-# NO_POSITIVITY_CHECK #-}; no postulate for non-axiom things; correct use of --without-K if doing HoTT; clean copatterns over head/tail.

Ecosystem

  • agda-stdlib (https://github.com/agda/agda-stdlib) — the canonical standard library.
  • agda/cubical (https://github.com/agda/cubical) — the Cubical Type Theory library; the primary HoTT formalization in any system.
  • agda-categories — category theory.
  • agda-prelude — alternative slimmer prelude.
  • HoTT-Agda — pre-cubical HoTT library (Brunerie, Licata).
  • plfa.github.io (Programming Language Foundations in Agda, Wadler et al.) — the standard textbook for learning Agda. https://plfa.github.io/
  • Notable formalizations:
    • Brunerie’s π_4(S^3) = ℤ/2ℤ — synthetic homotopy theory in Cubical Agda.
    • Software Foundations-style PL semantics — many courses use Agda.
    • Type-driven library design — the agda-stdlib itself is a showcase.

Gotchas

  • Termination checker is conservative: Lots of “obviously terminating” functions (filter-style with extra guards) need with clauses or sized types to pass.
  • with reduces both sides: with p x substitutes p x everywhere in the goal and context — leading to confusing unification failures. The with-abstraction is one of Agda’s hardest concepts.
  • Pattern matching uses K by default: Innocent code may break under --without-K. Decide your stance per project.
  • Implicits + instance arguments slow elaboration: Heavy stdlib use can make agda --compile minutes-long for medium files.
  • Postulates and --no-positivity-check are unsafe: They admit ⊥. CI should grep for both.
  • No real package manager: Library installation is manual git clone + ~/.agda/libraries editing. Docker images and Nix flakes mitigate this in practice.
  • Editor-driven workflow is non-negotiable: Reading Agda source without an editor that fills in implicit args and shows hole types is brutal. Plan your tooling.
  • Set ω errors: When level inference fails, you get “Setω is not a valid type” — almost always means a missing Level parameter or universe-polymorphic generalization.
  • Mixfix parsing surprises: if x then y else z works; if x then y does not. Mixfix names must be applied to all their argument positions or fully eta-expanded.
  • The Haskell backend is fragile to GHC version drift. Pinning a GHC + Agda + stdlib triple via Nix or Docker is the standard practice.

Citations

Graph View